%0 Journal Article
%T 使用事件自动机规约的c语言有界模型检测
%A 阚双龙？
%A 黄志球？
%A 陈哲？
%A 徐丙凤？
%J 软件学报
%P 2452-2472
%D 2014
%R 10.13328/j.cnki.jos.004609
%X 提出使用事件自动机对c程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法.事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性.事件自动机将属性规约与c程序本身隔离,不会改变程序的结构.在事件自动机的基础上,提出了自动机可达树的概念.结合自动机可达树和有界模型检测技术,给出将事件自动机和c程序转化为可满足性模理论smt(satisfiabilitymodulotheory)模型的算法.最后,使用smt求解器对生成的smt模型求解,并根据求解结果给出反例路径分析算法.实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约.
%K 事件自动机
%K 可满足性模理论
%K 有界模型检测
%K 自动机可达树
%K 安全关键软件
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=4609&flag=1