{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T16:36:50Z","timestamp":1743093410024,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540402534"},{"type":"electronic","value":"9783540448808"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-44880-2_24","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:12:53Z","timestamp":1183479173000},"page":"408-420","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Refinement Preserves PLTL Properties"],"prefix":"10.1007","author":[{"given":"Christophe","family":"Darlot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacques","family":"Julliand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olga","family":"Kouchnarenko","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,5,27]]},"reference":[{"key":"24_CR1","unstructured":"J.-R. Abrial. The B Book. Cambridge University Press \u2014 ISBN 0521-496195, 1996."},{"key":"24_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0053357","volume-title":"Second Conference on the B method","author":"J.-R. Abrial","year":"1998","unstructured":"J.-R. Abrial and L. Mussat. Introducing dynamic constraints in B. In Second Conference on the B method, volume 1393 of LNCS, pages 83\u2013128, 1998."},{"key":"24_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"230","DOI":"10.1007\/3-540-44525-0_14","volume-title":"Proc. First Int. Conf. ZB\u20192000, York, GB","author":"F. Bellegarde","year":"2000","unstructured":"F. Bellegarde, C. Darlot, J. Julliand, and O. Kouchnarenko. Reformulate dynamic properties during B refinement and forget variants and loop invariants. In Proc. First Int. Conf. ZB\u20192000, York, GB, volume 1878 of Lecture Notes in Computer Science, pages 230\u2013249. Springer-Verlag, September 2000."},{"key":"24_CR4","unstructured":"F. Bellegarde, C. Darlot, J. Julliand, and O. Kouchnarenko. How to verify LTL properties on infinite refined systems by proof and model-checking cooperation. In AVIS\u201901, March 2001."},{"key":"24_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1007\/3-540-45251-6_2","volume-title":"FME\u201901","author":"F. Bellegarde","year":"2001","unstructured":"F. Bellegarde, C. Darlot, J. Julliand, and O. Kouchnarenko. Reformulation: a way to combine dynamic properties and B refinement. In J.N. Oliveira and P. Zave, editors, FME\u201901, volume 2021 of LNCS, pages 2\u201319, Berlin, Allemagne, March 2001. Springer-Verlag."},{"key":"24_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/3-540-46428-X_19","volume-title":"FASE\u20192000","author":"F. Bellegarde","year":"2000","unstructured":"F. Bellegarde, J. Julliand, and O. Kouchnarenko. Ready-simulation is not ready to express a modular refinement relation. In FASE\u20192000, volume 1783 of LNCS, pages 266\u2013283, April 2000."},{"key":"24_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-45648-1_23","volume-title":"ZB 2002: Formal specification an development in Z and B","author":"F. Bellegarde","year":"2002","unstructured":"F. Bellegarde, J. Julliand, and O. Kouchnarenko. Synchronized parallel composition of event systems in B. In D. Bert, J. P. Bowen, M. C. Henson, and K. Robinson, editors, ZB 2002: Formal specification an development in Z and B, volume 2272 of LNCS, pages 436\u2013457. Springer-Verlag, 2002."},{"key":"24_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/3-540-40911-4_14","volume-title":"Proc. of the 2nd Int. Conf. on Integrated Formal Methods (IFM 2000)","author":"D. Bert","year":"2000","unstructured":"D. Bert and F. Cave. Construction of finite labelled transition systems from B abstract systems. In Proc. of the 2nd Int. Conf. on Integrated Formal Methods (IFM 2000), volume 1945 of LNCS, pages 235\u2013254, Dagstuhl, Germany, novembre 2000. Springer-Verlag."},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"M.J. Butler. Stepwise refinement of communicating systems. Science of Computer Programming, 1996.","DOI":"10.1016\/0167-6423(96)81173-7"},{"key":"24_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1007\/3-540-58043-3_22","volume-title":"A Decade of Concurrency","author":"Y. Kesten","year":"1994","unstructured":"Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification of simulation and refinement. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, A Decade of Concurrency, volume 803 of LNCS, pages 273\u2013346. Springer-Verlag, 1994."},{"issue":"3","key":"24_CR11","doi-asserted-by":"publisher","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L. Lamport","year":"1994","unstructured":"L. Lamport. A temporal logic of actions. ACM Transactions On Programming Languages And Systems, TOPLAS, 16(3):872\u2013923, May 1994.","journal-title":"ACM Transactions On Programming Languages And Systems, TOPLAS"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"}],"container-title":["Lecture Notes in Computer Science","ZB 2003: Formal Specification and Development in Z and B"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44880-2_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,17]],"date-time":"2023-02-17T14:19:09Z","timestamp":1676643549000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44880-2_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540402534","9783540448808"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-44880-2_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"27 May 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}