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

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

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

许庆国, 缪淮扣

上海大学计算机工程与科学学院, 上海 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

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

摘要/Abstract

摘要： 时序逻辑作为一种规格说明语言,能够很好地描述程序性质.为了能够利用现有的定理证明器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

中图分类号:

TP311

许庆国, 缪淮扣. 基于PVS的时序逻辑语义模型及其实现[J]. 应用科学学报, 2006, 24(6): 598-603.

XU Qing-guo, MIAO Huai-kou. Temporal Logic Semantics Model and Its Implementation Using PVS[J]. Journal of Applied Sciences, 2006, 24(6): 598-603.

[1]	雷晓春, 潘奕伟, 张永雅, 江泽涛, 李孟桐. 基于复合三分支和深度特征编码的实时语义分割[J]. 应用科学学报, 2026, 44(2): 250-265.
[2]	刘永畅, 杜怡颖, 吴翠莹, 刘亚文. 航空影像引导的LiDAR点云语义分割[J]. 应用科学学报, 2025, 43(6): 922-934.
[3]	高剑奇, 黄典, 骆祥峰. 基于句法语义增强的实体事件关系对联合抽取[J]. 应用科学学报, 2025, 43(6): 1024-1036.
[4]	连晓峰, 康毛毛, 谭励, 王艳莉. 一种基于轻量化卷积模块的语义分割网络[J]. 应用科学学报, 2025, 43(1): 66-79.
[5]	华怡坦, 黄影平, 过文昊. 基于CNN和Transformer点云图像融合的道路检测[J]. 应用科学学报, 2024, 42(4): 695-708.
[6]	高剑奇, 骆祥峰, 裴昕淼. 基于实例分布约束的事件语义自动划分[J]. 应用科学学报, 2024, 42(2): 323-333.
[7]	郭子溢, 朱桐, 林广艳, 谭火彬. 球面坐标下基于语义分层的知识图谱补全方法[J]. 应用科学学报, 2024, 42(1): 119-133.
[8]	刘青, 陈艳平, 邹安琪, 秦永彬, 黄瑞章. 面向小样本抽取式问答的多标签语义校准方法[J]. 应用科学学报, 2024, 42(1): 161-173.
[9]	张耀方, 张哲宇, 李彤彤, 孙军, 王子博, 王佰玲. 融合工业控制操作的攻击建模[J]. 应用科学学报, 2023, 41(5): 855-869.
[10]	尹美杰, 倪翠, 王朋, 张广渊. 基于语义分割的遥感影像建筑变化检测[J]. 应用科学学报, 2023, 41(3): 448-460.
[11]	栗风永, 叶彬, 秦川. 基于奇偶交叉卷积的轻量级图像语义分割网络[J]. 应用科学学报, 2022, 40(3): 448-456.
[12]	郑智文, 甘健侯, 周菊香, 欧阳昭相, 鹿泽光. 基于注意力网络推理图的细粒度图像分类[J]. 应用科学学报, 2022, 40(1): 36-46.
[13]	包振山, 丁义龙, 张文博. 具备认知能力的行为模仿机器人系统[J]. 应用科学学报, 2022, 40(1): 13-24.
[14]	张涵, 秦昆, 毕奇, 张晔, 许凯. 注意力引导的三维卷积网络用于遥感场景变化检测[J]. 应用科学学报, 2021, 39(2): 272-280.
[15]	毕奇, 童心, 张济勇, 许凯, 张涵, 秦昆. 基于PLSA和BoW的高分遥感影像小型港口检测[J]. 应用科学学报, 2019, 37(3): 301-312.