| 摘要: |
| 本文提出了一个用于反应系统规范及验证的修改时序逻辑．它包含一个用于显示区分程序执行步同环境执行步的机制．环境的特性可以在系统开发时进行考虑．文中首先给出了程序的一个可复合计算模型──模块转换系统．基于此模型，给出了修改时序逻辑以及它的证明规则．本文提出的方法基于Manna－Pnueli的时序逻辑框架．经典的资源分配问题的例子用于说明此方法．最后给出了并行复合原理，它可以看成是Abadi和LamPort的关于复合假设／保证规范研究工作的具体应用． |
| 关键词: 反应系统 时序逻辑 规范 验证 模块转换系统 资源分配问题 并行复合 假设／保证规范 |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到博士点基金及江苏省应用基础基金资助. |
|
| A MODIFIED TEMPORAL LOGIC FOR REACTIVE SYSTEMS |
|
JIA Guoping,ZHENG Guoliang
|
| Abstract: |
| This paper presents a modified version of temporal logics for the specification and verification of reactive systems．It includes a mechanism tO explicitly distinguish pro-gram steps from environment steps and the characteristics of the environment can be taken into account during the development of system．A compositional computation model of programs——modular transition system is firstly given．Then based on this model，a mod-ified temporal logic and its proof rules are presented．The proposed approach is used with-in Manna-Pnueli'S temporal logic framework．The classical example of the Resource Allo-cator is used tO illustrate the approach．At the end of the paper，a parallel composition principle is proposed，it can be viewed as an application of Abadi and Lamport'S works on
the composing assumption/guarantee specifications． |
| Key words: Reactive system temporal logic specification verification modular transition system resource allocator parallel composition assumption/guarantee specification |
