Publications (co-) authored by Rance Cleaveland: 1996


Efficient local model checking for fragments of the modal mu-calculus.
In T. Margaria and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), volume 1055 of Lecture Notes in Computer Science, pages 107--126, Passau, Germany, March 1996. Springer-Verlag.
Abstract:

This paper develops efficient local model-checking algorithms for expressive fragments of the modal mu-calculus. The time complexity of our procedures matches that of the best existing global algorithms; however, in contrast to those routines, ours explore a system's state space in a need-driven fashion and do not require its a priori construction. Consequently, our algorithms should perform better in practice. Our approach relies on a novel reformulation of the model-checking problem for the modal mu-calculus in terms of checking whether certain linear-time temporal formulas are satisfied by generalized Kripke structures that we call and-or Kripke structures.


Efficient model checking via the equational mu-calculus.
In Eleventh Annual Symposium on Logic in Computer Science (LICS '96), pages 304--312, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.
Abstract:

This paper studies the use of an equational variant of the modal mu-calculus as a unified framework for efficient temporal logic model checking. In particular, we show how an expressive temporal logic, CTL*, may be efficiently translated into the mu-calculus. Using this translation, one may then employ mu-calculus model-checking techniques, including on-the-fly procedures, BDD-based algorithms and compositional model-checking approaches, to determine if systems satisfy formulas in CTL*.


Formality and Software Design.
ACM Computing Surveys, 28es(4), December 1996.
Note: This is an electronic issue of the journal.
Semantic Theories and System Design.
ACM Computing Surveys, 28es(4), December 1996.
Note: This is an electronic issue of the journal.
A theory of testing for soft real-time systems.
To appear in Eighth International Conference on Software Engineering and Knowledge Engineering (SEKE '96), pages 474--479, Lake Tahoe, Nevada, June 1996. Knowledge Systems Institute, Skokie, Illinois.
Abstract:

We present a semantic framework for soft real-time processes, i.e., processes that meet their deadlines most of the time. The key components of our framework are: (1) a specification language PDP (for Probabilistic and Discrete-time Processes) that incorporates both probabilistic and timing aspects of process behavior; (2) a formal operational semantics for PDP given as a recursively defined probability distribution function over process terms and atomic actions; and (3) a natural notion of a process passing a test with a certain probability, where a test is a process with the added capability of reporting success. By encoding deadlines as tests, the probability of a process passing a test may now be interpreted as the probability of the process meeting a deadline, thereby capturing the essence of soft real-time. A simple video frame transmission example illustrates our approach.


The Concurrency Factory software development environment.
In T. Margaria and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), volume 1055 of Lecture Notes in Computer Science, pages 391--395, Passau, Germany, March 1996. Springer-Verlag.
Abstract:

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.

This demo is intended to demonstrate the following features of the Concurrency Factory: the graphical user interface VTView and VTSim, the local model checker for the alternation-free modal mu-calculus, and the graphical compiler that transforms VTView specifications into executable code.


The Concurrency Factory: A development environment for concurrent systems.
In R. Alur and T. Henzinger, editors, Computer-Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, pages 398--401, New Brunswick, NJ, July 1996. Springer-Verlag.
Abstract: The Concurrency Factory supports the specification, simulation, verification, and implementation of real-time concurrent systems such as communication protocols and process control systems. While the system uses process algebra as its underlying design formalism, the primary focus of the project is practical utility: the tools should be usable by engineers who are not familiar with formal models of concurrency, and they should be capable of handling large-scale systems such as those found in the telecommunications industry.

This paper serves as a status report for the Factory project and briefly describes a case-study involving the GNU UUCP i-protocol.


A process algebra with distributed priorities.
In U. Montanari and V. Sassone, editors, CONCUR '96, volume 1119 of Lecture Notes in Computer Science, pages 34--49, Pisa, Italy, August 1996. Springer-Verlag.
Abstract:

This paper presents a process algebra for distributed systems in which some actions may take precedence over others. In contrast with existing approaches to priorities, our algebra only allows actions to pre-empt others at the same ``location'' and therefore captures a notion of localized precedence. Using Park's and Milner's notion of strong bisimulation as a basis, we develop a behavioral congruence and axiomatize it for finite processes; we also derive an associated observational congruence. Simple examples highlight the utility of the theory.

Note: A journal version subsumes this paper.


Priorities for verifying distributed systems.
In T. Margaria and B. Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '96), volume 1055 of Lecture Notes in Computer Science, pages 278--297, Passau, Germany, March 1996. Springer-Verlag.
Abstract:

This paper illustrates the use of priorities in process algebras by a real-world example dealing with the design of a safety-critical network which is part of a railway signaling scheme. Priorities in process algebras support an intuitive modeling of distributed systems since undesired interleavings can be suppressed. This fact also leads to a substantial reduction in the sizes of models. We have impelemnted a CCS-based process algebra with priorities as a new front-end for the NCSU Concurrency Workbench, and we use model checking for verifying properties of the signaling system.

Note: A journal version subsumes this paper.


Modeling and verifying distributed systems using priorities: A case study.
Software Concepts and Tools 17:50--62, 1996.
Abstract:

This paper illustrates the use of priorities in process algebras by a real-world example dealing with the design of a safety-critical network which is part of a railway signaling system. Priorities in process algebras support an intuitive modeling of distributed systems since undesired interleavings can be suppressed. This fact also leads to a substantial reduction of the sizes of the models. We have implemented a CCS-based process algebra with priorities as a new front-end for the NCSU Concurrency Workbench, and we used model checking for verifying properties of the signaling system.


The NCSU Concurrency Workbench.
In R. Alur and T. Henzinger, editors, Computer-Aided Verification (CAV '96), volume 1102 of Lecture Notes in Computer Science, pages 394--397, New Brunswick, NJ, July 1996. Springer-Verlag.
Abstract:

The NCSU Concurrency Workbench is a tool for verifying finite-state systems. A key feature is its flexibility; its modular design eases the task of adding new analyses and changing the language users employ for describing systems. This note gives an overview of the system's features, including its capacity for generating diagnostic information for incorrect systems, and discusses some of its applications.


Strategic directions in computing research: Concurrency working group report
To appear in ACM Computing Surveys, 28(4):607--625, December 1996.

W. Elseaidy, J. Baugh and R. Cleaveland
Verification of an active control system using temporal process algebra.
Engineering with Computers12:46--61, 1996.
Note: This paper is not available on-line. Interested parties should contact John Baugh for a copy of it.
Formal timing analysis for fault-tolerant active structural control systems.
In Proceedings of the First Workshop on Formal Methods in System Practice, San Diego, January 1996.
Abstract:

This paper presents the results of a case study involving the use of a formal graphical notation, Modechart, and an automatic verification tool, the Concurrency Workbench, to the analysis of the design of a fault-tolerant active structural control system. Such control systems must satisfy strict requirements on their timing behavior; we show how to use various features supported by the Workbench to examine the timing behavior of different design alternatives, one of which has in excess of 10^19 states. The simple techniques illustrated here may be used by systems designers to model and anlayze other large and complex real-time systems as well.

Note: A journal version subsumes this paper.


An algebraic theory of process efficiency.
In Eleventh Annual Symposium on Logic in Computer Science (LICS '96), pages 63--72, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.
Abstract:

This paper presents a testing-based semantic theory for reasoning about the efficiency of concurrent systems as measured in terms of the amount of their internal activity. The semantic preorders are given an algebraic characterization, and their optimality is established by means of a full abstractness result. They are also shown to subsume existing bisimulation-based efficiency preorders. An example is provided to illustrate the utility of this approach.


Predictability of real-time systems: A process-algebraic approach.
In Real-Time Systems Symposium, pages 82--91, Washington, DC, December 1996. IEEE Computer Society Press.
Abstract:

This paper presents a testing-based semantic preorder for reasoning about the predictability of real-time systems specified using the process description language TPL. The predictability of the systems is measured in terms of the amount of variability present in their ``activity-completion times''. The semantic preorder is shown to coincide with an already existing, well-investigated implementation relation for TPL -- the must-preorder. Further the optimality of the semantics is established by means of a full abstractness result. An example is provided to illustrate the utility of this work.


Go to Rance Cleaveland's publication home page.

Last modified: August 13, 1998

Rance Cleaveland
rance@cs.sunysb.edu