查看文章

The Concurrency Workbench is an automated tool that caters for the analysis of concurrent nite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its scope: a variety of di erent veri cation 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 veri cation methods can be formulated as combinations of a small number of primitive algorithms. The Workbench has been applied to examples involving the veri cation 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 veri cation methods through some simple examples.