Reasoning About Real-Time Systems in Event-B Models with Fairness Assumptions

Stepwise-based 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, while additional reasoning is required to prove liveness properties. Our previous work proposes to use real-time trigger-response properties to reason about liveness properties and timed properties in real-time systems. Conditions such as weak fairness assumptions, relative deadlock freedom, and conditional convergence are explored to eliminate Zeno behavior when modeling real-time systems. In this reasoning framework, the response events are required not to be disabled by other events. This paper extends our previous results by using strong fairness assumptions to relax the constraints on response events. Refinement rules and strategies are also developed to refine real-time systems in the form of trace semantics and LTL operators with fairness assumptions. A simplified bounded re-transmission protocol case study is used to illustrate the approach