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

Verification of programs based on an axiom system for the MSVL language

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

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

出　　处：《西安电子科技大学学报》2010年第1期96-101,共6页Journal of Xidian University

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

摘　　要：MSVL语言是一种用于模拟、建模和验证程序的区间时序逻辑程序设计语言.为了证明区间时序逻辑程序的正确性,提出了MSVL语言的一个公理系统:包括正则形转换的状态公理和状态推演规则,以及将程序从一个状态转换到另一个状态的区间公理和区间推演规则.最后给出验证实例说明基于该公理系统的程序验证方法.The language MSVL is an interval temporal logic programming language. It can be used for the purpose of modeling, simulation and verification of programs. To prove the correctness of interval temporal logic programs, we present a proof system for MSVL. To do so, a set of state axioms and state inference rules is given to deduce a program into its normal form. In addition, a set of axioms and inference rules over intervals is formalized to transform a program from one state to another. Finally, an example is given to illustrate how the axiom system works.

关 键 词：形式验证 时序逻辑 正则形 安全性 公理系统 

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