This chapter deals with the use of two verification approaches: theorem proving and model checking. The authors focus on the Event-B method by using its associated theorem proving tool (Click_n_Prove), and on the language TLA+ by using its model checker TLC. By considering the limitation of the Event-B method to invariance properties, the authors propose to apply the language TLA+ to verify liveness properties on a software behavior. The authors extend first the expressivity and the semantics of a B model (called temporal B model) to deal with the specification of fairness and eventuality properties. Second, they give transformation rules from a temporal B model into a TLA+ module. The authors present in particular, their prototype system called B2TLA+, that they have developed to support this transformation; then they can verify these properties thanks to the model checker TLC on finite state systems. For the verification of infinite-state systems, they propose the use of the predicate diagrams. The authors illustrate their approach on a case study of a parcel sorting system.
TopIntroduction
Reactive systems are systems whose role is to maintain an ongoing interaction with their environment rather than produce some final values upon termination. Typical examples of reactive systems are Air traffic control systems, Programs controlling mechanical devices such as a train, a plane, or ongoing processes such as a nuclear reactor. Formal methods [Spivey,1988] is the term used to describe the specification and verification of these systems using mathematical and logical techniques. The main advantages of the formal approach to software construction [Dyba, Kampenes & Sjøberg, 2006; Pickard, Kitchenham & Jones, 1998; Wohlin, 2005; Wordsworth, 1987] is that, whenever applicable, it can lead to an increase of the reliability and correctness of the resulting programs by several orders of magnitude.
Several approaches for the verification of reactive systems are available, the most prominent are Algorithmic (model checking [Clarke, GRUMBERG, Jha, Lu & Veith, 2001; Clarke, Emerson & Sistla, 1986; Clarke, 1994; Clarke, 1997; Clarke, Grumberg & Peled, 1999; Kaltenbach, 1994]) and Deductive verification (theorem-proving techniques [Hoare, 1969; Dijkstra, 1975; Kaufmann & Moore, 2004; Archer, Vito & Muno, 2003; Holzmann, 2003]). These approaches are used to establish the correctness of reactive programs relative to their temporal specifications. Verifying the correctness of a program involves formulating a property to be verified using a suitable logic such as first order logic or temporal logic.
The model checking problem [Clarke, GRUMBERG, Jha, Lu & Veith, 2001; Clarke, Emerson & Sistla, 1986] involves the construction of an abstract model M, in the form of variations on finite state automata, and the construction of specification formulas ϕ, in the form of variations on temporal logic. The verification algorithm used in model checking involves exploring the set of reachable states of the model to ensure that the formula ϕ holds. It has gained popularity in industry because the verification procedure can be fully automated [Clarke, Emerson & Sistla, 1986] and counterexamples are automatically generated if the property being verified does not hold. Furthermore, model checkers rely on exhaustive state space enumeration to establish whether a property holds or doesn't hold. This approach to verification puts immediate limits on the state space of problems that can be explored by model checkers. This common problem, known as the state explosion problem, is an often cited drawback of verification by model checking.