The Concurrency Workbench: A Semantics-based Tool for the Verification of Concurrent Systems
Rance Cleaveland, Joachim Parrow and Bernhard SteffenAbstract: 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.
This report was published in ACM Transactions on Programming Languages and Systems vol.15, no. 1 (Jan. 1993) pp. 36-72.
Previous | Index | Next