%0 Journal Article
%T A MODIFIED TEMPORAL LOGIC FOR REACTIVE SYSTEMS<br>用于反应系统的修改时序逻辑
%A JIA Guoping
%A ZHENG Guoliang
%A <br>贾国平
%A 郑国梁
%J 软件学报
%D 1997
%I 
%X This paper presents a modified version of ternporal logics for the specificationand verification of reactive systems. It includes a mechanism to explicitly distinguish pro-gram steps from environment steps and the characteristics of the erivironment can be takeninto account during the development of system. A cornpositional computation model ofprograrns-modular transition system is firstly given. Then based on this model, a mod-if ied temporal logic and its proof rules are presented. The proposed approach is used with-in Manna-Pnueli's ternporal logic framework. The classical example of the Resource Allo-cator is used to illustrate the approach. At the end of the paper, a parallel compositionprinciple is proposed, it can be viewed as an application of Abadi and Lamport's works onthe composing assurnption/guarantee specifications.
%K Reactive system
%K temporal logic
%K specification
%K verification
%K modular transition system
%K resource allocator
%K parallel composition
%K assumption/guarantee specification<br>反应系统
%K 时序逻辑
%K 规范
%K 验证
%K 模块转换系统
%K 资源分配问题
%K 并行复合
%K 假设／保证规范
%U http://www.alljournals.cn/get_abstract_url.aspx?pcid=5B3AB970F71A803DEACDC0559115BFCF0A068CD97DD29835&cid=8240383F08CE46C8B05036380D75B607&jid=7735F413D429542E610B3D6AC0D5EC59&aid=1F15034A31138DF69CB750F2E1C4C19A&yid=5370399DC954B911&vid=5D311CA918CA9A03&iid=9CF7A0430CBB2DFD&sid=46FF101E7ECF9F15&eid=B7DE0F3CA34DA149&journal_id=1000-9825&journal_name=软件学报&referenced_num=0&reference_num=22