FORWARD AND BACKWARD SIMULATIONS
FORWARD AND BACKWARD SIMULATIONS
复制标题
DOI：
10.1006/inco.1995.1134
复制
发表时间：
1995-09-01
影响因子：
1
通讯作者：
VAANDRAGER, F
中科院分区：
文献类型：
--
作者：
LYNCH, N;VAANDRAGER, F
根据简单的无定时自动机模型，给出了用于验证并发系统的仿真技术的统一、全面的介绍。特别是，定义了（1）细化，（2）前向和后向模拟，（3）混合前向-后向和后向-前向模拟，以及（4）历史和预言关系。历史和预言关系是Abadi和Lamport的历史和预言变量以及Owicki和Gries的辅助变量的抽象版本，陈述和证明了不同类型模拟之间的关系以及结果的健全性和完整性。最后，展示了如何将不变量纳入所有模拟中。尽管许多结果是首次在此提出，但本文也可以被视为对模拟技术研究文献的综述（在简单的背景下）。无定时自动机的开发旨在支持定时自动机的类似开发，本文的第二部分将展示如何将本文的结果转移到定时自动机的设置中。 (C) 1995 学术出版社
A unified, comprehensive presentation of simulation techniques for verification of concurrent systems is given, in terms of a simple untimed automaton model. In particular, (1) refinements, (2) forward and backward simulations, (3) hybrid forward-backward and backward-forward simulations, and (4) history and prophecy relations are defined. History and prophecy relations are abstract versions of the history and prophecy variables of Abadi and Lamport, as well as the auxiliary variables of Owicki and Gries, Relationships between the different types of simulations, as well as soundness and completeness results, are stated and proved. Finally, it is shown how invariants can be incorporated into all the simulations. Even though many results are presented here for the first time, this paper can also be read as a survey (in a simple setting) of the research literature on simulation techniques. The development for untimed automata is designed to support a similar development for timed automata, Part II of this paper will show how the results of this paper can be carried over to the setting of timed automata. (C) 1995 Academic Press, Inc.