{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:15:11Z","timestamp":1762460111128,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031172434"},{"type":"electronic","value":"9783031172441"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-17244-1_19","type":"book-chapter","created":{"date-parts":[[2022,10,9]],"date-time":"2022-10-09T19:33:23Z","timestamp":1665344003000},"page":"316-333","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Trace Refinement in\u00a0B and\u00a0Event-B"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2231-8656","authenticated-orcid":false,"given":"Sebastian","family":"Stock","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1210-5953","authenticated-orcid":false,"given":"Atif","family":"Mashkoor","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4595-1518","authenticated-orcid":false,"given":"Michael","family":"Leuschel","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3128-5427","authenticated-orcid":false,"given":"Alexander","family":"Egyed","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,10]]},"reference":[{"key":"19_CR1","volume-title":"The B-book: Assigning Programs to Meanings","author":"JR Abrial","year":"2005","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)"},{"key":"19_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"6","key":"19_CR3","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transfer 12(6), 447\u2013466 (2010). https:\/\/doi.org\/10.1007\/s10009-010-0145-y","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Riccobene, E.: Automatic refinement of ASM abstract test cases. In: 2019 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp. 1\u201310 (2019)","DOI":"10.1109\/ICSTW.2019.00025"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-540-48654-1_28","volume-title":"CONCUR \u201994: Concurrency Theory","author":"RJR Back","year":"1994","unstructured":"Back, R.J.R., von Wright, J.: Trace refinement of action systems. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 367\u2013384. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/978-3-540-48654-1_28"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-030-85248-1_12","volume-title":"Formal Methods for Industrial Critical Systems","author":"J Bendisposto","year":"2021","unstructured":"Bendisposto, J., et al.: ProB2-UI: a Java-based user interface for ProB. In: Lluch Lafuente, A., Mavridou, A. (eds.) FMICS 2021. LNCS, vol. 12863, pp. 193\u2013201. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-85248-1_12"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/BFb0027291","volume-title":"ZUM \u201997: The Z Formal Specification Notation","author":"M Butler","year":"1997","unstructured":"Butler, M.: An approach to the design of distributed systems with B AMN. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 221\u2013241. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0027291"},{"key":"19_CR8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-92711-4","volume-title":"Refinement: Semantics, Languages and Applications","author":"J Derrick","year":"2018","unstructured":"Derrick, J., Boiten, E.: Refinement: Semantics, Languages and Applications. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-319-92711-4"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/11415787_4","volume-title":"ZB 2005: Formal Specification and Development in Z and B","author":"S Dunne","year":"2005","unstructured":"Dunne, S., Conroy, S.: Process refinement in B. In: Treharne, H., King, S., Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 45\u201364. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11415787_4"},{"key":"19_CR10","unstructured":"Rodin User\u2019s Handbook. https:\/\/www3.hhu.de\/stups\/handbook\/rodin\/current\/html\/. Accessed 12 Sep 2022"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/978-3-030-18744-6_10","volume-title":"Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification","author":"T Fischer","year":"2019","unstructured":"Fischer, T., Dghyam, D.: Formal model validation through acceptance tests. In: Collart-Dutilleul, S., Lecomte, T., Romanovsky, A. (eds.) RSSRail 2019. LNCS, vol. 11495, pp. 159\u2013169. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-18744-6_10"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/978-3-642-54862-8_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Gibson-Robinson","year":"2014","unstructured":"Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 \u2014 a modern refinement checker for CSP. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187\u2013201. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_13"},{"key":"19_CR13","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. 5977, pp. 287\u2013301. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11811-1_22"},{"issue":"3","key":"19_CR14","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. Sci. Comput. Program. 78(3), 272\u2013292 (2013)","journal-title":"Sci. Comput. Program."},{"issue":"8","key":"19_CR15","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-030-48077-6_24","volume-title":"Rigorous State-Based Methods","author":"F Houdek","year":"2020","unstructured":"Houdek, F., Raschke, A.: Adaptive exterior light and speed control system. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 281\u2013301. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_24"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/978-3-030-76020-5_9","volume-title":"Logic, Computation and Rigorous Methods","author":"M Leuschel","year":"2021","unstructured":"Leuschel, M.: Spot the difference: a detailed comparison between B and Event-B. In: Raschke, A., Riccobene, E., Schewe, K.-D. (eds.) Logic, Computation and Rigorous Methods. LNCS, vol. 12750, pp. 147\u2013172. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76020-5_9"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/11576280_24","volume-title":"Formal Methods and Software Engineering","author":"M Leuschel","year":"2005","unstructured":"Leuschel, M., Butler, M.: Automatic refinement checking for B. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 345\u2013359. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11576280_24"},{"issue":"2","key":"19_CR19","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.: ProB: an automated analysis toolset for the B method. Int. J. Softw. Tools Technol. Transfer 10(2), 185\u2013203 (2008)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-030-48077-6_27","volume-title":"Rigorous State-Based Methods","author":"M Leuschel","year":"2020","unstructured":"Leuschel, M., Mutz, M., Werth, M.: Modelling and validating an automotive system in classical B and Event-B. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 335\u2013350. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_27"},{"key":"19_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-00867-2_9","volume-title":"Methods, Models and Tools for Fault Tolerance","author":"QA Malik","year":"2009","unstructured":"Malik, Q.A., Lilius, J., Laibinis, L.: Model-based testing using scenarios and Event-B refinements. In: Butler, M., Jones, C., Romanovsky, A., Troubitsyna, E. (eds.) Methods, Models and Tools for Fault Tolerance. LNCS, vol. 5454, pp. 177\u2013195. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00867-2_9"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-030-48077-6_28","volume-title":"Rigorous State-Based Methods","author":"A Mammar","year":"2020","unstructured":"Mammar, A., Frappier, M., Laleau, R.: An Event-B model of an automotive adaptive exterior light system. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 351\u2013366. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_28"},{"key":"19_CR23","doi-asserted-by":"crossref","unstructured":"Mashkoor, A., Jacquot, J.P.: Guidelines for formal domain modeling in Event-B. In: 2011 IEEE 13th International Symposium on High-Assurance Systems Engineering, pp. 138\u2013145 (2011)","DOI":"10.1109\/HASE.2011.47"},{"issue":"3","key":"19_CR24","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00766-011-0120-5","volume":"16","author":"A Mashkoor","year":"2011","unstructured":"Mashkoor, A., Jacquot, J.: Utilizing Event-B for domain engineering: a critical analysis. Requir. Eng. 16(3), 191\u2013207 (2011)","journal-title":"Requir. Eng."},{"issue":"12","key":"19_CR25","doi-asserted-by":"publisher","first-page":"2350","DOI":"10.1002\/spe.2634","volume":"48","author":"A Mashkoor","year":"2018","unstructured":"Mashkoor, A., Kossak, F., Egyed, A.: Evaluating the suitability of state-based formal methods for industrial deployment. Softw. Pract. Exp. 48(12), 2350\u20132379 (2018)","journal-title":"Softw. Pract. Exp."},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Mashkoor, A., Leuschel, M., Egyed, A.: Validation obligations: a novel approach to check compliance between requirements and their formal specification. In: 2021 IEEE\/ACM 43rd International Conference on Software Engineering: New Ideas and Emerging Results (ICSE-NIER), pp. 1\u20135 (2021)","DOI":"10.1109\/ICSE-NIER52604.2021.00009"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Snook, C., Hoang, T.S., Dghaym, D., Fathabadi, A.S., Butler, M.: Domain-specific scenarios for refinement-based methods. J. Syst. Architect. 112, 101833 (2021)","DOI":"10.1016\/j.sysarc.2020.101833"},{"key":"19_CR28","unstructured":"Snook, C., Hoang, T.S., Fathabadi, A.S., Dghaym, D., Butler, M.: Scenario checker: an Event-B tool forvalidating abstract models. In: Rodin Workshop (2021)"},{"key":"19_CR29","unstructured":"Wynne, M., Hellesoy, A., Tooke, S.: The Cucumber Book: Behaviour-driven Development for Testers and Developers. Pragmatic Bookshelf (2017)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17244-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T12:25:53Z","timestamp":1674908753000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17244-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031172434","9783031172441"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17244-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"10 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Madrid","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/maude.ucm.es\/ICFEM22\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"61","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3 invited papers (two papers and one abstract)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}