{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T17:19:50Z","timestamp":1779124790464,"version":"3.51.4"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2015,8,4]],"date-time":"2015-08-04T00:00:00Z","timestamp":1438646400000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2017,4]]},"DOI":"10.1007\/s10009-015-0394-x","type":"journal-article","created":{"date-parts":[[2015,8,3]],"date-time":"2015-08-03T09:03:34Z","timestamp":1438592614000},"page":"247-269","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Rigorous development process of a safety-critical system: from ASM models to Java code"],"prefix":"10.1007","volume":"19","author":[{"given":"Paolo","family":"Arcaini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,8,4]]},"reference":[{"key":"394_CR1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B: System and Software Engineering, 1st edn. Cambridge University Press, New York, NY, USA (2010)","edition":"1"},{"key":"394_CR2","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Proceedings of the 2nd International Conference on Abstract State Machines, Alloy, B and Z (ABZ 2010), volume 5977 of Lecture Notes in Computer Science, pages 61\u201374. Springer (2010)","DOI":"10.1007\/978-3-642-11811-1_6"},{"key":"394_CR3","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Automatic Review of Abstract State Machines by Meta-Property Verification. In: Mu\u00f1oz, C. (ed.) Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA\/CP-2010-216215, pp. 4\u201313. NASA (2010)"},{"key":"394_CR4","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: CoMA: Conformance monitoring of Java programs by Abstract State Machines. In: Khurshid, S., Sen, K. (eds.) Runtime Verification volume 7186 of Lecture Notes in Computer Science, pp. 223\u2013238. Springer (2012)","DOI":"10.1007\/978-3-642-29860-8_17"},{"key":"394_CR5","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Combining model-based testing and runtime monitoring for program testing in the presence of nondeterminism. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, Workshops Proceedings, Luxembourg, March 18-22, 2013, pp. 178\u2013187. IEEE (2013)","DOI":"10.1109\/ICSTW.2013.29"},{"key":"394_CR6","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Modeling and Analyzing Using ASMs: The Landing Gear System Case Study. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study volume 433 of Communications in Computer and Information Science, pp. 36\u201351. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_3"},{"key":"394_CR7","doi-asserted-by":"crossref","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Offline Model-Based Testing and Runtime Monitoring of the Sensor Voting Module. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study volume 433 of Communications in Computer and Information Science, pp. 95\u2013109. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_7"},{"key":"394_CR8","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Using SMT for dealing with nondeterminism in ASM-based runtime verification. ECEASST 70 (2014)"},{"key":"394_CR9","first-page":"155","volume":"41","author":"P Arcaini","year":"2011","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw.: Pract. Exp. 41, 155\u2013166 (2011)","journal-title":"Softw.: Pract. Exp."},{"key":"394_CR10","doi-asserted-by":"crossref","unstructured":"Banach, R.: The Landing Gear Case Study in Hybrid Event-B. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study volume 433 of Communications in Computer and Information Science, pp. 126\u2013141. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_9"},{"issue":"3","key":"394_CR11","doi-asserted-by":"crossref","first-page":"199","DOI":"10.1016\/S0164-1212(02)00041-9","volume":"65","author":"M Barnett","year":"2003","unstructured":"Barnett, M., Schulte, W.: Runtime verification of NET contracts. J. Syst. Softw. 65(3), 199\u2013208 (2003)","journal-title":"J. Syst. Softw."},{"key":"394_CR12","doi-asserted-by":"crossref","unstructured":"Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Trans. Softw. Method. (TOSEM) 20 (2011)","DOI":"10.1145\/2000799.2000800"},{"key":"394_CR13","doi-asserted-by":"crossref","unstructured":"Berthomieu, B., Dal\u00a0Zilio, S., Fronc, \u0141.: Model-Checking Real-Time Properties of an Aircraft Landing Gear System Using Fiacre. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 110\u2013125. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_8"},{"key":"394_CR14","doi-asserted-by":"crossref","unstructured":"Boniol, F., Wiels, V.: The Landing Gear System Case Study. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 1\u201318. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_1"},{"key":"394_CR15","doi-asserted-by":"crossref","unstructured":"Boniol, F., Wiels, V., Ameur, Y.A., Schewe, K.-D.: ABZ 2014: The Landing Gear Case Study Case Study Track, Held at the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z Toulouse, France, June 2-6, 2014, Proceedings. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9"},{"key":"394_CR16","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1007\/s00165-003-0012-7","volume":"15","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: The ASM refinement method. Form. Aspects Comput. 15, 237\u2013257 (2003)","journal-title":"Form. Aspects Comput."},{"key":"394_CR17","unstructured":"B\u00f6rger, E.: The ASM method for system design and analysis. A tutorial introduction. In: Gramlich, B. (ed.) Proceedings of Frontiers of Combining Systems, 5th International Workshop, FroCoS 2005, Vienna, Austria, September 19-21, 2005, volume 3717 of Lecture Notes in Computer Science, pp. 264\u2013283. Springer (2005)"},{"key":"394_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"E B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Berlin Heidelberg (2003)"},{"key":"394_CR19","doi-asserted-by":"crossref","unstructured":"Carioni, A., Gargantini, A., Riccobene, E., Scandurra, P.: A Scenario-Based Validation Language for ASMs. In: Proceedings of the 1st International Conference on Abstract State Machines, B and Z (ABZ 2008), volume 5238 of Lecture Notes in Computer Science, pp. 71\u201384. Springer-Verlag (2008)","DOI":"10.1007\/978-3-540-87603-8_7"},{"key":"394_CR20","doi-asserted-by":"crossref","unstructured":"Chen, F., D\u2019Amorim, M., Ro\u015fu, G.: A formal monitoring-based framework for software development and analysis. In: Davies, J., Schulte, W., Barnett, M. (eds.) Formal Methods and Software Engineering, volume of 3308 LNCS, pp. 357\u2013372. Springer, Berlin \/ Heidelberg (2004)","DOI":"10.1007\/978-3-540-30482-1_31"},{"key":"394_CR21","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge, MA, USA (1999)"},{"key":"394_CR22","doi-asserted-by":"crossref","unstructured":"Dausend, M., Raschke, A.: Introducing Aspect-Oriented Specification for Abstract State Machines. In: Ait\u00a0Ameur, Y., Schewe, K.-D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, volume 8477 of Lecture Notes in Computer Science, pp. 174\u2013187. Springer Berlin Heidelberg (2014)","DOI":"10.1007\/978-3-662-43652-3_15"},{"key":"394_CR23","unstructured":"Dausend, M., Stegmaier, M., Raschke, A.: Debugging Abstract State Machine Specifications: An Extension of CoreASM. In: Mazzanti, F., Trentanni, G. (eds.) Proceedings of iFM 2012 & ABZ 2012 - Posters & Tool demos Session, pp. 21\u201325 (2012)"},{"issue":"12","key":"394_CR24","doi-asserted-by":"crossref","first-page":"859","DOI":"10.1109\/TSE.2004.91","volume":"30","author":"N Delgado","year":"2004","unstructured":"Delgado, N., Gates, A.Q., Roach, S.: A taxonomy and catalog of runtime software-fault monitoring tools. IEEE Trans. Softw. Eng. 30(12), 859\u2013872 (2004)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"394_CR25","doi-asserted-by":"crossref","unstructured":"Dhaussy, P., Teodorov, C.: Context-Aware Verification of a Landing Gear System. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 52\u201365. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_4"},{"key":"394_CR26","unstructured":"Falcone, Y., Havelund, K., Reger, G.: A Tutorial on Runtime Verification. In: Engineering Dependable Software Systems, volume\u00a034 of NATO Science for Peace and Security Series\u2014D: Information and Communication Security, pp. 141\u2013175. IOS Press (2013)"},{"issue":"2","key":"394_CR27","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1002\/spe.1029","volume":"41","author":"R Farahbod","year":"2011","unstructured":"Farahbod, R., Gl\u00e4sser, U.: The CoreASM modeling framework. Softw., Pract. Exp. 41(2), 167\u2013178 (2011)","journal-title":"Softw., Pract. Exp."},{"key":"394_CR28","first-page":"262","volume":"7","author":"A Gargantini","year":"2001","unstructured":"Gargantini, A., Riccobene, E.: ASM-based testing: coverage criteria and automatic test sequence generation. J. Univ. Comput. Sci. 7, 262\u2013265 (2001)","journal-title":"J. Univ. Comput. Sci."},{"key":"394_CR29","doi-asserted-by":"crossref","unstructured":"Gargantini, A., Riccobene, E., Rinzivillo, S.: Using Spin to Generate Tests from ASM Specifications. In: B\u00f6rger, E., Gargantini, A., Riccobene, E. (eds.) Abstract State Machines 2003, volume of 2589 Lecture Notes in Computer Science, pp. 263\u2013277. Springer, Berlin Heidelberg (2003)","DOI":"10.1007\/3-540-36498-6_15"},{"issue":"12","key":"394_CR30","first-page":"1949","volume":"14","author":"A Gargantini","year":"2008","unstructured":"Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for abstract state machines. J. Univ. Comput. Sci. 14(12), 1949\u20131983 (2008)","journal-title":"J. Univ. Comput. Sci."},{"issue":"9","key":"394_CR31","first-page":"74","volume":"3","author":"U Gl\u00e4sser","year":"2013","unstructured":"Gl\u00e4sser, U., Hallerstede, S., Leuschel, M., Riccobene, E.: Integration of tools for rigorous software construction and analysis (Dagstuhl Seminar 13372). Dagstuhl Rep. 3(9), 74\u2013105 (2013)","journal-title":"Dagstuhl Rep."},{"key":"394_CR32","doi-asserted-by":"crossref","unstructured":"Hansen, D., Ladenberger, L., Wiegard, H., Bendisposto, J., Leuschel, M.: Validation of the ABZ Landing Gear System Using ProB. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study volume 433 of Communications in Computer and Information Science, pp. 66\u201379.Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_5"},{"issue":"4","key":"394_CR33","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1002\/1099-1689(200012)10:4<201::AID-STVR214>3.0.CO;2-Z","volume":"10","author":"R Hierons","year":"2000","unstructured":"Hierons, R., Derrick, J.: Editorial: special issue on specification-based testing. Softw. Test. Verif. Reliab. 10(4), 201\u2013202 (2000)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"394_CR34","doi-asserted-by":"crossref","unstructured":"Kossak, F.: Landing Gear System: An ASM-Based Solution for the ABZ Case Study. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 142\u2013147. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_10"},{"key":"394_CR35","volume-title":"AspectJ in Action: Practical Aspect-Oriented Programming","author":"R Laddad","year":"2003","unstructured":"Laddad, R.: AspectJ in Action: Practical Aspect-Oriented Programming. Manning Publications Co., Greenwich, CT, USA (2003)"},{"key":"394_CR36","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1007\/s11334-009-0096-1","volume":"5","author":"H Liang","year":"2009","unstructured":"Liang, H., Dong, J., Sun, J., Wong, W.: Software monitoring through formal specification animation. Innov. Syst. Soft. Eng. 5, 231\u2013241 (2009)","journal-title":"Innov. Syst. Soft. Eng."},{"key":"394_CR37","doi-asserted-by":"crossref","unstructured":"Mammar, A., Laleau, R.: Modeling a Landing Gear System in Event-B. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 80\u201394. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_6"},{"key":"394_CR38","doi-asserted-by":"crossref","unstructured":"M\u00e9ry, D., Singh, N.\u00a0K.: Modeling an Aircraft Landing System in Event-B. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.-D., (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 154\u2013159. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_12"},{"issue":"11","key":"394_CR39","first-page":"952","volume":"7","author":"G Schellhorn","year":"2001","unstructured":"Schellhorn, G.: Verification of ASM refinements using generalized forward simulation. J. Univ. Comput. Sci. 7(11), 952\u2013979 (2001)","journal-title":"J. Univ. Comput. Sci."},{"issue":"12","key":"394_CR40","first-page":"1984","volume":"14","author":"A Slissenko","year":"2008","unstructured":"Slissenko, A., Vasilyev, P.: Simulation of timed abstract state machines with predicate logic model-checking. J. Univ. Comput. Sci. 14(12), 1984\u20132006 (2008)","journal-title":"J. Univ. Comput. Sci."},{"key":"394_CR41","doi-asserted-by":"crossref","unstructured":"St\u00e4rk, R.F., Schmid, J., B\u00f6rger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer (2001)","DOI":"10.1007\/978-3-642-59495-3"},{"key":"394_CR42","doi-asserted-by":"crossref","unstructured":"Su, W., Abrial, J.-R.: Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System. In: Boniol, F., Wiels, V., Ait\u00a0Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014: The Landing Gear Case Study, volume 433 of Communications in Computer and Information Science, pp. 19\u201335. Springer International Publishing (2014)","DOI":"10.1007\/978-3-319-07512-9_2"},{"key":"394_CR43","volume-title":"Practical Model-Based Testing: A Tools Approach","author":"M Utting","year":"2006","unstructured":"Utting, M., Legeard, B.: Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann, San Francisco, CA (2006)"},{"issue":"4","key":"394_CR44","doi-asserted-by":"crossref","first-page":"19:1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1\u201319:36 (2009)","journal-title":"ACM Comput. Surv."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0394-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-015-0394-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0394-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-015-0394-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,19]],"date-time":"2022-05-19T21:32:04Z","timestamp":1652995924000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-015-0394-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,8,4]]},"references-count":44,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2017,4]]}},"alternative-id":["394"],"URL":"https:\/\/doi.org\/10.1007\/s10009-015-0394-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,8,4]]}}}