基于PVS的时序逻辑语义模型及其实现  

Temporal Logic Semantics Model and Its Implementation Using PVS

作　　者：许庆国[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海200072

出　　处：《应用科学学报》2006年第6期598-603,共6页Journal of Applied Sciences

基　　金：国家自然科学基金(60173031);国家"973"重点基础研究发展计划(2002CB312001)资助项目

摘　　要：时序逻辑作为一种规格说明语言,能够很好地描述程序性质.为了能够利用现有的定理证明器PVS(prototype verification system)对用时序逻辑公式描述的程序性质予以证明,从而达到程序验证的目的.文中在PVS中建立了时序逻辑的语义模型,同时给出了其语义解释.然后通过一个简单的例子(求解整数平方根的程序),应用时序逻辑公式对该程序的部分性质进行了描述,取得了较好的效果.实现了程序性质的时序逻辑公式表示,为使用PVS验证程序的性质打下了一个好的基础.As a specification language , temporal logic is powerful enough in expressing the properties for program. In order to prove the theorem that expresses the property （PVS）, this paper establishes a semantics model for using temporal logic formula in a prototype verification system temporal logic as well as the semantics interpretation. As an example, a program for solving the square root for an integer is investigated. Some properties of this program are in temporal logic formulas. An interface for verifying program by PVS is orovided. specified

关 键 词：时序逻辑 语义 定理证明 程序性质 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]