English

应用科学学报 ›› 2006, Vol. 24 ›› Issue (6): 598-603.

• 论文 • 上一篇    下一篇

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

许庆国, 缪淮扣   

  1. 上海大学计算机工程与科学学院, 上海 200072
  • 收稿日期:2005-12-12 修回日期:2006-01-11 出版日期:2006-11-30 发布日期:2006-11-30
  • 作者简介:许庆国,博士生,研究方向:实时系统的形式验证,E-mail:qgxu@mail.shu.edu.cn;缪准扣,教授,博导,研究方向:软件形式化方法、软件工程,E-mail:hkmiao@staff.shu.edu.cn
  • 基金资助:
    国家自然科学基金(60173031);国家"973"重点基础研究发展计划(2002CB312001)资助项目

Temporal Logic Semantics Model and Its Implementation Using PVS

XU Qing-guo, MIAO Huai-kou   

  1. School of Computer Engineering & Computer Science, Shanghai University, Shanghai 200072, China
  • Received:2005-12-12 Revised:2006-01-11 Online:2006-11-30 Published:2006-11-30

PDF

68

被引次数

3

摘要： 时序逻辑作为一种规格说明语言,能够很好地描述程序性质.为了能够利用现有的定理证明器PVS(prototype verification system)对用时序逻辑公式描述的程序性质予以证明,从而达到程序验证的目的.文中在PVS中建立了时序逻辑的语义模型,同时给出了其语义解释.然后通过一个简单的例子(求解整数平方根的程序),应用时序逻辑公式对该程序的部分性质进行了描述,取得了较好的效果.实现了程序性质的时序逻辑公式表示,为使用PVS验证程序的性质打下了一个好的基础.

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

Abstract: 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 using temporal logic formula in a prototype verification system (PVS), this paper establishes a semantics model for 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 specified in temporal logic formulas.An interface for verifying program by PVS is provided.

Key words: semantics, program properties, temporal logic, PVS

中图分类号: