B. D. Barradas-h.-r, « Proof obligations for specification and refinement of liveness properties under weak fairness, 2005.

F. Bellegarde, J. J. Darlot-c, and . Kouchnarenko-o, Reformulate Dynamic Properties during B Refinement and Forget Variants and Loop Invariants, Lecture Notes in Computer Science, vol.1878, pp.230-245, 2000.
DOI : 10.1007/3-540-44525-0_14

. Lam and . L. Lamport, « The Temporal Logic of Actions, 1991.

. Lam and . L. Lamport, Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers, 2002.