Publications (co-) authored by Rance Cleaveland: 1989

A semantics-based tool for the verification of finite-state systems.

In Proceedings of the IFIP Symposium on Protocol Specification, Testing and Verification, pages 287--302, Enschede, the Netherlands, June 1989. North-Holland.

The Concurrency Workbench is an automated tool that caters for the analysis of concurrent finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its scope: a variety of different verification methods, including equivalence checking, preorder checking, and model checking, are supported for several different process semantics. One experience from our work is that a large number of interesting verification methods can be formulated as combinations of a small number of primitive algorithms. The Workbench has been applied to examples involving the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research. We will present the architecture of the Workbench and illustrate the verification methods through some simple examples.

Note: A journal version subsumes this paper.

The Concurrency Workbench.

In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems (CAV '89), volume 407 of Lecture Notes in Computer Science, pages 24--37, Grenoble, France, June 1989. Springer-Verlag.

The Concurrency Workbench is an automated tool that caters for the analysis of networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its scope: a variety of different verification methods, including equivalence checking, preorder checking, and model checking, are supported for several different process semantics. One experience from our work is that a large number of interesting verification methods can be formulated as combinations of a small number of primitive algorithms. The Workbench has been applied to examples involving the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research.

Note: A journal version subsumes this paper.

Testing equivalence as a bisimulation equivalence.

In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems (CAV '89), volume 407 of Lecture Notes in Computer Science, pages 11--23, Grenoble, France, June 1989. Springer-Verlag.

In this paper we show how the testing equivalences and preorders on transition systems may be interpreted as instances of generalized bisimulation equivalences and prebisimulation preorders. The characterization relies on defining transformations on the transition systems in such a way that the testing relations on the original systems correspond to (pre)bisimulation relations on the altered systems. Using these results, it is possible to use algorithms for determining the (pre)bisimulation relations in the case of finite-state transition systems to compute the testing relations.

Note: A journal version subsumes this paper.

Last modified: August 13, 1998