Proof obligations for specification and refinement of liveness properties under weak fairness

Simple item page
dc.creatorBarradas, Hector Ruiz
dc.creatorBert, Didier
dc.date2005-02-09
dc.date.accessioned2026-07-07T03:22:31Z
dc.date.available2026-07-07T03:22:31Z
dc.descriptionIn 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.
dc.identifierhttps://arxiv.org/abs/cs/0502046
dc.identifierhttp://arxiv.org/abs/cs/0502046
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/32624
dc.subjectLogic in Computer Science
dc.subjectACM: F3.1
dc.titleProof obligations for specification and refinement of liveness properties under weak fairness
dc.typetext

Files

Collections

arXiv