| 时态逻辑形式化描述并发系统性质 |
| |
| 引用本文： | 肖美华,薛锦云. 时态逻辑形式化描述并发系统性质[J]. 海军工程大学学报, 2004, 16(5): 10-13 |
| |
| 作者姓名： | 肖美华 薛锦云 |
| |
| 作者单位： | 1. 江西师范大学,计算机信息工程学院,江西,南昌,330027;南昌大学,计算中心,江西,南昌,330029;中国科学院软件研究所,计算机科学重点实验室,北京,100080
2. 江西师范大学,计算机信息工程学院,江西,南昌,330027;中国科学院软件研究所,计算机科学重点实验室,北京,100080 |
| |
| 基金项目： | 国家自然科学基金资助项目(60273092)，江西省自然科学基金资助项目(0411041)，南昌大学2003年度科研基金资助项目 |
| |
| 摘 要： | 时态逻辑是一种描述反应式(并发)系统中状态迁移序列的形式化方法,用于刻画并发系统所需验证的性质,是模型检测的基础.阐述了时态逻辑CTL 及其子逻辑CTL、LTL的语法及语义,然后分析运用时态逻辑描述并发系统性质,最后给出一个应用实例.
|
| 关 键 词： | 形式化方法 并发系统 时态逻辑 模型检测 |
| 文章编号： | 1009-3486(2004)05-0010-04 |
| 修稿时间： | 2004-05-15 |
Formal description of properties of concurrency system by temporal logic |
| |
| XIAO Mei-hua. Formal description of properties of concurrency system by temporal logic[J]. Journal of Naval University of Engineering, 2004, 16(5): 10-13 |
| |
| Authors: | XIAO Mei-hua |
| |
| Affiliation: | XIAO Mei-hua~ |
| |
| Abstract: | The temporal logic is a formal method for describing sequences of transition between states in a reactive (concurrent) system. It is common to use the temporal logic to specify the properties that the design must satisfy. The temporal logic is the basic of model checking. This paper states the syntax and semantics of CTL~* and its sub-logics: CTL and LTL, and analyzes how to state the properties of concurrent system, and finally the application example is given. |
| |
| Keywords: | formal method concurrent system temporal logic model checking |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
