%0 Journal Article
%T 用于反应系统的修改时序逻辑
%A 贾国平
%A 郑国梁
%J -
%D 1997
%X 本文提出了一个用于反应系统规范及验证的修改时序逻辑．它包含一个用于显示区分程序执行步同环境执行步的机制．环境的特性可以在系统开发时进行考虑．文中首先给出了程序的一个可复合计算模型──模块转换系统．基于此模型，给出了修改时序逻辑以及它的证明规则．本文提出的方法基于Manna－Pnueli的时序逻辑框架．经典的资源分配问题的例子用于说明此方法．最后给出了并行复合原理，它可以看成是Abadi和LamPort的关于复合假设／保证规范研究工作的具体应用
%K 反应系统 时序逻辑 规范 验证 模块转换系统 资源分配问题 并行复合 假设／保证规范
%U http://www.jos.org.cn/jos/ch/reader/view_abstract.aspx?file_no=19970904&flag=1