Proving reachability in B using substitution refinement

This paper proposes an approach to prove reachability properties of the form AG(ψEFφ) using substitution refinement in classical B. Such properties denote that there exists an execution path for each state satisfying ψ to a state satisfying φ. These properties frequently occur in security policies and information systems. We show how to use Morgan s specification statement to represent a property and refinement laws to prove it. The idea is to construct by stepwise refinement a program whose elementary statements are operation calls. Thus, the execution of such a program provides an execution satisfying AG(ψ⇒EFφ). Proof obligations are represented using assertions (ASSERTIONS clause of B) and can be discharged using Atelier B.