Methods and Tools for the Verification of

Infinite State Systems

AIM AND SCOPE

The aim of this school is to assemble researchers and graduate students interested in the verification of infinite state systems.

In the last few years many different approaches to this problem have emerged. The purpose of the school is to give an overview of the state of the art of current research directions, specially focusing on:

Results concerning models and verification methods for systems having a dense state space such as real-time and hybrid systems, as well as for systems with an infinite but discrete state space such as Petri Nets and automata extended with unbounded data domains (queues, counters, ...).

Current trends on the development of verification methods and tools seeking the extension and the combination of algorithmic and deductive analysis techniques looking for trade-offs between efficiency and generality.

The school is organized by VERIMAG and sponsored by the Institut d'Etudes Scientifiques Avancees (IESA) of Grenoble. It will take place immediately before the International Workshop on Hybrid and Real-Time Systems HART'97.

PROGRAM

(no abstract)

In a trace-based world, the modular specification, verification, and control of live systems require each module to be receptive; that is, each module must be able to meet its liveness assumptions no matter how the other modules behave. For example, physical realizability, assume-guarantee reasoning about live trace inclusion, and controller synthesis for live trace inclusion all depend on the receptiveness condition. In a real-time world, liveness is automatically present in the form of diverging time. The receptiveness condition, then, translates to the requirement that a module must be able to let time diverge no matter how the environment behaves.

In the first part of the talk, we study the receptiveness condition for real-time systems by extending the model of reactive modules to timed and hybrid modules. We define the receptiveness of such a module as the existence of a winning strategy in a coBüchi game of the module against its environment: the module wins iff in every zeno trajectory, the module only finitely often prevents time from advancing (and thus, the environment is to be blamed for causing the convergence of the trajectory). By solving the game on region graphs, we present an (optimal) Exptime algorithm for checking the receptiveness of propositional timed modules. By giving a fixpoint characterization of the game, we present a symbolic procedure for checking the receptiveness of linear hybrid modules. This leads to an assume-guarantee principle for reasoning about timed and hybrid modules, and a method for synthesizing receptive controllers of timed and hybrid modules.

In the second part of the talk, we focus on a specific strategy for hierarchical verification that is implemented in the verifier COSPAN. Receptiveness is enforced by restrictions on the syntax. Modular and compositional rules are used to decompose the task of verifying that the implementation refines its specification. To check each individual subtask, we require the user to provide a mapping between states of the two modules, and then algorithmically verify that the mapping preserves timed behaviors. We illustrate this strategy on examples that are otherwise intractable.

(no abstract)

(no abstract)

In this lecture, we present an overview of various expressivity, decidability, and complexity results concerning the problem of deciding equivalences within various classes of automata, focussing on the various techniques exploited in each case.

A recently popular approach presents in a unified way different classes of simple infinite state processes like Context Free processes, Pushdown Automata, Petri Nets and others. We check the expressive power of the different classes up to bisimulation and Upton language equivalence.

Most techniques for the verification of concurrent systems proceed by an exhaustive traversal of the state space. Therefore, they are inherently incapable of considering systems with infinitely many states.

Recently, some methods have been developed to overcome this limitation, at least for restricted classes of infinite-state systems. Using them, several verification problems have been shown to be decidable, and even tractable. These decidability and complexity results can be classified into two groups:

results on the equivalence problem: given two infinite-state systems, are they equal with respect to a certain equivalence notion?

results on the model-checking problem: given an infinite-state system and a property expressed in a certain temporal logic, does the system satisfy the property?

In his tutorial at this School, Faron Moller surveys some of the most relevant results of the first group. He restricts his attention to infinite-state systems having a discrete state space. The purpose of this paper is to give a similar overview of the results of the second group.

The model-checking problem has two parameters: a family of systems, and a temporal logic used to express properties of their behaviour. Following Moller's tutorial (who takes this idea from Caucal), we consider families of transition systems defined by rewrite rules including sequential rewrite transition systems, like pushdown automata and Basic Process Algebra processes, and parallel rewrite transition systems, like Petri nets and Basic Parallel Processes. Temporal logics are classified according to their linear-time or branching-time character, and to their expressive power.

In their tutorials at this School, Javier Esparza and Faron Moller give a survey about model checking und equivalence checking for infinite state systems. The purpose of this tutorial is to give an intuitive account of the second-order approach to infinite state model checking. In contrast to the usual iterative model checking approaches, which compute the set of formulas that are satisfied by a certain state, second order model checking iteratively computes a property transformer for each process pattern of the finite process representation. These property transformers can then simply be applied to solve the model-checking problem, yielding an overall algorithm of acceptable complexity.

We will illustrate the second order approach by successively extending a basic algorithm, covering context-free processes and the alternation free modal $\mu$-calculus to a version for regular graphs and the full modal $\mu$-calculus.

Boundedness, coverability, quasi-liveness, regularity, liveness, reachability, bisimulation and, more generally, model-cheking against a temporal logic play a central role for the verification of infinite-state systems. A lot of these properties may be decided by computing and by using a fine regular approximation of the reachability tree. For example, boundedness, coverability, quasi-liveness and regularity problems can be decided with the coverability tree whose set of nodes is a regular set; the coverability tree approximates (covers) the reachability tree of a Petri net. Model-checking of a Timed Automaton is achieved with a finite graph of regions. Analysis of systems of Communicating Finite State Machines (CFSMs) can be done by computing a (may be infinite) regular minimal coverability tree.

There are at least two different approaches for attacking the verification problem of infinite-state systems. One approach is to look for decidability results and for algorithms which solve particular verification problems for some particular classes of infinite-state systems. This may lead to nice theoretical results but not necessarly to efficacious tools: the considered infinite-state systems are not always satisfying for the modelling and the complexity of algorithms often is enormous. The second approach is to search semi-algorithms which sometimes terminate when applied on real examples. One may obtain good practical results but the reasons of success (or unsuccess) remain unclear. The talk takes into account these two approaches and it shows the connections and the differences between both. We propose to see verification semi-algorithms as a first step for designing verification algorithms and also as natural extensions of well-known verification algorithms for undecidable models.

To be able to design verification semi-algorithms for general infinite-state transition systems, one of the first things to do is to find the hypothesis which insure the possibility to compute an approximation of the reachability tree. Monotone transition systems allows to define semi-algorithms solving (when they terminate) finite termination and boundedness. When monotone transition systems have the regular-repetitive property, it is shown that coverability, quasi-liveness and regularity become partially analysable. Moreover, we show how to construct a regular approximation (sometimes an exact representation) of the reachability tree. All Petri nets, some high-level Petri nets and systems of CFSMs are monotone with the regular-repetitive property.

The second part of the talk presents other general hypothesis allowing to obtain decidability results. Two classes of well-structured systems are introduced. One key property of well-structured transition systems is the existence of a monotone well-ordering on the reachability tree which permits to stop previous semi-algorithms and to build new algorithms. The termination of the coverability tree algorithm is shown for well-structured systems of type (1), hence, the boundedness problem is decidable. The reachability problem is decidable for well-structured systems of type (2). Applications of the theory of well-structured systems to different classes of CFSMs are presented.

(no abstract)

Starting with the observation that many verification problems can be reduced to deciding various forms of state reachability, this talk then examines how the latter can be done in the context of infinite state systems. It identifies the central problem to be solved as computing, in a way that can generate an infinite number of states in a finite amount of time, the fixpoint of the (forwards or backwards) transition relation of the program to be analyzed. Doing this requires three basic components: a finite representation for infinite sets of states together with the algorithms for manipulating it; a technique for bootstrapping from finite to infinite sets of states; and a termination criterion. For the first component, its is shown that regular sets play a central role. For the second, a variety of techniques are discussed, but one, the "loop-first search", is emphasized. For the third, it is argued that termination detection is sufficient and that termination guarantee offers little additional practical advantage beyond a theoretical illusory peace of mind.

(no abstract)

(no abstract)

(no abstract)

Deductive modelchecking allows modelchecking of infinite-state systems, by means of transformations on falsification diagrams, justified by deductive methods.

A falsification diagram is a graph that embeds a superset of all computations of a system that satisfy the negation of the specification. This diagram is refined using transformations that preserve system computations; many of these transformations can be applied automatically, until a counterexample is found, or until the set of computations embedded in the diagram is empty, showing that the system satisfies the specification.

Like standard modelchecking, our procedure does not require user provided auxiliary formulas (except for well-founded orders), and allows the construction of counterexamples; the process is guided by the search for such computations. Like deductive methods, it only needs to check local conditions, and allows the verification of infinite-state systems through the use of symbolic representations to describe sets of states (e.g. first-order formulas). We also accomodate the use previously established invariants and simple temporal properties.

Even when the modelchecking effort is not completed, the resulting falsification diagram can be used to restrict the search for a counterexample in testing.

We will present the procedure, illustrated with examples, and discuss its relationship to modelchecking and deductive methods, in particular verification diagrams.

Decision procedures are vital components in a number of mechanized verification systems. PVS is one such verification system. Its decision procedures include simplifiers for equality, arithmetic, and boolean simplification, and model checkers for finite-state verification. These individual decision procedures are most useful when integrated into a deductive framework where they are used to automate the individual steps in a proof. This presentation will serve as an introduction to the PVS approach to deductive verification. It will describe:
1. Shostak's approach to obtaining decision procedures for combinations of ground theories.
2. The integration of these decision procedures in an interactive verifier.
3. The integration of symbolic model checking.
4. Examples illustrating the use of decision procedures in the verification of finite and infinite-state systems.
The talk will be of an introductory nature but will assume a basic background in logic and verification. More information regarding PVS can be obtained from the web site: http://www.csl.sri.com/sri-csl-pvs.html.

To specify and verify distributed real-time systems, a formal framework has been developed based on Hoare triples (precondition, program, postcondition). This framework has been applied to a number of case studies, such as a chemical batch processing system, a distributed real-time arbitration protocol, and a mine pump system. Although these examples have been verified manually, it became clear that for more complex applications some form of mechanical support is indispensable.
Therefore we have experimented with the use of the tool PVS (Prototype Verification System) during the design of distributed real-time systems. Our formal framework has been formulated in the specification language of PVS, a higher-order typed logic, with many built-in types including booleans, integers, reals, sets, lists, and records.
To be able to represent design steps formally, our formalism has been adapted to be able to mix specifications and programming constructs freely. Using the proof checker of PVS, proofs can be constructed interactively and rerun automatically after small changes. The resulting PVS framework has been applied to several examples, including the RPC-Memory specification problem, part of the ACCESS.bus protocol, and a steam boiler control system.

``Group communication services'', as provided by systems like Isis, Horus, and Transis, are becoming widely accepted as building blocks for the construction of fault-tolerant distributed applications. An important special case is a ``virtually synchronous'' group communication service, which allows different ``views'' of the current group membership to become established, which associates every message with a particular view, and which maintains a consistent ordering of messages within the same view at different locations. Such a service can be implemented even in the presence of unpredictable process and communication link failures and recoveries. It appears to provide suitable communication support for many fault-tolerant applications, for example, replicated data management and load balancing.

One problem is that there is no consensus among system designers and researchers about exactly what a virtually synchronous group communication service is supposed to guarantee! Many different formal specifications have been proposed so far, most of which are quite complicated. However, we believe that a clear and simple specification is needed if such a service is to become an effective practical building block.

This talk presents a new, simple specification for a virtually synchronous group communication service. This specification separates basic correctness properties from performance and fault-tolerance properties. The usefulness of this specification is demonstrated by showing how it can be used in some applications. All system components are modelled as input/output automata, and all application-level correctness, performance and fault-tolerance properties are stated and proved formally.

The proof methods used are a combination of compositional methods, invariant assertions, simulation relations, and operation reasoning (for performance and fault-tolerance).

Based on joint work with Alan Fekete and Alex Shvartsman.

(no abstract)

TRAVEL INFORMATION

Train: From Paris, the fast TGV train departs from Gare de Lyon several times a day and reaches Grenoble within 3 hours.

Plane: The airports of Lyon (Satolas) and Geneva (Cointrin) are served by most major airlines. From Lyon-Satolas you can take a shuttle bus to Grenoble (one hour), from Geneva-Cointrin you can take a train to Grenoble (3 hours). Grenoble Airport (Saint Geoirs) is served mostly by local flights, and from there you can take a bus to Grenoble (40mn).

Inside Grenoble: Tram tickets are bought using automatic machines at the stations (some machines do not give change). Tickets cost 7.5 francs each or 51 francs for ten tickets. They can be used in trams and buses within one hour after the first usage, but only in the same direction.

ACCOMMODATION

We propose three hotels in downtown Grenoble. All the rooms are All the prices include breakfast.

REGISTRATION FEES

Before December 10, 1996	1500 FF
After December 10, 1996	1700 FF

They include attendance to all sessions, a copy of proceedings, banquet, lunches and coffee breaks. Click here for the registration form.

For further information contact:

Chantal Costes
Verimag
Centre Equation
2, av. de Vignate
38610 Gières, France
Phone: +33 (0) 476 63 48 47
Fax: +33 (0) 476 63 48 50

Last modified: March 6, 1997.
Added abstracts: March 20, 1997. (bls)