###
DOI:
Journal of Software:1997.8(9):663-672

用于反应系统的修改时序逻辑
贾国平,郑国梁
(南京大学计算机科学系,南京,210093)
A MODIFIED TEMPORAL LOGIC FOR REACTIVE SYSTEMS
JIA Guoping,ZHENG Guoliang
()
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 4011   Download 2697
    Revised:October 22, 1996
> 中文摘要: 本文提出了一个用于反应系统规范及验证的修改时序逻辑.它包含一个用于显示区分程序执行步同环境执行步的机制.环境的特性可以在系统开发时进行考虑.文中首先给出了程序的一个可复合计算模型──模块转换系统.基于此模型,给出了修改时序逻辑以及它的证明规则.本文提出的方法基于Manna-Pnueli的时序逻辑框架.经典的资源分配问题的例子用于说明此方法.最后给出了并行复合原理,它可以看成是Abadi和LamPort的关于复合假设/保证规范研究工作的具体应用.
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.
文章编号:     中图分类号:    文献标志码:
基金项目:本文研究得到博士点基金及江苏省应用基础基金资助. 本文研究得到博士点基金及江苏省应用基础基金资助.
Foundation items:
Reference text:

贾国平,郑国梁.用于反应系统的修改时序逻辑.软件学报,1997,8(9):663-672

JIA Guoping,ZHENG Guoliang.A MODIFIED TEMPORAL LOGIC FOR REACTIVE SYSTEMS.Journal of Software,1997,8(9):663-672