Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2021)

Stepwise development supported by the Event-B formalism has been used in the domain of system design and verification. This refinement approach guarantees that safety properties are preserved with Event-B proof obligations, while additional reasoning and fairness assumptions are required to prove the transformation of liveness properties in Event-B models. This paper presents a new proof-based approach that integrates Linear Temporal Logic (LTL) and Event-B for reasoning about the refinement of liveness properties. We first developed an extended version of LTL that could be used in Event-B models with three basic atomic propositions: state-related propositions, event-related propositions, and enabledness of events. Then we employed this extended LTL to express four important temporal properties with Event-B proof obligations and fairness assumptions. Besides the typical Event-B proof obligations, we specified conditions such as relative deadlock freeness, conditional convergence, and fairness assumptions to allow temporal properties to be transformed during refinement steps. The generic fairness-based refinement strategies were developed to replace or strengthen the fairness assumptions in the refinement steps of Event-B models. A reliable retransmission example is used to illustrate the approach.