时序逻辑程序的模型检测

摘要：

时序逻辑程序的形式化验证对提高程序的正确性具有重要意义.以投影时序逻辑的可执行子集、框架投影时序逻辑语言Framed Tempura为研究对象,使用命题投影时序逻辑描述Framed Tempura程序的性质,将程序P和性质φ统一表示在投影时序逻辑中,模型检测需要判定p→φ是否有效,可转化为判定P ∧-φ是否不可满足,这可以通过构造P∧-φ的正则图加以解决.最后,给出了Framed Tempura程序的模型检测实例.

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

所属期刊栏目：36

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2009-12-08（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：164-167