行业报告详情 - 行业报告数据库

行业分类

找到报告 1 篇当前为第 1 页共 1 页

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

作者：阚双龙；黄志球；陈哲；徐丙凤作者单位：南京航空航天大学计算机科学与技术学院加工时间：2014-12-18 信息来源：软件学报

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

行业分类

友情链接

联系我们

QQ咨询

电话咨询

微信公众号

感谢访问