{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,12]],"date-time":"2025-11-12T13:41:30Z","timestamp":1762954890327},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642118104"},{"type":"electronic","value":"9783642118111"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-11811-1_14","type":"book-chapter","created":{"date-parts":[[2010,2,19]],"date-time":"2010-02-19T06:57:22Z","timestamp":1266562642000},"page":"174-188","source":"Crossref","is-referenced-by-count":47,"title":["Supporting Reuse in Event B Development: Modularisation Approach"],"prefix":"10.1007","author":[{"given":"Alexei","family":"Iliasov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elena","family":"Troubitsyna","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Linas","family":"Laibinis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander","family":"Romanovsky","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kimmo","family":"Varpaaniemi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dubravka","family":"Ilic","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Timo","family":"Latvala","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"14_CR1","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1145\/151646.151649","volume":"15","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Lamport, L.: Composing Specifications. ACM Transactions on Programming Languages and Systems\u00a015(1), 73\u2013132 (1993)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"14_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-Book","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)"},{"key":"14_CR3","first-page":"169","volume-title":"Proceedings of 1st Conference on the B Method","author":"J.-R. Abrial","year":"1996","unstructured":"Abrial, J.-R.: Extending B without Changing it. In: Proceedings of 1st Conference on the B Method, Nantes, France, November 1996, pp. 169\u2013191. Springer, Heidelberg (1996)"},{"issue":"1-2","key":"14_CR4","first-page":"1","volume":"77","author":"J.-R. Abrial","year":"2007","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, decomposition, and instantiation of discrete models: Application to event-b. Fundam. Inf.\u00a077(1-2), 1\u201328 (2007)","journal-title":"Fundam. Inf."},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-52559-9_61","volume-title":"Stepwise Refinement of Distributed Systems","author":"R. Back","year":"1990","unstructured":"Back, R.: Refinement calculus, Part II: Parallel and reactive programs. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol.\u00a0430, pp. 67\u201393. Springer, Heidelberg (1990)"},{"issue":"3","key":"14_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01214918","volume":"8","author":"R. Back","year":"1996","unstructured":"Back, R., Sere, K.: Superposition refinement of reactive systems. Formal Aspects of Computing\u00a08(3), 1\u201323 (1996)","journal-title":"Formal Aspects of Computing"},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Butler, M.: Decomposition Structures for Event-B. In: Integrated Formal Methods (2009)","DOI":"10.1007\/978-3-642-00255-7_2"},{"key":"14_CR8","unstructured":"Factsheet: BepiColombo. ESA Media Center, Space Science (15.01.2008), \n                    \n                      http:\/\/www.esa.int\/esaSC\/SEMNEM3MDAF_0_spk.html"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Fitzgerald, J.: Modularity in Model-oriented Formal Specifications and its Interaction with Formal Reasoning. University of Manchester, Ph.D. Thesis (1991)","DOI":"10.1007\/978-1-4471-3864-8_6"},{"key":"14_CR10","doi-asserted-by":"publisher","first-page":"564","DOI":"10.1145\/357114.357119","volume":"2","author":"D. Gries","year":"1981","unstructured":"Gries, D., Levin, G.: Assignment and Procedure Call Proof Rules. ACM Transactions on Programming Language Systems\u00a02, 564\u2013579 (1981)","journal-title":"ACM Transactions on Programming Language Systems"},{"key":"14_CR11","unstructured":"Industrial deployment of system engineering methods providing high dependability and productivity (DEPLOY). IST FP7 project, \n                    \n                      http:\/\/www.deploy-project.eu\/"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/BF00264276","volume":"20","author":"A.J. Martin","year":"1983","unstructured":"Martin, A.J.: A General Proof Rule for Procedures in Predicate Transformer Semantics. Acta Informatica\u00a020, 301\u2013313 (1983)","journal-title":"Acta Informatica"},{"key":"14_CR13","unstructured":"OBSW formal development in Event B, \n                    \n                      http:\/\/deploy-eprints.ecs.soton.ac.uk\/view\/type\/rodin=5Farchive.html"},{"key":"14_CR14","unstructured":"Poppleton, M.: Decomposition Structures for Event-B. In: Proc. of ABZ 2008: Int. Conference on ASM, B and Z, London September 16-18 (2008)"},{"key":"14_CR15","unstructured":"Rigorous Open Development Environment for Complex Systems (RODIN). Deliverable D7, Event B Language, \n                    \n                      http:\/\/rodin.cs.ncl.ac.uk\/"},{"key":"14_CR16","unstructured":"RODIN modularisation plug-in. Documentation, \n                    \n                      http:\/\/wiki.event-b.org\/index.php\/Modularisation_Plug-in"},{"key":"14_CR17","unstructured":"Space Engineering: Ground Systems and Operations Telemetry and Telecommand Packet Utilization, ECSS-E-70-41A. ECSS Secretariat (30.01.2003), \n                    \n                      http:\/\/www.ecss.nl\/"},{"key":"14_CR18","unstructured":"The RODIN platform, \n                    \n                      http:\/\/rodin-b-sharp.sourceforge.net\/"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B and Z"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-11811-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T13:43:47Z","timestamp":1558273427000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-11811-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642118104","9783642118111"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-11811-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}