Taming the infinite: Verification of infinite-state reactive systems by finitary means.

*(English)*Zbl 0989.68092
Hoare, Tony (ed.) et al., Engineering theories of software construction. Proceedings of the NATO ASI, Marktoberdorf, Germany, July 25 - August 6, 2000. Amsterdam: IOS Press. NATO Sci. Ser. III, Comput. Syst. Sci. 180, 261-299 (2001).

Summary: These lecture notes present a set of techniques for the verification of reactive systems. We concentrate on the case of infinite-states systems and the application of algorithmic approaches for their verification.

After introducing the computational model of Fair Discrete Systems (FDS) and the specification language of (linear) temporal logic we describe the canonic algorithmic approach to the verification of finite-state FDS’s: model checking, first in its explicit-state version and then in its symbolic version. Then we move to the main theme of the lectures, which shows how infinite-state systems can be verified by algorithmic methods.

Two such methods are presented: a) Network Invariants – All but a small number of processes (the kernel processes) in a parameterized system are abstracted into a single process which captures their relevant behavior as an environment to the kernel processes. b) Predicate Abstraction – We define a joint abstraction of a system and its temporal specification in a “safe” way which guarantees that if the abstracted system satisfies its abstracted specification, then so does the original system. In the case that the abstracted system turns out to be finite-state, the abstract verification can be performed by model checking.

For the entire collection see [Zbl 0972.00060].

After introducing the computational model of Fair Discrete Systems (FDS) and the specification language of (linear) temporal logic we describe the canonic algorithmic approach to the verification of finite-state FDS’s: model checking, first in its explicit-state version and then in its symbolic version. Then we move to the main theme of the lectures, which shows how infinite-state systems can be verified by algorithmic methods.

Two such methods are presented: a) Network Invariants – All but a small number of processes (the kernel processes) in a parameterized system are abstracted into a single process which captures their relevant behavior as an environment to the kernel processes. b) Predicate Abstraction – We define a joint abstraction of a system and its temporal specification in a “safe” way which guarantees that if the abstracted system satisfies its abstracted specification, then so does the original system. In the case that the abstracted system turns out to be finite-state, the abstract verification can be performed by model checking.

For the entire collection see [Zbl 0972.00060].

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |