MSVL语言的公理系统的程序验证

• 作者: 杨潇潇 段振华
• 来源期刊: 西安电子科技大学学报（自然科学版）
• 学科: 工学
• 关键词: 形式验证 时序逻辑 正则形 安全性 公理系统
• 年，卷（期）: 2010,（1）
• 页码范围: 96-101
• 页数: 6页
• 分类号: TP301
• 字数: 4287字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2400.2010.01.017

摘要

MSVL语言是一种用于模拟、建模和验证程序的区同时序逻辑程序设计语言.为了证明区间时序逻辑程序的正确性,提出了MSVL语言的一个公理系统:包括正则形转换的状态公理和状态推演规则,以及将程序从一个状态转换到另一个状态的区间公理和区问推演规则.最后给出验证实例说明基于该公理系统的程序验证方法.

作者信息

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