Software Model Checking

Abstract

In thes notes we will review the automata-theoretic verification method and propo-sitional linear temporal logic, with specific emphasis on their potential application to dis-tributed 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 refine-ment techniques, or one can attempt to derive a verification model from an implementa-tion, using systematic abstraction techniques. The former method has long been advo-cated, 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 prom-ise. We will discuss it in detail.