Publications (co-) authored by Rance Cleaveland: 1993


Analyzing concurrent systems using the Concurrency Workbench.
In P.E. Lauer, editor, Functional Programming, Concurrency, Simulation and Automated Reasoning, volume 693 of Lecture Notes in Computer Science, pages 129--144. Springer-Verlag, 1993.
Abstract:

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.


An operational semantics of value-passing.
In Proceedings of the North American Process Algebra Workshop, Cornell University Technical Report TR 93-1369, Ithaca, New York, August 1993.
Abstract:

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.


Testing equivalence as a bisimulation equivalence.
Formal Aspects of Computing, 5:1--20, 1993.
Abstract:

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: A semantics-based verification tool for the verification of concurrent systems.
ACM Transactions on Programming Languages and Systems, 15(1):36--72, January 1993.
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.


A linear-time model-checking algorithm for the alternation-free modal mu-calculus.
Formal Methods in System Design, 2:121--147, 1993.
Abstract:

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.


A. Fredette and R. Cleaveland.
A generalized approach to real-time schedulability analysis.
In Proceedings of the Workshop on Real-Time Operating Systems and Software, pages 98--103, New York, NY, May 1993.
Note: This paper is subsumed by the one immediately below.
RTSL: A language for real-time schedulability analysis.
Proceedings of the Real-Time Systems Symposium, pages 274--283, Durham, North Carolina, December 1993. Computer Society Press.
Abstract:

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
rance@cs.sunysb.edu