Skip to main content
main-content
Top

Hint

Swipe to navigate through the chapters of this book

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

share
SHARE

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.
Footnotes
2
Note that $x denotes the variable x in the AsmetaL notation.
 
3
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.
 
Literature
1.
go back to reference Al-Shareefi, F.: Analysing Safety-Critical Systems and Security Protocols with Abstract State Machines. Ph.D. thesis, University of Liverpool (2019) Al-Shareefi, F.: Analysing Safety-Critical Systems and Security Protocols with Abstract State Machines. Ph.D. thesis, University of Liverpool (2019)
4.
go back to reference 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.: 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
7.
go back to reference 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.: 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
9.
go back to reference 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 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
21.
go back to reference 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_​5 CrossRef 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_​5 CrossRef
25.
go back to reference Börger, E.: The ASM refinement method. Formal Aspects Comput. 15, 237–257 (2003) CrossRef Börger, E.: The ASM refinement method. Formal Aspects Comput. 15, 237–257 (2003) CrossRef
32.
go back to reference Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19(3), 215–261 (2009) CrossRef Fraser, G., Wotawa, F., Ammann, P.E.: Testing with model checkers: a survey. Softw. Test. Verif. Reliab. 19(3), 215–261 (2009) CrossRef
37.
go back to reference 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 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.
go back to reference Gurevich, Y.: Evolving Algebras 1993: Lipari Guide, pp. 9–36. Oxford University Press Inc., USA (1995) Gurevich, Y.: Evolving Algebras 1993: Lipari Guide, pp. 9–36. Oxford University Press Inc., USA (1995)
44.
go back to reference 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 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
48.
go back to reference 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 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
Metadata
Title
The ASMETA Approach to Safety Assurance of Software Systems
Authors
Paolo Arcaini
Andrea Bombarda
Silvia Bonfanti
Angelo Gargantini
Elvinia Riccobene
Patrizia Scandurra
Copyright Year
2021
DOI
https://doi.org/10.1007/978-3-030-76020-5_13

Premium Partner