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

摘要：

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

关键词：事件自动机、可满足性模理论、有界模型检测、自动机可达树、安全关键软件

分类号：TP301(计算技术、计算机技术)

资助基金：国家自然科学基金61272083,61100034

在线出版日期：2015-01-22（万方平台首次上网日期，不代表论文的发表时间）

页数：共21页

页码：2452-2472