良基归纳法在时序逻辑程序不变式验证中的应用  

Application of Well-founded Induction in Verifying Invariance of Temporal Logic Programs

作　　者：杨潇潇[1] 段振华[1] 

机构地区：[1]西安电子科技大学计算理论与技术研究所,西安710071

出　　处：《计算机科学》2009年第6期150-152,共3页Computer Science

基　　金：国家自然科学基金资助项目(60873018);国家自然科学基金重大资助项目(60433010)资助

摘　　要：并发程序的不变式验证对理解程序和提高程序的正确性具有重要意义。以一种区间时序逻辑程序设计语言Framed Tempura为研究对象,给出了该语言的等价正则形,定义了该正则形在相邻两个状态上的良基关系,进而利用良基归纳法原理对该语言所描述的系统的不变式进行归纳验证。提出的基于良基归纳法的验证方法在时序逻辑程序中可以方便地验证系统的不变式,尤其是循环结构的不变量性质。Invariance properties are very central in concurrent software systems. Thinking by virtue of establishing an invariant and preserving it has immediate implications for reasoning about programs and their design. In this paper, we emploied an interval temporal logic programming language, called Framed Tempura, to specify concurrent systems, and gave the logical equivalent normal form for this language. Further, we investigated and defined a well-fotmded relation based on the normal form. Therefore, well-founded induction can be used to verify the invariance properties of the temporal logic programs.

关 键 词：时序逻辑程序 正则形 良基关系 良基归纳法 不变式证明 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]