{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,21]],"date-time":"2026-02-21T19:44:52Z","timestamp":1771703092759,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642245589","type":"print"},{"value":"9783642245596","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-24559-6_38","type":"book-chapter","created":{"date-parts":[[2011,10,21]],"date-time":"2011-10-21T15:13:17Z","timestamp":1319209997000},"page":"569-584","source":"Crossref","is-referenced-by-count":1,"title":["Refining Nodes and Edges of State Machines"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Hallerstede","sequence":"first","affiliation":[]},{"given":"Colin","family":"Snook","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"38_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. In: CUP (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"38_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. In: CUP (2010)","DOI":"10.1017\/CBO9781139195881"},{"issue":"6","key":"38_CR3","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":"38_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"K.R. Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of Sequential and Concurrent Programs. Springer, Heidelberg (2009)"},{"issue":"3","key":"38_CR5","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/s00165-008-0070-y","volume":"21","author":"R.-J. Back","year":"2009","unstructured":"Back, R.-J.: Invariant based programming: basic approach and teaching experiences. Formal Asp. Comput.\u00a021(3), 227\u2013244 (2009)","journal-title":"Formal Asp. Comput."},{"key":"38_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-17071-3_5","volume-title":"Formal Methods for Components and Objects","author":"A.S. Fathabadi","year":"2010","unstructured":"Fathabadi, A.S., Butler, M.: Applying Event-B Atomicity Decomposition to a Multi Media Protocol. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol.\u00a06286, pp. 89\u2013104. Springer, Heidelberg (2010)"},{"key":"38_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-642-11811-1_21","volume-title":"Abstract State Machines, Alloy, B and Z","author":"S. Hallerstede","year":"2010","unstructured":"Hallerstede, S.: Structured Event-B Models and Proofs. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 273\u2013286. Springer, Heidelberg (2010)"},{"key":"38_CR8","unstructured":"Hallerstede, S., Leuschel, M.: Experiments in Program Verification using Event-B. In: Formal Asp. Comput. (to appear, 2011)"},{"key":"38_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/978-3-642-11811-1_22","volume-title":"Abstract State Machines, Alloy, B and Z","author":"S. Hallerstede","year":"2010","unstructured":"Hallerstede, S., Leuschel, M., Plagge, D.: Refinement-Animation for Event-B \u2014 Towards a Method of Validation. In: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol.\u00a05977, pp. 287\u2013301. Springer, Heidelberg (2010)"},{"key":"38_CR10","volume-title":"Programming: The Derivation of Algorithms","author":"A. Kaldewaij","year":"1990","unstructured":"Kaldewaij, A.: Programming: The Derivation of Algorithms. Prentice-Hall, Englewood Cliffs (1990)"},{"key":"38_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"274","DOI":"10.1007\/978-3-540-27815-3_23","volume-title":"Algebraic Methodology and Software Technology","author":"A. Knapp","year":"2004","unstructured":"Knapp, A., Merz, S., Wirsing, M.: Refining Mobile UML State Machines. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 274\u2013288. Springer, Heidelberg (2004)"},{"key":"38_CR12","doi-asserted-by":"crossref","unstructured":"Lano, K., Clark, D.: Semantics and Refinement of Behavior State Machines. In: Filipe, J., Cordeiro, J. (eds.) Enterprise Information Systems. LNBIP, vol.\u00a019, pp. 42\u201349. Springer, Heidelberg (2009)","DOI":"10.5220\/0001683700420049"},{"key":"38_CR13","volume-title":"Programming from Specifications","author":"C.C. Morgan","year":"1994","unstructured":"Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)","edition":"2"},{"key":"38_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/978-3-642-05089-3_37","volume-title":"FM 2009: Formal Methods","author":"M.Y. Said","year":"2009","unstructured":"Said, M.Y., Butler, M.J., Snook, C.F.: Language and tool support for class and state machine refinement in UML-B. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 579\u2013595. Springer, Heidelberg (2009)"},{"issue":"3","key":"38_CR15","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1002\/stvr.349","volume":"16","author":"A.J.H. Simons","year":"2006","unstructured":"Simons, A.J.H.: A theory of regression testing for behaviourally compatible object types. Softw. Test, Verif. Reliab.\u00a016(3), 133\u2013156 (2006)","journal-title":"Softw. Test, Verif. Reliab."},{"key":"38_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/11955757_15","volume-title":"B 2007: Formal Specification and Development in B","author":"C. Snook","year":"2006","unstructured":"Snook, C., Wald\u00e9n, M.: Refinement of statemachines using event B semantics. In: Julliand, J., Kouchnarenko, O. (eds.) B 2007. LNCS, vol.\u00a04355, pp. 171\u2013185. Springer, Heidelberg (2006)"},{"issue":"1","key":"38_CR17","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C.F. Snook","year":"2006","unstructured":"Snook, C.F., Butler, M.J.: UML-B: Formal modeling and design aided by UML. ACM Trans. Softw. Eng. Methodol.\u00a015(1), 92\u2013122 (2006)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"38_CR18","unstructured":"Snook, C.: Exploring the Barriers to Formal Specification. PhD thesis, Electronics and Computer Science, University of Southampton (2002)"},{"issue":"4","key":"38_CR19","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1145\/362575.362577","volume":"14","author":"N. Wirth","year":"1971","unstructured":"Wirth, N.: Program development by stepwise refinement. CACM\u00a014(4), 221\u2013227 (1971)","journal-title":"CACM"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24559-6_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T04:59:08Z","timestamp":1741841948000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24559-6_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642245589","9783642245596"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24559-6_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}