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

• 作者: 杨潇潇 段振华
• 来源期刊: 计算机科学
• 学科: 工学
• 关键词: 时序逻辑程序 正则形 良基关系 良基归纳法 不变式证明
• 年，卷（期）: 2009,（6）
• 所属期刊栏目: 软件工程与数据库技术
• 页码范围: 150-152
• 页数: 3页
• 分类号: TP301
• 字数: 3881字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-137X.2009.06.038

摘要

并发程序的不变式验证对理解程序和提高程序的正确性具有重要意义.以一种区间时序逻辑程序设计语言Framed Tempura为研究对象,给出了该语言的等价正则形,定义了该正则形在相邻两个状态上的良基关系,进而利用良基归纳法原理对该语言所描述的系统的不变式进行归纳验证.提出的基于良基归纳法的验证方法在时序逻辑程序中可以方便地验证系统的不变式,尤其是循环结构的不变量性质.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	段振华	西安电子科技大学计算理论与技术研究所	47	363	10.0	16.0
2	杨潇潇	西安电子科技大学计算理论与技术研究所	2	2	1.0	1.0