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 telecommuncations 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 simulator for VTView specifications; and a graphical compiler that transforms VTView and VPL specifications into executable code.
This paper presents a framework for the abstract interpretation of processes that pass values. We define a process description language that is parameterized with respect to the set of values that processes may exchange and show that an abstraction over values induces an abstract semantics for processes. Our main results state that if the abstract value interpretation safely/optimally approximates the ground interpretation, then the resulting abstracted processes safely/optimally approximate those derived from the ground semantics (in a precisely defined sense). As the processes derived from an abstract semantics in general have far fewer states than those derived from a concrete semantics, our technique enables the automatic analysis of systems that lie beyond the scope of existing techniques.
This paper develops a semantic framework for concurrent languages with value passing. An operation analogous to substitution in the $\lambda$-calculus is given, and a semantics is given for a value-passing version of Milner's Calculus of Communicating Systems (CCS). An operational equivalence is then defined and shown to coincide with Milner's (early) bisimulation equivalence. We also show how semantics may given for languages with asynchronous communication primitives. In contrast with existing approaches to value passing, this semantics does not reduce data exchange to pure synchronization over (potentially infinite) families of ports indexed by data, and it avoids variable renamings that are not local to processes engaged in communication.
This paper describes the formal verification of the timing properties of the design of an intelligent structural control system using the Concurrency Workbench, an automatic verification tool for finite-state processes. The high-level design of the system is first given in Modechart, a graphical specification language for real-time systems, and then translated into a temporal process algebra supported by the Workbench. The facilities provided by this tool are then used to analyze the system and ultimately show it correct.
This paper defines a behavioral equivalence based on the notion of {\em weak observational equivalence} for processes in which actions may take priority over other actions. The largest congruence contained in this relation is then identified and given a complete equational axiomatization for finite processes. An example illustrates the utility of this equivalence which, in contrast with other equivalences for systems with priorities, abstracts from internal computation.
We present a testing preorder for probabilistic processes based on a quantification of the probability with which processes pass tests. The theory enjoys close connections with the classical testing theory of Hennessy and DeNicola in that whenever a process passes a test with probability 1 (respectively some non-zero probability) in our setting, then the process must (respectively may) pass the test in the classical theory. We also develop an alternative characterization of the probabilistic testing preorders that takes the form of a mapping from probabilistic traces to the interval [0,1], where a probabilistic trace is an alternating sequence of actions and probability distributions over actions.
Finally, we give proof techniques, derived from the alternative characterizations, for establishing preorder relationships between probabilistic processes. The utility of these techniques is demonstrated by means of some simple examples.
Note: A journal version subsumes this paper.
| Go to Rance Cleaveland's publication home page. |
Last modified: November 30, 1999
Rance Cleaveland