软件学报
軟件學報
연건학보
JOURNAL OF SOFTWARE
2014年
11期
2452-2472
,共21页
阚双龙%黄志球%陈哲%徐丙凤
闞雙龍%黃誌毬%陳哲%徐丙鳳
감쌍룡%황지구%진철%서병봉
事件自动机%可满足性模理论%有界模型检测%自动机可达树%安全关键软件
事件自動機%可滿足性模理論%有界模型檢測%自動機可達樹%安全關鍵軟件
사건자동궤%가만족성모이론%유계모형검측%자동궤가체수%안전관건연건
event automata%satisfiability modulo theory%bounded model checking%automaton reachability tree%safety critical software
提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。
提齣使用事件自動機對 C 程序的安全屬性進行規約,併給齣瞭基于有界模型檢測的形式化驗證方法。事件自動機可以規約程序中基于事件的安全屬性,且可以描述無限狀態的安全屬性。事件自動機將屬性規約與C程序本身隔離,不會改變程序的結構。在事件自動機的基礎上,提齣瞭自動機可達樹的概唸。結閤自動機可達樹和有界模型檢測技術,給齣將事件自動機和C程序轉化為可滿足性模理論SMT(satisfiability modulo theory)模型的算法。最後,使用SMT求解器對生成的SMT模型求解,併根據求解結果給齣反例路徑分析算法。實例分析和實驗結果錶明,該方法可以有效驗證軟件繫統中針對事件的屬性規約。
제출사용사건자동궤대 C 정서적안전속성진행규약,병급출료기우유계모형검측적형식화험증방법。사건자동궤가이규약정서중기우사건적안전속성,차가이묘술무한상태적안전속성。사건자동궤장속성규약여C정서본신격리,불회개변정서적결구。재사건자동궤적기출상,제출료자동궤가체수적개념。결합자동궤가체수화유계모형검측기술,급출장사건자동궤화C정서전화위가만족성모이론SMT(satisfiability modulo theory)모형적산법。최후,사용SMT구해기대생성적SMT모형구해,병근거구해결과급출반례로경분석산법。실례분석화실험결과표명,해방법가이유효험증연건계통중침대사건적속성규약。
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.