Automatic Verification Methods for Finite State Systems

We present here two software tools, Auto and Autograph. Both originated directly from the basic theory of process calculi. Both were experimented on well-known problems to enhance their accordance to users expectations.Auto is a verification tool for process terms with finite automata representation. It computes minimal normal forms along a variety of user parameterized semantics, including some taking into account partial observation and abstraction. It checks for bisimulation equivalence (on the normal forms), and allows powerful diagnostics methods in case of failure.Autograph is a graphical, non syntactic system for manipulation of process algebraic terms as intuitively appealing drawings. It allows graphical editing by the user, but also visual support for display of information recovered from analysis with Auto.

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. Using 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 is an automated tool that caters for the analysis of networks of finite-state processes expressed in Milner's Calculus of Communicating Systems. Its key feature is its scope: 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 examples involving the verification of communications protocols and mutual exclusion algorithms and has proven a valuable aid in teaching and research.

The Argonaute system is specifically designed to describe, specify and verify reactive systems such as communication protocols, real-time applications, man-machine interfaces, ... It is based upon the Argos graphical language, whose syntax relies on the Higraphs formalism by D. Harel [HAR88], and whose semantics is given by using a process algebra. Automata form the basic notion of the language, and hierarchical or parallel decompositions are given by using operators of the algebra. The complete formalization of the language inherits notions from both classical process algebras such as ccs [MIL80], and existing programming languages used in the same field such as Esterel [BG88] or the Statecharts formalism [HAR87]. Concerning complex system description, Argos allows to describe intrinsic states directly — with the basic automation notion — and only them: connections between components need no extra-state. The Argonaute system allows to describe reactive systems graphically, to specify properties by means of temporal logic formulas, to produce a model on which logic formulas can be evaluated and to simulate an execution of the system described, by using the external graphical form to show evolutions. We present the global structure and functionalities of the Argonaute system, and the theoretical basis of the Argos language.

An interactive system for proving properties of CCS specifications is described. This system allows users to take advantage of all three views of CCS semantics (the transitions, the operationally defined equivalences and the axioms) and to define their own verification strategies for moving from one view to another. The system relies on term rewriting techniques and manipulates only the symbolic representation of specifications without resorting to any other kind of internal representation.

A method for automatic verification of trace and test equivalence between regular CCS specifications is presented. The method consists of two steps: (i) CCS specifications are transformed to deterministic, and finitely represented attributed trees, which we call test trees (TT's), and (ii) TT's are compared for verification of trace or test equivalence between the corresponding CCS specifications.

Projections of the reachability graph reduce the storage costs of the computation and support the evaluation. Secondly the specification of systems and their components is completed by restrictions to the behaviour of their environments. Components can then be analysed separately from each other, and in the analysis of a system components can be replaced by reduced substitutes. The decision of the abstract equality of indeterministic behaviours and the computation of reduced substitutes is based on the use of corresponding deterministic acceptors.

Elementary net systems, basic net-theoretic models of distributed systems, as well as their properties are represented by formulas of deterministic propositional dynamic logic. A semantic tableaux based theorem prover is used to verify the properties, i.e. to find out whether they are entailed by the representations of the systems. The theorem prover implements a simplified tableaux decision procedure, the simplifications are due to the special nature of the set of formulas representing an elementary net system.

The ACP Bisimulation Tool is an implementation of an action relation model for the algebraic process theory ACP_r.In the action relation model processes are denoted by process expressions. A transition system is associated with each process expression through a set of inductive transition rules; the semantics of the model are the transition systems modulo bisimulation equivalence.It is shown how the verification of a system property can be expressed as a bisimulation decision problem with abstraction, enabling automated proof with the ACP Bisimulation Tool. Verification of mutual exclusion is considered as an example.It is known that in ACP_r all computable processes are finitely expressible, hence all computable finite state models can be finitely represented in ACP_r. Thus a finite state process model called the Selection/Resolution model is shown to be contained in ACP_r by a translation [.] from S/R processes to ACP_r process expressions.

MEC is a tool for constructing and analysing transition systems modelizing processes and systems of communicating processes.From representations of processes by transition systems and from a representation of the interactions between the processes of a system by the set of all allowed global actions, MEC builds a transition system representing the global system of processes as the synchronized product of the component processes.Such transition systems can be checked by computing sets of states and sets of transitions verifying properties given by the user of MEC. These properties are expressed in a language allowing definitions of new logical operators as least fixed points of systems of equations; thus all properties expressed in most of the branching-time temporal logic can be expressed in this language too.MEC can handle transition systems with some hundred thousands states and transitions. Constructions of transition systems by synchronized products and computations of sets of states and transitions are performed in time linear with respect to the size of the transition system.

SMG [GB88] is a system designed to generate a finite state model of a program from the program itself and an operational semantics for the programming language. Model-checking can then be used to verify that the program satisfies a set of desired temporal properties.In this paper we first show how we have incorporated notions of fairness into SMG; in particular, a user is now able to define semantics with “fair” constructs, for example, parallel composition, repetitive choice, etc. A program may contain several fair constructs, each with its own fairness type. Secondly we describe a practical approach to model checking of linear temporal formulae over the fair-satisfiability generated by the new SMG_F. Our approach is a refinement and extension of the fair-satisfiability algorithms, presented earlier by Lichtenstein and Pnueli [LP85], together with techniques developed in our practical implementations of decision procedures for linear temporal logic [Gou84].

In this paper we show that observation equivalence on CCS processes preserves temporal properties (drawn from a very general temporal logic encompassing standard linear and branching time logics). Moreover, relative to a progress requirement, we show that CCS processes are live. But it is also very important to be able to verify that a process has or lacks a temporal property. In Section 3 we briefly discuss the idea of local model checking, checking that a particular finitary process has a property. Finally in Section 4 we exhibit a correct model checker for a sublogic, the linear time mu-calculus, of the general temporal logic.

Designs of communicating systems can be validated by checking that their behavior satisfy desirable properties expressed in a temporal logic. We describe an adaptation of a branching-time temporal logic, CTL, to which we have given a semantics in terms of sequences of communication actions. We describe a method for checking that a communicating system satisfies a formula in the logic. The method works as follows: we first transform the communicating system to conform with the standard semantics of CTL; we then use an existing algorithm for CTL with the standard semantics, for which an implementation exists in the EMC, to check that the system satisfies a formula. The method is implemented within the framework of the Concurrency Workbench.

We have described a scheme that allows timing assumptions to be incorporated into automatic proofs of arbitrary finite-state temporal properties. The obvious extension is to be able to prove timing properties, not just assume them. This would provide a verification framework for finite-state hard real-time systems. We conjecture that the method presented can, in fact, be extended in this way.Another major question is practicality. We believe that, with some simple program optimizations, the proposed method can be useful for certain small but tricky systems, such as asynchronous control circuits. For larger systems, approximate and heuristic methods will be needed.

We advocate the use of the synchronous declarative language Lustre as a unique language for specifying and programming real-time systems. Furthermore, we show that the finite automaton produced by the Lustre compiler may be used for verifying many logical properties, by model checking. The paper deals with an example program, extracted from a railways regulation system.

We present a theory of Modal Specifications which has been specifically designed in order to allow loose specifications to be expressed. Modal Specifications extends Process Algebra in the sense that specifications may be combined using process constructs. Moreover, Modal Specifications is given an operational interpretation imposing restrictions on the transitions of possible implementations by telling which transitions are necessary and which are admissable. This allows a refinement ordering between Modal Specifications to be defined extending the well-established notion of bisimulation. In the paper we present a logical characterization of the refinement-ordering and derive characteristic logical formulas from any given Modal Specifications. Also, we explore the possibility of combining Modal Specifications themselves logically, and we briefly comment on the automation of refinement.

Real-time systems occur in many safety critical applications. Automated verification of crucial system properties is therefore desirable. This paper discusses a timed transition model (TTM) for real-time systems, and summarizes recently developed procedures for automated verification of a class of temporal logic properties for finite state systems. The procedures are linear in the size of the system reachability graph. The verification procedures have been implemented in Prolog.

This report is a case study applying temporal logic to specify the operation of a bank of identical elevators servicing a number of floors in a building. The goal of the study was to understand the application of temporal logic in a problem domain that is appropriate for the method, and to determine some of the strengths and weaknesses of temporal logic in this domain. The case study uses a finite state machine language to build a model of the system specification, and verifies that the temporal logic specifications are consistent using this model. The specification aspires to be complete, consistent, and unambiguous.

Model checking is a well known method to carry out formal verification of distributed systems. This method needs a model representing the behaviour of the system to be verified. The size of this model depends on the complexity of the system. To be able to verify real life systems, it is necessary to use techniques allowing to take advantage of all the available storage space, to reduce the amount of information needed for the verification and to speed up computation time. But the expressiveness of the languages used to describe the system and its expected behaviours (properties) limit the possible reductions. We present in this paper our choices for an automatic verification tool by using model checking. The preliminary results obtained from its use for the verification of a real life protocol allow us to make some estimations about the limits of model checking methods.

PROLOG Interpreted Predicate Net (PIPN) is a software tool for the specification and analysis of communications in distributed computing systems. Labelled Predicate/Transition Nets are embedded into a logic programming environment. Executable specifications are defined by labelled transition systems. Observational equivalence and temporal logic techniques are concurrently applied.

LOTOS is a Formal Description Technique developed within ISO to specify services and protocols. This paper describes a tool for doing LOTOS to LOTOS transformations. It has applications in state exploration, deadlock detection, testing, validation and in design by stepwise refinement. The transformations are: expansion (transformation of parallelism into summation and prefix); parameterized expansion; i action removal. The transformations obtain LOTOS specifications which relate to the original one through strong (expansion and parameterized expansion) or weak (i-action removal) bisimulation congruence.

Protocol verification detects the existence of logic errors in protocol design specifications. Various verification approaches have been proposed to deal with the state space explosion problem resulting from the reachability analysis. This paper proposes a parallel protocol verification algorithm, called the Two-Phase algorithm, in an attempt to provide a maximum of verification with a minimum of state space. This algorithm allows verification for all FSMs to be executed in parallel through exploring fewer states. To quantify the reduction in state space, the paper provides the state space complexity comparison between the reachability analysis and the Two-Phase algorithm. The paper defines four protocol models giving the lower and upper bound state space complexity according to both state and channel synchronization characteristics of protocols. For each model, the state space complexity of these two verification algorithms are analyzed and compared. The Two-Phase algorithm is shown to require much smaller state space. To support the analytical result, this paper also gives experimental results on several protocols, including the Call Set-Up and Termination phases of the CCITT X.25 and X.75 protocols.

Since the beginning of time, the semantics of choice for synchronous circuits has been the finite state machine (FSM). Years of research on FSMs have provided many tools for the design and verification of synchronous hardware. But from a mathematical manipulation point of view, FSMs have several drawbacks, and a new hardware specification style based on the functional approach has gained ground recently. Earlier we described a functional semantics for synchronous circuits based on monotonic length-preserving (MLP) functions on finite strings. We have now implemented this theory inside the Boyer-Moore theorem prover, and proved correctness properties for a variety of circuits. In 1985 Paillet presented an interesting sequence of synchronous circuits of increasing "sequential complexity", with hand-proofs of their correctness in his P-calculus. Our semantics supports a calculus which extends his. It was therefore very tempting to investigate mechanical proofs of those circuits in the Boyer-Moore implementation of our theory. We present the results here.

A system that combines CTL model checking and trace theory for verifying speed-independent asynchronous circuits is described. This system is able to verify a large and useful class of liveness and fairness properties, and is able to find safety violations after examining only a small fraction of the circuit's state space in many cases. An extension has been implemented that allows the verification of circuits that are not speed-independent, but instead rely on assumptions about the relative delays of their components for correct operation. This greatly expands the class of circuits that can be automatically verified, making the verifier a more useful tool in the design of asynchronous circuits. The system is demonstrated on several fair mutual exclusion circuits, including a speed-independent version that is verified correct. It is also shown that given quite weak assumptions about the relative delays of components, the problem of designing a fair mutual exclusion circuit using a potentially unfair mutual exclusion element becomes almost trivial.

Automated theorem provers can provide substantial assistance when verifying that circuits described with Synchronized Transitions preserve invariants. To make verification practical for large circuits, Synchronized Transitions allows circuits to be described as hierarchies of subcircuits. Protocols defined for each subcircuit permit them to be verified one at a time. This localized proof technique factors the verification of a circuit into manageable pieces, making machine assisted verification both simpler and faster.

This paper presents an original method to compare two synchronous sequential machines. The method consists in a breadth first traversal of the product machine during which symbolic expressions of its observable behaviour are computed. The method uses formal manipulations on boolean functions to avoid the state enumeration and diagram construction. For this purpose, new algorithms on boolean functions represented by Typed Decision Graphs has been defined.

Consider a process M implemented as a collection of subprocesses SM_i. To certify the implementation to be correct, the collective behaviors of SM_i and the behavior of M are compared using a suitable verification criterion. In many approaches the implementation is specified structurally using operators such as ∥, hiding, and renaming while M is specified behaviorally using action prefixing and choice operators. This style is being used for hardware specification also [10, 8, 4, 3]. In this paper we address the question whether behavioral specifications can be deduced rapidly from structural specifications in the setting of a simple language HOP. We also address the question of doing the same for geometrically regular (array) structures that abound in VLSI. We present two algorithms PARCOMP, and PARCOMP-DC, report their performance, and explain the heuristics used to make them efficient.