Software model checking.

*(English)*Zbl 0989.68093
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, 309-355 (2001).

Summary: We review the automata-theoretic verification method and propositional linear temporal logic, with specific emphasis on their potential application to distributed software verification.

An important issue in software verification is the establishment of a formal relation between the concrete, implementation-level, software application and the abstract, derived, automata-model that is the subject of the actual verification. In principle one can either attempt to derive an implementation from a verified abstract model, using refinement techniques, or one can attempt to derive a verification model from an implementation, using systematic abstraction techniques. The former method has long been advocated, but has not received much attention in industrial practice.

The latter method, deriving abstract models from concrete implementations guided by explicitly stated correctness requirements, has recently begun to show considerable promise. We discuss it in detail.

For the entire collection see [Zbl 0972.00060].

An important issue in software verification is the establishment of a formal relation between the concrete, implementation-level, software application and the abstract, derived, automata-model that is the subject of the actual verification. In principle one can either attempt to derive an implementation from a verified abstract model, using refinement techniques, or one can attempt to derive a verification model from an implementation, using systematic abstraction techniques. The former method has long been advocated, but has not received much attention in industrial practice.

The latter method, deriving abstract models from concrete implementations guided by explicitly stated correctness requirements, has recently begun to show considerable promise. We discuss it in detail.

For the entire collection see [Zbl 0972.00060].

##### MSC:

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

68N01 | General topics in the theory of software |