The concurrency workbench
- 1 January 1993
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 15 (1) , 36-72
- https://doi.org/10.1145/151646.151648
Abstract
The Concurrency Workbench is an automated tool for analyzing networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its breadth: 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 the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research.Keywords
This publication has 22 references indexed in Scilit:
- An efficient algorithm for branching bisimulation and stuttering equivalencePublished by Springer Nature ,2005
- Bisimulation through probabilistic testingInformation and Computation, 1991
- Priorities in process algebrasInformation and Computation, 1990
- CCS expressions, finite state processes, and three problems of equivalenceInformation and Computation, 1990
- Submodule construction as equation solving in CCSTheoretical Computer Science, 1989
- Automated analysis of mutual exclusion algorithms using CCSFormal Aspects of Computing, 1989
- Characteristic formulaePublished by Springer Nature ,1989
- Modal logics for communicating systemsTheoretical Computer Science, 1987
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- A note on reliable full-duplex transmission over half-duplex linksCommunications of the ACM, 1969