This paper presents a case study illustrating the different analytical facilities provided by the Concurency Workbench, an automatic verification tool for finite-state systems. The system we consider is the Alternating Bit Protocol, a communications protocol designed to ensure error-free data transfer over lossy media. Using the Workbench we investigate several features of the protocol, and we isolate a crucial property (the assumption of which is unstated in the protocol definition) that media must have in order for the protocol to be deadlock-free.
This paper develops an operational semantics for concurrent languages with value passing. An operation analogous to substitution in the lambda-calculus is given, and an operational equivalence is defined and shown to coincide with Milner's bisimulation equivalence. In contrast with existing process-algebraic approaches to value passing, this semantics does not reduce data exchange to pure synchronization over (potentially infinite) families of ports indexed by data.
In this paper we show how the testing equivalences and preorders on transition systems may be interpreted as instances of generalized bisimulation equivalences and prebisimulation preorders. The characterization relies on defining transformations on the transition systems in such a way that the testing relations on the original systems correspond to (pre)bisimulation relations on the altered systems. On the basis of these results, it is possible to use algorithms for determining the (pre)bisimulation relations in the case of finite-state transition systems to compute the testing relations.
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.
We develop a model-checking algorithm for a logic that permits propositions to be defined using greatest and least fixed points of mutually recursive systems of equations. This logic is as expressive as the alternation-free fragment of the modal mu-calculus identified by Emerson and Lei, and it may therefore be used to encode a number of temporal logics and behavioral preorders. Our algorithm determines whether a process satisfies a formula in time proportional to the product of the sizes of the process and the formula; this improves on the best known algorithm for similar fixed-point logics.
This paper aims to close the gap between real-time schedulability analysis approaches and formal specification and verification techniques. We develop a generalized approach to schedulability analysis that is mathematically founded in a process algebra called RTSL. RTSL is used to describe the functional behavior, timing behavior, timing constraints (or deadlines), and scheduling discipline for real-time systems. Within the framework of our approach, we formally model the most commonly used real-time scheduling disciplines and provide a capability for modeling others. The formal semantics of RTSL uses the scheduling discipline as a parameter and allows the reachable state space of any system to be automatically generated and searched for timing exceptions. We provide a generalized schedulability analysis algorithm to perform this state-based analysis.
Go to Rance Cleaveland's publication home page. |
Last modified: August 13, 1998
Rance Cleaveland