典型文献
面向计算机并发程序的形式化验证方法设计
文献摘要：
计算机并发性程序形式化验证一直是软件安全领域的难题.软件并发性漏洞难以被发现,一旦发生问题,会造成不可估量的安全问题.形式化验证基于严格的数学推导基础,采用语言、语义、推理证明三位一体方法,构建形式逻辑系统,以确保被验证系统的安全性能.传统的形式化验证方法由于人工参与多、验证工作量大、验证效率低等不足,难以对计算机并发程序进行严谨高效的模型描述与验证.研究了一种可双向转换的并发性程序形式化验证方法,解决了人工抽象建模存在的工作量大且易出错的问题,并且保证了源码层与抽象层验证的一致性,大幅提升了形式化验证的效率.
文献关键词：
软件并发;形式化建模;功能正确性验证;属性验证
中图分类号：
作者姓名：
谢小赋;曾梦岐;庞飞
作者机构：
中国电子科技集团有限公司第三十研究所,四川 成都 610041
文献出处：
引用格式：
[1]谢小赋;曾梦岐;庞飞-.面向计算机并发程序的形式化验证方法设计)[J].信息安全与通信保密,2022(03):54-62
A类：
软件并发,功能正确性验证
B类：
并发程序,形式化验证,验证方法,方法设计,软件安全,安全领域,发生问题,不可估量,数学推导,推理证明,构建形式,形式逻辑,逻辑系统,验证系统,安全性能,出错,源码,形式化建模,属性验证
AB值：
0.336966
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
