Publications (co-)authored by Rance Cleaveland: 2001

R. Cleaveland.
Alternative Approaches to Symbolic Verification: Preface by the Section Editor.
Software Tools for Technology Transfer 3(3):247-249, August 2001.
©2001 Springer-Verlag.

The papers in this special section present a sampling of new symbolic approaches determining whether or not a system satisfies its specification. Abstracts of these articles appeared originally in the Proceedings of the 1999 Symposium on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '99).

G. Bhat, R. Cleaveland and A. Groce.
Efficient Model Checking Via Büchi Tableau Automata.
In G. Berry, H. Comon and A. Finkel, editors, Computer-Aided Verification 2001, volume 2102 of Lecture Notes in Computer Science, pages 38-52, Paris, July 2001. Springer-Verlag.
©2001 Springer-Verlag. Abstract:

This paper describes an approach to engineering efficient model checkers that are generic with respect to the temporal logic in which system properties are given. The methodology is based on the ``compilation'' of temporal formulas into variants of alternating tree automata called \emph{alternating B\"uchi tableau automata} (ABTAs). The paper gives an efficient on-the-fly model-checking procedure for ABTAs and illustrates how translations of temporal logics into ABTAs may be concisely specified using inference rules, which may be thus seen as high-level definitions of ``model checkers'' for the logic given. Heuristics for simplifying ABTAs are also given, as are experimental results in the CWB-NC verification tool suggesting that, despite the generic ABTA basis, our approach can perform better than model checkers targeted for specific logics. The ABTA-based approach we advocate simplifies the retargeting of model checkers to different logics, and it also allows the use of ``compile-time'' simplifications on ABTAs that improves model-checker performance.

R. Cleaveland and O. Sokolsky.
Equivalence and Preorder Checking for Finite-State Systems.
In J. Bergstra, A. Ponse and S. Smolka, editors, Handbook of Process Algebra, chapter 6, pages 391-424. North-Holland, Amsterdam, 2001.
©2001 North-Holland.

This chapter surveys algorithms for computing semantic equivalences and refinement relations, or preorders, over states in finite-state labeled transitions systems. Methods for calculating a general equivalence, namely bisimulation equivalence, and a general preorder are described and shown to be useful as a basis for calculating other semantic relations as well. Two general classes of algorithms are considered: global ones, which require the a priori construction of the state space but are generally more efficient in the asymptotic case, and local, or on-the-fly ones, which avoid the construction of unnecessary states while incurring some additional computational overhead.

R. Cleaveland, G. Lüttgen and V. Natarajan.
Priority in Process Algebra.
In J. Bergstra, A. Ponse and S. Smolka, editors, Handbook of Process Algebra, chapter 12, pages 711-765. North-Holland, Amsterdam, 2001.
©2001 North-Holland.

This chapter surveys the semantic ramifications of extending traditional process algebras with notions of priority that allow some transitions to be given precedence over others. The need for these enriched formalisms arises when one wishes to model system features such as interrupts, prioritized choice, or real-time behavior.

Approaches to priority in process algebras can be classified according to whether the induced notion of pre-emption on transitions is global or local and whether priorities are static or dynamic. Early work in the area concentrated on global pre-emption and static priorities and led to formalisms for modeling interrupts and aspects of real-time, such as maximal progress, in centralized computing environments. More recent research has investigated localized notions of pre-emption in which the distribution of systems is taken into account, as well as dynamic priority approaches. The latter allows priority values to change as systems evolve and enables an efficient encoding of real-time semantics.

Technically, this chapter studies the different models of priorities by presenting extensions of Milner's Calculus of Communicating Systems (CCS) with static and dynamic priority as well as with notions of global and local pre-emption. For each extension, the operational semantics of CCS is modified appropriately, behavioral theories based on strong and weak bisimulation are given, and related approaches for different process-algebraic settings are discussed.

D. Hansel, R. Cleaveland and S. Smolka.
Distributed Prototyping from Validated Specifications.
In 12th IEEE International Workshop on Rapid System Prototyping, pages 97-102, Monterey, California, June 2001. IEEE Computer Society Press.
©2001 IEEE.

We present vpl2cxx, a translator that automatically generates efficient, fully distributed C++ code from high-level system designs specified in the mathematically rigorous VPL design language. The Concurrency Workbench of the New Century (CWB-NC) verification tool includes a front end for VPL, and this means designers may use the full range of automatic verification and simulation checks provided by the tool before invoking the translator, thereby generating distributed prototypes from validated specifications. Besides being fully distributed, the code generated by \verb+vpl2cxx+ is highly readable and portable to a host of execution environments and real-time operating systems (RTOSes). This is achieved by encapsulating all generated code dealing with low-level interprocess communication issues in a library for synchronous communication, which in turn is built upon the ACE client-server network programming interface. Finally, benchmarks show that the performance of the generated code is more than acceptable for a distributed prototype. We discuss one such example in the RETHER real-time ethernet protocol for voice and video applications.

Note: A journal version subsumes this paper.

L. Tan and R. Cleaveland.
Simulation Revisited.
In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of Lecture Notes in Computer Science, pages 480-495, Genoa, April 2001. Springer-Verlag.
©2001 Springer-Verlag.

This paper develops an efficient algorithm for determining when one system is capable of simulating the behavior of another. The method combines an iterative algorithm for computing behavioral preorders with an algorithm that simultaneously computes the bisimulation equivalence classes of the systems in question. Experimental data indicate that the new routine dramatically outperforms the best-known algoritm for computing simulation, even when the systems are minimized with respect to bisimulation before the simulation algorithm is invoked.

A. Philippou, O. Sokolsky, I. Lee, R. Cleaveland, and S. Smolka.
Hiding Resources That Can Fail: An Axiomatic Perspective.
Information Processing Letters 80(1):3-13, October 2001.
©2001 Elsevier.

In earlier work, we presented a process algebra, PACSR, that uses a notion of resource failure to capture probabilistic behavior in reactive systems. PACSR also supports an operator for resource hiding. In this paper, we carefully consider the interaction hbetween these two features from an axiomatic perspective. For this purpose, we introduce a subset of PACSR, called ``PACSR-lite,'' that allows us to isolate the semantic issues surrounding resource hiding in a probabilistic setting, and we provide a sound and complete axiomatization of strong bisimulation for this fragment.

S. Sims, R. Cleaveland, K. Butts, and S. Ranville.
Automated Validation of Software Models.
16th International Conference on Automated Software Engineering, pages 91-96, Coronado Island, California, November 2001. IEEE Computer Society Press.
©2001 IEEE.

This paper describes the application of an automated verification tool to a software model developed at Ford. Ford already has in place an advanced model-based software development framework that employs the Matlab®, Simulink® and Stateflow® modeling tools. During this project we applied the invariant checker Salsa to a Simulink® / Stateflow® model of automotive software to check for nondeterminism, missing cases, dead code, and redundant code. During the analysis, a number of anomalies were detected that had not been found during manual review. We argue that the detection and correction of these problems demonstrates a cost-effective application of formal verification that elevates our level of confidence in the model.

Rance Cleaveland
Last modified: Fri May 14 15:31:48 EDT 2004