{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T17:34:32Z","timestamp":1781976872249,"version":"3.54.5"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2016,11,1]],"date-time":"2016-11-01T00:00:00Z","timestamp":1477958400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>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.<\/jats:p>","DOI":"10.1007\/s00165-016-0376-0","type":"journal-article","created":{"date-parts":[[2016,4,28]],"date-time":"2016-04-28T16:11:45Z","timestamp":1461859905000},"page":"909-935","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Foundations for using linear temporal logic in Event-B refinement"],"prefix":"10.1145","volume":"28","author":[{"given":"Thai Son","family":"Hoang","sequence":"first","affiliation":[{"name":"ECS, University of Southampton, Southampton, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Surrey, Guildford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[{"name":"Department of Computer Science, University of Surrey, Guildford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David M.","family":"Williams","sequence":"additional","affiliation":[{"name":"VU University, Amsterdam, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"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\u2013466","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01872848"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Abrial J Mussat L (1998) Introducing dynamic constraints in B. In: Bert D (ed) B\u201998: Recent Advances in the Development and Use of the B Method vol. 1393. Springer Heidelberg pp 83\u2013128","DOI":"10.1007\/BFb0053357"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Bicarregui J Arenas A Aziz B Massonet P Ponsard C (2008) Towards modelling obligations in Event-B. In: B\u00a8orger E Butler M Bowen JP Boca P (eds) Abstract state machines B and Z vol. 5238. Springer Heidelberg pp 181\u2013194","DOI":"10.1007\/978-3-540-87603-8_15"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"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\u2013September 2 2000 Proceedings volume 1878 of Lecture notes in computer science. Springer pp 230\u2013249","DOI":"10.1007\/3-540-44525-0_14"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"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\u201316 2001 Proceedings volume 2021 of Lecture notes in computer science. Springer pp 2\u201319","DOI":"10.1007\/3-540-45251-6_2"},{"key":"e_1_2_1_2_8_2","unstructured":"Butler MJ (1992) A CSP approach to action systems. Dhil thesis Oxford University"},{"key":"e_1_2_1_2_9_2","unstructured":"ClearSy (2014) Atelier B version 4.2. http:\/\/www.atelierb.eu\/en\/download-atelier-b\/. Accessed 20 Feb 2016"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Chandy M Misra J (1989) Parallel program design: a foundation. Addison-Wesley Reading Mass","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"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\u20136 2003 Proceedings pp 408\u2013420","DOI":"10.1007\/3-540-44880-2_24"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-011-0177-4"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"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\u2013124","DOI":"10.1007\/11955757_11"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Hoang TS Abrial J (2011) Reasoning about liveness properties in Event-B. In: ICFEM volume 6991 of LNCS. Springer pp 456\u2013471","DOI":"10.1007\/978-3-642-24559-6_31"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Hudon S Hoang TS (2013) Systems design guided by progress concerns. In: Integrated formal methods\u201410th International Conference on integrated formal methods (IFM2013) volume 7940 of Lecture notes in computer science. Springer-Verlag pp 16\u201330","DOI":"10.1007\/978-3-642-38613-8_2"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2011.03.005"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/PL00008921"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-007-0063-9"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"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\u2013723","DOI":"10.1007\/978-3-642-05089-3_45"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0065-0"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"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\u2013326","DOI":"10.1007\/978-1-4612-4476-9_37"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-011-0183-6"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-009-0132-3"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Puhakka A Valmari A (2001) Liveness and fairness in process-algebraic verification. In: CONCUR 2001\u2014concurrency theory 12th International Conference Aalborg Denmark August 20\u201325 2001 Proceedings pp 202\u2013217","DOI":"10.1007\/3-540-44685-0_14"},{"key":"#cr-split#-e_1_2_1_2_25_2.1","doi-asserted-by":"crossref","unstructured":"Sun J Liu Y Dong JS Wang HH (2008) Specifying and verifying event-based fairness enhanced systems. In: Formal methods","DOI":"10.1007\/978-3-540-88194-0_4"},{"key":"#cr-split#-e_1_2_1_2_25_2.2","unstructured":"and software engineering 10th International Conference on formal engineering methods ICFEM 2008 Kitakyushu-City Japan October 27-31 2008. Proceedings pp 5-24"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-012-0265-0"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Schneider S Treharne H Wehrheim H Williams D (2014) Managing LTL properties in Event-B refinement. arXiv:1406.6622 IFM2014 June","DOI":"10.1007\/978-3-319-10181-1_14"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Schneider S Treharne H Wehrheim H Williams DM (2014) Managing LTL properties in event-b refinement. In: Integrated formal methods\u201411th International Conference IFM 2014 Bertinoro Italy September 9\u201311 2014 Proceedings volume 8739 of Lecture notes in computer science. Springer pp 221\u2013237","DOI":"10.1007\/978-3-319-10181-1_14"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"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\u2013182","DOI":"10.1007\/978-3-642-32943-2_14"},{"key":"e_1_2_1_2_30_2","unstructured":"Zurich ETH et\u00a0al (2014) Rodin version 3.1.0. http:\/\/www.event-b.org\/. Accessed 20 Feb 2016"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0376-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0376-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0376-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0376-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:04:43Z","timestamp":1641485083000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0376-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,11]]},"references-count":31,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2016,11]]}},"alternative-id":["10.1007\/s00165-016-0376-0"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0376-0","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,11]]}}}