A fairness-based refinement strategy to transform liveness properties in Event-B models

Alur, 2020 Lamport, 1977, Proving the correctness of multiprocess programs, IEEE Trans. Softw. Eng., SE-3, 125, 10.1109/TSE.1977.229904 van Glabbeek, 2019, Ensuring liveness properties of distributed systems: open problems, J. Log. Algebraic Methods Program., 109 Ostroff, 1999, Composition and refinement of discrete real-time systems, ACM Trans. Softw. Eng. Methodol., 8, 1, 10.1145/295558.295560 Tassey, 2002 Clarke, 1996, Formal methods, ACM Comput. Surv., 28, 626, 10.1145/242223.242257 Méry, 2015, Towards an integrated formal method for verification of liveness properties in distributed systems: with application to population protocols, Softw. Syst. Model., 16, 1083, 10.1007/s10270-015-0504-y Leuschel, 2003, Prob: a model checker for b, 855 Zhu, 2021, Reasoning about real-time systems in Event-B models with fairness assumptions, 143 Butler, 2016, Reasoned modelling with Event-B, 51 Hoang, 2010 Zhu, 2018, Semantics of real-time trigger-response properties in Event-B, 150 Zhu, 2019, Towards refinement semantics of real-time trigger-response properties in Event-B, 1 Back, 1989, Refinement calculus, Part II: Parallel and reactive programs, 67 Abrial, 2009 Jastram, 2014 Zhu, 2020, Trace semantics and refinement patterns for real-time properties in Event-B models, Sci. Comput. Program., 197, 10.1016/j.scico.2020.102513 Pnueli, 1977, The temporal logic of programs, 46 Manna, 1989, A hierarchy of temporal properties (invited paper, 1990), 377 K. Robinson, System modelling & design using Event-B, the University of New South Wales, Recuperado en agosto de 2012. Devlin, 1979 Hoang, 2016, Foundations for using linear temporal logic in Event-B refinement, Form. Asp. Comput., 28, 909, 10.1007/s00165-016-0376-0 Abadi, 1991, The existence of refinement mappings, Theor. Comput. Sci., 82, 253, 10.1016/0304-3975(91)90224-P Alur, 1995, Local liveness for compositional modeling of fair reactive systems, 166 Williams, 2012, Model checking under fairness in ProB and its application to fair exchange protocols, 168 Hoang, 2009, Event-B patterns and their tool support, 456 Schneider, 2014, Managing LTL properties in Event-B refinement, 221 KM, 1988 Hudon, 2013, Systems design guided by progress concerns, 16 Abadi, 1994, An old-fashioned recipe for real time, ACM Trans. Program. Lang. Syst., 16, 1543, 10.1145/186025.186058