一种基于Büchi自动机LTL程序模型检测方法.pdf

计算机与现代化 YUXIANDAIHUA 2010年第8期 JISUANJI 总第180期 文章编号：1006-2475(2010)08-0058-04 罗清胜 (江西财经大学国际学院，江西南昌330013) 摘要：时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。基于自动机的理论，用标签转移系统(S)表示程 序的行为，用时序逻辑公式(F)描述程序的性质，构建相应的BncIli自动机，从而证明形式化公式s}F是否可满足。 关键词：线性时序逻辑；Biichi自动机；模型检测 中图分类号：TPl8 文献标识码：A doi：10．3969／j．issn．1006-2475．2010．08．017 BasedB／ichiAutonmton AMethodforLinear Model on Logic Checking TemporalPrograms LUO Qing—sheng Schoolof of (IntemationalJiangxiUniversityFinanceEconomics，Nanchang330013，China) verificationof all rolein Abstract：Formaltemporallogicprogramsplaysimportantimprovingprogram on labeledtransition BtichiAutomatonisconstructedbasedautomata which theory。in system(S)indicating whetherformalformulaS}Fissatisfiableornot． that pondlogicformulas(F)indicatingprograms’property．Thus。itproves words：Lineartime Key temporallogic；Bfichiautomaton；modelchecking 自动机，并用形式化的方法对给定的系统是否具有所 0 引 言 期望的性质进行验ii[E4,7-8]。 随着计算机软硬件系统日益复杂，如何保证其正 I LTL的语法和语义 确性和可靠性成为紧迫的问题。形式化方法由于是 建立在严格的数学基础之上，可以通过符号化的手段 在线性时序逻辑的构想中，在语法和语义层次上 来描述系统的属性，支持系统属性的推理及系统描述 把动作看作一阶对象，首先考虑由动作索引的下一状 的正确性验证…。程序的形式化验证方法主要有定 态模式的m的版本一J。 理证明和模型检测。定理证明的验证方法过程复杂， 给定—个原子命题的有限非空集P={P。，P2，…}， 只能判断系统是否满足性质，不能找出违反性质的原 因¨。2l。而模型检测具有较高的自动化程度，当系统 义：m(