时序逻辑程序的模型检测  

Model Checking for Temporal Logic Programs

作　　者：王小兵[1,2] 段振华[1] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,西安710071 [2]武汉大学软件工程国家重点实验室,武汉430072

出　　处：《计算机科学》2009年第10期164-167,共4页Computer Science

基　　金：国家自然科学基金重点资助项目(60433010);国家自然科学基金资助项目(60873018);武汉大学软件工程国家重点实验室开放基金项目(SKLSE20080713)资助

摘　　要：时序逻辑程序的形式化验证对提高程序的正确性具有重要意义。以投影时序逻辑的可执行子集、框架投影时序逻辑语言Framed Tempura为研究对象,使用命题投影时序逻辑描述Framed Tempura程序的性质,将程序p和性质Ф统一表示在投影时序逻辑中,模型检测需要判定p→Ф是否有效,可转化为判定p∧Ф是否不可满足,这可以通过构造p∧Ф的正则图加以解决。最后,给出了Framed Tempura程序的模型检测实例。Formal verification of temporal logic programs plays an important role in improving program correctness. A framing projection temporal logic language, called Framed Tempura, is the research object as an executable subset of projection temporal logic. Propositional temporal logic was used to describe properties of a Framed Tempura program, thus the program p and properties φ were both formalized in projection temporal logic, then model checking needs to eva-luate whether or not p→φ is valid which can be translated into evaluate whether or not P∧-φ is unsatisfiable,and this problem is solved by constructing the normal form graph of p P∧-φ. At last, an example of model checking a Framed Tempura program was given.

关 键 词：时序逻辑程序 形式化验证 正则图 模型检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]