Abstract
In this paper we present a new way of reconciling Event-B refinement with linear temporal logic (LTL) properties. In particular, the results presented in this paper allow properties to be established for abstract system models, and identify conditions to ensure that the properties (suitably translated) continue to hold as those models are developed through refinement. There are several novel elements to this achievement: (1) we identify conditions that allow LTL properties to be mapped across refinement chains; (2) we provide translations of LTL predicates to reflect the introduction through refinement of new events and the renaming and splitting of existing events; (3) we do this for an extended version of LTL particularly suited to Event-B, including state predicates and enabledness of events, which can be model-checked at the abstract level. Our results are more general than any previous work in this area, covering liveness in the context of anticipated events, and relaxing constraints between adjacent refinement levels. The approach is illustrated with a case study. This enables designers to develop event based models and to consider their execution patterns so that liveness and fairness properties can be verified for Event-B systems.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abrial J, Butler MJ, Hallerstede S, Hoang TS, Mehta F, Voisin L (2010) Rodin: an open toolset for modelling and reasoning in Event-B. STTT 12(6):447–466
Abrial J-R (2010) Modeling in Event-B: system and software engineering. Cambridge University Press, Cambridge
Apt KR, Francez N, Katz S (1988) Appraising fairness in languages for distributed programming. Distrib Comput 2(4): 226–241
Abrial J, Mussat L (1998) Introducing dynamic constraints in B. In: Bert D (ed) B’98: Recent Advances in the Development and Use of the B Method, vol. 1393. Springer, Heidelberg, pp 83–128
Bicarregui J, Arenas A, Aziz B, Massonet P, Ponsard C (2008) Towards modelling obligations in Event-B. In: B¨orger E, Butler M, Bowen JP, Boca P (eds) Abstract state machines, B and Z, vol. 5238. Springer, Heidelberg, pp 181–194
Bellegarde F, Darlot C, Julliand J, Kouchnarenko O (2000) Reformulate dynamic properties during B refinement and forget variants and loop invariants. In: Bowen JP, Dunne S, Galloway A, King S (eds) ZB 2000: Formal specification and development in Z and B. First International Conference of B and Z Users, York, UK, August 29–September 2, 2000, Proceedings, volume 1878 of Lecture notes in computer science. Springer, pp 230–249
Bellegarde F, Darlot C, Julliand J, Kouchnarenko O (2001) Reformulation: a way to combine dynamic properties and B refinement. In: Oliveira JN, Zave P (eds) FME 2001: Formal methods for increasing software productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12–16, 2001, Proceedings, volume 2021 of Lecture notes in computer science. Springer, pp 2–19
Butler MJ (1992) A CSP approach to action systems. Dhil thesis, Oxford University
ClearSy (2014) Atelier B version 4.2. http://www.atelierb.eu/en/download-atelier-b/. Accessed 20 Feb 2016
Chandy M, Misra J (1989) Parallel program design: a foundation. Addison-Wesley, Reading, Mass
Darlot C, Julliand J, Kouchnarenko O (2003) Refinement preserves PLTL properties. In: ZB 2003: Formal specification and development in Z and B, Third International Conference of B and Z Users, Turku, Finland, June 4–6, 2003, Proceedings, pp 408–420
Derrick J, Smith G (2012) Temporal-logic property preservation under Z refinement. Form Asp Comput 24(3): 393–416
Groslambert J (2006) Verification of LTL on B event systems. In: B 2007: Formal specification and development in B, volume 4355 of LNCS. Springer, pp 109–124
Hoang TS, Abrial J (2011) Reasoning about liveness properties in Event-B. In: ICFEM, volume 6991 of LNCS. Springer, pp 456–471
Hudon S, Hoang TS (2013) Systems design guided by progress concerns. In: Integrated formal methods—10th International Conference on integrated formal methods (IFM2013), volume 7940 of Lecture notes in computer science. Springer-Verlag, pp 16–30
Hallerstede S, Leuschel M, Plagge D (2013) Validation of formal models by refinement animation. Sci Comput Program 78(3): 272–292
Lamport L (2000) Fairness and hyperfairness. Distrib Comput 13(4): 239–245
Leuschel M, Butler MJ (2008) ProB: an automated analysis toolset for the B method. STTT 10(2): 185–203
Leuschel M, Falampin J, Fritz F, Plagge D (2009) Automated property verification for large scale B models. In: FM, volume 5850 of LNCS. Springer, pp 708–723
Lowe G (2008) Specification of communicating processes: temporal logic versus refusals-based refinement. Form Asp Comput 20(3): 277–294
Morgan CC (1990) Of wp and CSP. In: Feijen WHJ et al (eds) Beauty is our business: a birthday salute to E. W. Dijkstra. Springer, New York, pp 319–326
Murray TC (2013) On the limits of refinement-testing for model-checking CSP. Form Asp Comput 25(2): 219–256
Plagge D, Leuschel M (2010) Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. STTT 12(1): 9–21
Puhakka A, Valmari A (2001) Liveness and fairness in process-algebraic verification. In: CONCUR 2001—concurrency theory, 12th International Conference, Aalborg, Denmark, August 20–25, 2001, Proceedings, pp 202–217
Sun J, Liu Y, Dong JS,Wang HH (2008) Specifying and verifying event-based fairness enhanced systems. In: Formal methods and software engineering, 10th International Conference on formal engineering methods, ICFEM 2008, Kitakyushu-City, Japan, October 27–31, 2008. Proceedings, pp 5–24
Schneider S, Treharne H, Wehrheim H (2014) The behavioural semantics of Event-Brefinement. Form Asp Comput 26(2): 251–280
Schneider S, Treharne H, Wehrheim H, Williams D (2014) Managing LTL properties in Event-B refinement. arXiv:1406.6622, IFM2014, June
Schneider S, Treharne H, Wehrheim H, Williams DM (2014) Managing LTL properties in event-b refinement. In: Integrated formal methods—11th International Conference, IFM 2014, Bertinoro, Italy, September 9–11, 2014, Proceedings, volume 8739 of Lecture notes in computer science. Springer, pp 221–237
Williams DM, de Ruiter J, Fokkink W (2012) Model checking under fairness in ProB and its application to fair exchange protocols. In ICTAC, volume 7521 of LNCS. Springer, pp 168–182
Zurich ETH et al (2014) Rodin version 3.1.0. http://www.event-b.org/. Accessed 20 Feb 2016
Author information
Authors and Affiliations
Corresponding author
Additional information
Michael Butler
Rights and permissions
Open Access This article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.
About this article
Cite this article
Hoang, T.S., Schneider, S., Treharne, H. et al. Foundations for using linear temporal logic in Event-B refinement. Form Asp Comp 28, 909–935 (2016). https://doi.org/10.1007/s00165-016-0376-0
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-016-0376-0