使用事件自动机规约的C语言有界模型检测?

• 作者: 徐丙凤 阚双龙 陈哲 黄志球
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 事件自动机 可满足性模理论 有界模型检测 自动机可达树 安全关键软件
• 年，卷（期）: 2014,（11）
• 所属期刊栏目: 理论计算机科学
• 页码范围: 2452-2472
• 页数: 21页
• 分类号: TP301
• 字数: 16459字
• 语种: 中文

摘要

提出使用事件自动机对 C 程序的安全属性进行规约，并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性，且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离，不会改变程序的结构。在事件自动机的基础上，提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术，给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后，使用SMT求解器对生成的SMT模型求解，并根据求解结果给出反例路径分析算法。实例分析和实验结果表明，该方法可以有效验证软件系统中针对事件的属性规约。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	黄志球	南京航空航天大学计算机科学与技术学院	183	1755	20.0	33.0
2	陈哲	南京航空航天大学计算机科学与技术学院	25	189	7.0	13.0
3	徐丙凤	南京航空航天大学计算机科学与技术学院	16	297	9.0	16.0
4	阚双龙	南京航空航天大学计算机科学与技术学院	15	132	5.0	11.0