实时系统形式规格说明在PVS中的建立

计算机科学 ›› 2006, Vol. 33 ›› Issue (12): 238-242.

• 计算机网络与信息安全 • 上一篇下一篇

实时系统形式规格说明在PVS中的建立

许庆国缪淮扣

上海大学计算机学院,上海200072

出版日期:2018-11-17 发布日期:2018-11-17
基金资助:
本文受国家自然科学基金项目（批准号60173031）和国家973项目（编号：2002CB312001）资助.

XU Qing-Guo, MIAO Huai-Kou （School of Computer Engineering ＆Computer Science, Shanghai University,Shanghai 200072）

Online:2018-11-17 Published:2018-11-17

摘要/Abstract

摘要： 本文首先简介了时间自动机和时间Büchi自动机形式模型，结合时间化时序逻辑（Timed Temporal Logic）的语法和语义，利用定理证明器PVS（Prototype Verification System）实现了定义在时间自动机状态（或运行）上的时间化分支（或线性）时序逻辑规格说明的形式体系。在此基础上，结合一个经典的实时系统实例，用该体系对其实时特性进行了形式描述和形式验证，并得到了良好的结果。

关键词: 实时系统时间Büchi自动机时间化时序逻辑 PVS

Abstract: On the Basis of the formal model of the timed automata, timed Büchi automata and the formal syntax and semantics of the timed temporal logic, some formal theories about timed branch （linear） temporal logic are implemented over the states （runs） of the tim

Key words: Real-time, Timed temporal logic, Timed büchi automata, PVS

许庆国缪淮扣. 实时系统形式规格说明在PVS中的建立[J]. 计算机科学, 2006, 33(12): 238-242. https://doi.org/

XU Qing-Guo, MIAO Huai-Kou （School of Computer Engineering ＆Computer Science, Shanghai University,Shanghai 200072）. [J]. Computer Science, 2006, 33(12): 238-242. https://doi.org/

参考文献

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed

实时系统形式规格说明在PVS中的建立

PDF (PC)

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 0

Metrics

本文评价

推荐阅读 0