- 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.

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

**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