{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,21]],"date-time":"2026-08-21T17:57:16Z","timestamp":1787335036569,"version":"build-2736575974"},"publisher-location":"Cham","reference-count":17,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319101804","type":"print"},{"value":"9783319101811","type":"electronic"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10181-1_14","type":"book-chapter","created":{"date-parts":[[2014,8,29]],"date-time":"2014-08-29T10:28:38Z","timestamp":1409308118000},"page":"221-237","source":"Crossref","is-referenced-by-count":6,"title":["Managing LTL Properties in Event-B Refinement"],"prefix":"10.1007","author":[{"given":"Steve","family":"Schneider","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helen","family":"Treharne","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David M.","family":"Williams","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"issue":"6","key":"14_CR2","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J.-R. Abrial","year":"2010","unstructured":"Abrial, J.-R., Butler, M.J., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. STTT\u00a012(6), 447\u2013466 (2010)","journal-title":"STTT"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0053357","volume-title":"B\u201998: Recent Advances in the Development and Use of the B Method","author":"J.-R. Abrial","year":"1998","unstructured":"Abrial, J.-R., Mussat, L.: Introducing dynamic constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol.\u00a01393, pp. 83\u2013128. Springer, Heidelberg (1998)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"360","DOI":"10.1007\/3-540-47884-1_20","volume-title":"Integrated Formal Methods","author":"H. Barradas","year":"2002","unstructured":"Barradas, H., Bert, D.: Specification and proof of liveness properties under fairness assumptions in B event systems. In: Butler, M., Petre, L., Sere, K. (eds.) IFM 2002. LNCS, vol.\u00a02335, pp. 360\u2013379. Springer, Heidelberg (2002)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-540-87603-8_15","volume-title":"Abstract State Machines, B and Z","author":"U. Feige","year":"2008","unstructured":"Feige, U., Arenas, A.E., Aziz, B., Massonet, P., Ponsard, C.: Towards modelling obligations in event-B. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 181\u2013194. Springer, Heidelberg (2008)"},{"key":"14_CR6","unstructured":"Butler, M.J.: A CSP approach to Action Systems. DPhil thesis, Oxford U. (1992)"},{"issue":"3","key":"14_CR7","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/s00165-011-0177-4","volume":"24","author":"J. Derrick","year":"2012","unstructured":"Derrick, J., Smith, G.: Temporal-logic property preservation under Z refinement. Formal Asp. Comput.\u00a024(3), 393\u2013416 (2012)","journal-title":"Formal Asp. Comput."},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/11955757_11","volume-title":"B 2007: Formal Specification and Development in B","author":"J. Groslambert","year":"2006","unstructured":"Groslambert, J.: Verification of LTL on B Event Systems. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 109\u2013124. Springer, Heidelberg (2006)"},{"issue":"3","key":"14_CR9","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/j.scico.2011.03.005","volume":"78","author":"S. Hallerstede","year":"2013","unstructured":"Hallerstede, S., Leuschel, M., Plagge, D.: Validation of formal models by refinement animation. Science of Computer Programming\u00a078(3), 272\u2013292 (2013)","journal-title":"Science of Computer Programming"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/978-3-642-24559-6_31","volume-title":"Formal Methods and Software Engineering","author":"T.S. Hoang","year":"2011","unstructured":"Hoang, T.S., Abrial, J.-R.: Reasoning about liveness properties in Event-B. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol.\u00a06991, pp. 456\u2013471. Springer, Heidelberg (2011)"},{"issue":"2","key":"14_CR11","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/s10009-007-0063-9","volume":"10","author":"M. Leuschel","year":"2008","unstructured":"Leuschel, M., Butler, M.J.: ProB: an automated analysis toolset for the B method. STTT\u00a010(2), 185\u2013203 (2008)","journal-title":"STTT"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1007\/978-3-642-05089-3_45","volume-title":"FM 2009: Formal Methods","author":"M. Leuschel","year":"2009","unstructured":"Leuschel, M., Falampin, J., Fritz, F., Plagge, D.: Automated property verification for large scale B models. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 708\u2013723. Springer, Heidelberg (2009)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Morgan, C.: Of wp and CSP. Beauty is our business: a birthday salute to E. W. Dijkstra, pp. 319\u2013326 (1990)","DOI":"10.1007\/978-1-4612-4476-9_37"},{"issue":"1","key":"14_CR14","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-009-0132-3","volume":"12","author":"D. Plagge","year":"2010","unstructured":"Plagge, D., Leuschel, M.: Seven at one stroke: LTL model checking for high-level specifications in B, Z, CSP, and more. STTT\u00a012(1), 9\u201321 (2010)","journal-title":"STTT"},{"issue":"2","key":"14_CR15","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s00165-012-0265-0","volume":"26","author":"S. Schneider","year":"2014","unstructured":"Schneider, S., Treharne, H., Wehrheim, H.: The behavioural semantics of Event-B refinement. Formal Asp. Comput.\u00a026(2), 251\u2013280 (2014)","journal-title":"Formal Asp. Comput."},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Schneider, S., Treharne, H., Wehrheim, H., Williams, D.: Managing LTL properties in Event-B refinement. arXiv:1406:6622 (June 2014)","DOI":"10.1007\/978-3-319-10181-1_14"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-642-32943-2_14","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2012","author":"D.M. Williams","year":"2012","unstructured":"Williams, D.M., de Ruiter, J., Fokkink, W.: Model checking under fairness in ProB and its application to fair exchange protocols. In: Roychoudhury, A., D\u2019Souza, M. (eds.) ICTAC 2012. LNCS, vol.\u00a07521, pp. 168\u2013182. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10181-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,14]],"date-time":"2023-02-14T16:09:31Z","timestamp":1676390971000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-10181-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319101804","9783319101811"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10181-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}