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