The concurrency factory - Practical tools for specification, simulation, verification, and implementation of concurrent systems
Rance Cleaveland, J Gada, P Lewis, Scott A. Smolka, Oleg V. Sokolsky, Shuhang Zhang · DIMACS series in discrete mathematics and theoretical computer science · 1994
. The Concurrency Factory is an integrated toolset for specification, simulation, verification, and implementation of concurrent systems such as communication protocols and process control systems. Two themes central to the project are the following: the use of process algebra , e.g., CCS, ACP, CSP, as the underlying formal model of computation, and the provision of practical support for process algebra. By "practical" we mean that the Factory should be usable by protocol engineers and software developers who are not necessarily familiar with formal verification, and it should be usable on problems of real-life scale, such as those found in the telecommunications industry. The main features of the Concurrency Factory are graphical (VTView) and textual (VPL) user interfaces; a suite of analysis routines for automatic verification including a bisimulation and model checker; a graphical simu- lator for VTView specifications; and a graphical compiler that transforms VTView and VPL speci...