首页 | 本学科首页   官方微博 | 高级检索  
     

使用事件自动机规约的C语言有界模型检测
引用本文:阚双龙,黄志球,陈哲,徐丙凤.使用事件自动机规约的C语言有界模型检测[J].软件学报,2014,25(11):2452-2472.
作者姓名:阚双龙  黄志球  陈哲  徐丙凤
作者单位:南京航空航天大学计算机科学与技术学院,江苏南京,210016
基金项目:国家自然科学基金(61272083, 61100034)
摘    要:提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。

关 键 词:事件自动机  可满足性模理论  有界模型检测  自动机可达树  安全关键软件
收稿时间:2013/7/30 0:00:00
修稿时间:2014/3/28 0:00:00

Bounded Model Checking of C Programs Using Event Automaton Specifications
KAN Shuang-Long,HUANG Zhi-Qiu,CHEN Zhe and XU Bing-Feng.Bounded Model Checking of C Programs Using Event Automaton Specifications[J].Journal of Software,2014,25(11):2452-2472.
Authors:KAN Shuang-Long  HUANG Zhi-Qiu  CHEN Zhe and XU Bing-Feng
Affiliation:College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China;College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China;College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China;College of Computer Science and Technology, Nanjing University of Aeronautics and Astronautics, Nanjing 210016, China
Abstract:In this paper, a technology is presented to use event automata to specify the safety properties of C programs and apply bounded model checking to verify whether a C program satisfies an event automaton property. An event automaton can specify a safety property which is based on the events generated by a program. It can also specify a property with infinite states. Since an event automaton separates from C programs, it will not change the structures of programs. The paper introduces the definition of an automaton reachability tree based on an event automaton. It then uses automaton reachability trees and the bounded model checking to build the SMT (satisfiability modulo theory) models of event automata and C programs. Finally, it supplies the SMT models to an SMT solver. An algorithm for generating counterexamples is obtained according to the results of the solver. The case studies and experimental results demonstrate that the presented approach can verify the event properties of software systems.
Keywords:event automata  satisfiability modulo theory  bounded model checking  automaton reachability tree  safety critical software
本文献已被 CNKI 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号