Proof obligations for specification and refinement of liveness properties under weak fairness
Barradas, Hector Ruiz · Bert, Didier
Original · EN
In this report, we present a formal model of fair iteration of events for B event systems. The model is used to justify proof obligations for basic liveness properties and preservation under refinement of general liveness properties. The model of fair iteration of events uses the dovetail operator, an operator proposed by Broy and Nelson to model fair choice. The proofs are mainly founded in fixpoint calculations of fair iteration of events and weakest precondition calculus.
English translation
This paper has no Arabic translation yet. Be the first: it takes a few seconds, and the result is stored for every future reader.