Top

Published in:

2021 | OriginalPaper | Chapter

The ASMETA Approach to Safety Assurance of Software Systems

Authors : Paolo Arcaini, Andrea Bombarda, Silvia Bonfanti, Angelo Gargantini, Elvinia Riccobene, Patrizia Scandurra

Published in: Logic, Computation and Rigorous Methods

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Safety-critical systems require development methods and processes that lead to provably correct systems in order to prevent catastrophic consequences due to system failure or unsafe operation. The use of models and formal analysis techniques is highly demanded both at design-time, to guarantee safety and other desired qualities already at the early stages of the system development, and at runtime, to address requirements assurance during the system operational stage.

In this paper, we present the modeling features and analysis techniques supported by ASMETA (ASM mETAmodeling), a set of tools for the Abstract State Machines formal method. We show how the modeling and analysis approaches in ASMETA can be used during the design, development, and operation phases of the assurance process for safety-critical systems, and we illustrate the advantages of integrated use of tools as that provided by ASMETA.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter What is the Natural Abstraction Level of an Algorithm?

next chapter Flashix: Modular Verification of a Concurrent and Crash-Safe Flash File System

Repository https://github.com/asmeta/asmeta/tree/master/asm_examples.

Note that $x denotes the variable x in the AsmetaL notation.

A Java annotation is a meta-data tag that permits to add information to code elements (class declarations, method declarations, etc.). Annotations are defined similarly as classes.

Al-Shareefi, F.: Analysing Safety-Critical Systems and Security Protocols with Abstract State Machines. Ph.D. thesis, University of Liverpool (2019)

Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 80–89. IEEE, September 2015. https://doi.org/10.1109/MEMCOD.2015.7340473

Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Integrating formal methods into medical software development: the ASM approach. Sci. Comput. Program. 158, 148–167 (2018). https://doi.org/10.1016/j.scico.2017.07.003CrossRef

Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E.: Visual notation and patterns for abstract state machines. In: Milazzo, P., Varró, D., Wimmer, M. (eds.) Software Technologies: Applications and Foundations, pp. 163–178. Springer International Publishing, Cham (2016)CrossRef

Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: Modelling an automotive software-intensive system with adaptive features using ASMETA. In: Raschke, A., Méry, D., Houdek, F. (eds.) ABZ 2020. LNCS, vol. 12071, pp. 302–317. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-48077-6_25CrossRef

Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) ABZ 2010. LNCS, vol. 5977, pp. 61–74. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11811-1_6CrossRef

Arcaini, P., Gargantini, A., Riccobene, E.: Automatic review of Abstract State Machines by meta property verification. In: Muñoz, C. (ed.) Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215, pp. 4–13. NASA, Langley Research Center, Hampton VA 23681–2199, USA, April 2010

Arcaini, P., Gargantini, A., Riccobene, E.: CoMA: conformance monitoring of Java programs by Abstract State Machines. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp. 223–238. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29860-8_17CrossRef

Arcaini, P., Gargantini, A., Riccobene, E.: Combining model-based testing and runtime monitoring for program testing in the presence of nondeterminism. In: Proceedings of the 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops, pp. 178–187. ICSTW 2013, IEEE Computer Society, Washington, DC, USA (2013). https://doi.org/10.1109/ICSTW.2013.29

10.

Arcaini, P., Gargantini, A., Riccobene, E.: Using SMT for dealing with nondeterminism in ASM-based runtime verification. ECEASST 70, 1–15 (2014). https://doi.org/10.14279/tuj.eceasst.70.970CrossRef

11.

Arcaini, P., Gargantini, A., Riccobene, E.: SMT-based automatic proof of ASM model refinement. In: De Nicola, R., Kühn, E. (eds.) SEFM 2016. LNCS, vol. 9763, pp. 253–269. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41591-8_17CrossRef

12.

Arcaini, P., Gargantini, A., Riccobene, E.: Rigorous development process of a safety-critical system: from ASM models to Java code. Int. J. Softw. Tools Technol. Transfer 19(2), 247–269 (2015). https://doi.org/10.1007/s10009-015-0394-xCrossRef

13.

Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw. Pract. Experience 41, 155–166 (2011). https://doi.org/10.1002/spe.1019CrossRef

14.

Arcaini, P., Holom, R.-M., Riccobene, E.: ASM-based formal design of an adaptivity component for a Cloud system. Formal Aspects Comput. 28(4), 567–595 (2016). https://doi.org/10.1007/s00165-016-0371-5MathSciNetCrossRefMATH

15.

Arcaini, P., Mirandola, R., Riccobene, E., Scandurra, P.: MSL: a pattern language for engineering self-adaptive systems. J. Syst. Softw. 164, 110558 (2020). https://doi.org/10.1016/j.jss.2020.110558CrossRef

16.

Arcaini, P., Riccobene, E., Scandurra, P.: Formal design and verification of self-adaptive systems with decentralized control. ACM Trans. Auton. Adapt. Syst. 11(4), 25:1-25:35 (2017). https://doi.org/10.1145/3019598CrossRef

17.

ASMETA (ASM mETAmodeling) toolset. https://asmeta.github.io/

18.

Barr, E.T., Harman, M., McMinn, P., Shahbaz, M., Yoo, S.: The oracle problem in software testing: a survey. IEEE Trans. Softw. Eng. 41(5), 507–525 (2015). https://doi.org/10.1109/TSE.2014.2372785CrossRef

19.

Benduhn, F., Thüm, T., Schaefer, I., Saake, G.: Modularization of refinement steps for agile formal methods. In: Duan, Z., Ong, L. (eds.) ICFEM 2017. LNCS, vol. 10610, pp. 19–35. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68690-5_2CrossRef

20.

Bombarda, A., Bonfanti, S., Gargantini, A.: Developing medical devices from abstract state machines to embedded systems: a smart pill box case study. In: Mazzara, M., Bruel, J.-M., Meyer, B., Petrenko, A. (eds.) TOOLS 2019. LNCS, vol. 11771, pp. 89–103. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29852-4_7CrossRef

21.

Bombarda, A., Bonfanti, S., Gargantini, A., Radavelli, M., Duan, F., Lei, Yu.: Combining model refinement and test generation for conformance testing of the IEEE PHD protocol using abstract state machines. In: Gaston, C., Kosmatov, N., Le Gall, P. (eds.) ICTSS 2019. LNCS, vol. 11812, pp. 67–85. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31280-0_5CrossRef

22.

Bonfanti, S., Gargantini, A., Mashkoor, A.: AsmetaA: animator for Abstract State Machines. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 369–373. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-91271-4_25CrossRef

23.

Bonfanti, S., Gargantini, A., Mashkoor, A.: Generation of C++ unit tests from Abstract State Machines specifications. In: 2018 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp. 185–193, April 2018. https://doi.org/10.1109/ICSTW.2018.00049

24.

Bonfanti, S., Gargantini, A., Mashkoor, A.: Design and validation of a C++ code generator from Abstract State Machines specifications. J. Softw. Evol. Process 32(2), e2205 (2020). https://doi.org/10.1002/smr.2205CrossRef

25.

Börger, E.: The ASM refinement method. Formal Aspects Comput. 15, 237–257 (2003)CrossRef

26.

Börger, E., Raschke, A.: Modeling Companion for Software Practitioners. Springer, Heidelberg (2018). https://doi.org/10.1007/978-3-662-56641-1

27.

Börger, E., Stärk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer Verlag, Heidelberg (2003). https://doi.org/10.1007/978-3-642-18216-7

28.

Calinescu, R., Weyns, D., Gerasimou, S., Iftikhar, M.U., Habli, I., Kelly, T.: Engineering trustworthy self-adaptive software with dynamic assurance cases. IEEE Trans. Softw. Eng. 44(11), 1039–1069 (2018). https://doi.org/10.1109/TSE.2017.2738640CrossRef

29.

Carioni, A., Gargantini, A., Riccobene, E., Scandurra, P.: A scenario-based validation language for ASMs. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 71–84. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87603-8_7CrossRef

30.

Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_29CrossRef

31.

Falcone, Y., Mariani, L., Rollet, A., Saha, S.: Runtime failure prevention and reaction. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 103–134. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_4CrossRef

32.

Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19(3), 215–261 (2009)CrossRef

33.

Gargantini, A., Riccobene, E.: ASM-based testing: coverage criteria and automatic test sequence. J. Univers. Comput. Sci. 7(11), 1050–1067 (2001). https://doi.org/10.3217/jucs-007-11-1050CrossRef

34.

Gargantini, A., Riccobene, E., Rinzivillo, S.: Using spin to generate tests from ASM specifications. In: Börger, E., Gargantini, A., Riccobene, E. (eds.) ASM 2003. LNCS, vol. 2589, pp. 263–277. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36498-6_15CrossRef

35.

Gargantini, A., Riccobene, E., Scandurra, P.: A semantic framework for metamodel-based languages. Autom. Softw. Eng. 16(3–4), 415–454 (2009). https://doi.org/10.1007/s10515-009-0053-0CrossRef

36.

Gargantini, A., Riccobene, E., Scandurra, P.: Ten reasons to metamodel ASMs. In: Abrial, J.-R., Glässer, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 33–49. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-11447-2_3CrossRef

37.

Gaspari, P., Riccobene, E., Gargantini, A.: A formal design of the Hybrid European Rail Traffic Management System. In: Proceedings of the 13th European Conference on Software Architecture - Volume 2. pp. 156–162. ECSA 2019, Association for Computing Machinery, New York, NY, USA (2019). https://doi.org/10.1145/3344948.3344993

38.

Gurevich, Y.: Evolving Algebras 1993: Lipari Guide, pp. 9–36. Oxford University Press Inc., USA (1995)

39.

Harel, D., Rumpe, B.: Meaningful modeling: What’s the semantics of “Semantics”? Computer 37(10), 64–72 (2004). https://doi.org/10.1109/MC.2004.172

40.

Leveson, N.: Are you sure your software will not kill anyone? Commun. ACM 63(2), 25–28 (2020). https://doi.org/10.1145/3376127CrossRef

41.

Lutz, R.R.: Software engineering for safety: a roadmap. In: Proceedings of the Conference on The Future of Software Engineering, pp. 213–226. ICSE 2000, Association for Computing Machinery, New York, NY, USA (2000). https://doi.org/10.1145/336512.336556

42.

Mirandola, R., Potena, P., Riccobene, E., Scandurra, P.: A reliability model for service component architectures. J. Syst. Softw. 89, 109–127 (2014). https://doi.org/10.1016/j.jss.2013.11.002CrossRef

43.

Riccobene, E., Scandurra, P.: A formal framework for service modeling and prototyping. Formal Aspects Comput. 26(6), 1077–1113 (2013). https://doi.org/10.1007/s00165-013-0289-0MathSciNetCrossRef

44.

Riccobene, E., Scandurra, P.: Model-based simulation at runtime with Abstract State Machines. In: Muccini, H., et al. (eds.) Software Architecture, pp. 395–410. Springer International Publishing, Cham (2020)CrossRef

45.

Schmidt, D.C.: Guest editor’s introduction: model-driven engineering. IEEE Comput. 39(2), 25–31 (2006). https://doi.org/10.1109/MC.2006.58CrossRef

46.

Utting, M., Legeard, B., Bouquet, F., Fourneret, E., Peureux, F., Vernotte, A.: Chapter two - recent advances in model-based testing. Advances in Computers, vol. 101, pp. 53–120. Elsevier (2016). https://doi.org/10.1016/bs.adcom.2015.11.004

47.

Van Tendeloo, Y., Van Mierlo, S., Vangheluwe, H.: A multi-paradigm modelling approach to live modelling. Softw. Syst. Model. 18(5), 2821–2842 (2018). https://doi.org/10.1007/s10270-018-0700-7CrossRef

48.

Vessio, G.: Reasoning about properties with Abstract State Machines. In: Gogolla, M., Muccini, H., Varró, D. (eds.) Proceedings of the Doctoral Symposium at Software Technologies: Applications and Foundations 2015 Conference (STAF 2015), L’Aquila, Italy, 20 July 2015. CEUR Workshop Proceedings, vol. 1499, pp. 1–10. CEUR-WS.org (2015). http://ceur-ws.org/Vol-1499/paper1.pdf

49.

Weyns, D., et al.: Perpetual assurances for self-adaptive systems. In: de Lemos, R., Garlan, D., Ghezzi, C., Giese, H. (eds.) Software Engineering for Self-Adaptive Systems III. Assurances. LNCS, vol. 9640, pp. 31–63. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-74183-3_2CrossRef

Title: The ASMETA Approach to Safety Assurance of Software Systems
Authors: Paolo Arcaini
Andrea Bombarda
Silvia Bonfanti
Angelo Gargantini
Elvinia Riccobene
Patrizia Scandurra
Publisher: Springer International Publishing
Book: Logic, Computation and Rigorous Methods
Print ISBN: 978-3-030-76019-9

Electronic ISBN: 978-3-030-76020-5

Copyright Year: 2021
DOI: https://doi.org/10.1007/978-3-030-76020-5_13

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner