Proving Reachability in B using Substitution Refinement

AbstractThis 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