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).
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.
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.
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.
We present
Note: A journal version subsumes this paper.
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.
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.
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.