The paper presents an approach for rigorous development of safety-critical systems based on the Abstract State Machine formal method. The development process starts from a high level formal view of the system and, through refinement, derives more detailed models till the desired level of specification. Along the process, different validation and verification activities are available, as simulation, model review, and model checking. Moreover, each refinement step can be proved correct using an SMT-based approach. As last step of the refinement process, a Java implementation can be developed and linked to the formal specification. The correctness of the implementation w.r.t. its formal specification can be proved by means of model-based testing and runtime verification. The process is exemplified by using a Landing Gear System as case study.

(2017). Rigorous development process of a safety-critical system: from ASM models to Java code [journal article - articolo]. In INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. Retrieved from http://hdl.handle.net/10446/50048

Rigorous development process of a safety-critical system: from ASM models to Java code

ARCAINI, Paolo;GARGANTINI, Angelo Michele;
2017-01-01

Abstract

The paper presents an approach for rigorous development of safety-critical systems based on the Abstract State Machine formal method. The development process starts from a high level formal view of the system and, through refinement, derives more detailed models till the desired level of specification. Along the process, different validation and verification activities are available, as simulation, model review, and model checking. Moreover, each refinement step can be proved correct using an SMT-based approach. As last step of the refinement process, a Java implementation can be developed and linked to the formal specification. The correctness of the implementation w.r.t. its formal specification can be proved by means of model-based testing and runtime verification. The process is exemplified by using a Landing Gear System as case study.
articolo
2017
Arcaini, Paolo; Gargantini, Angelo Michele; Riccobene, Elvinia
(2017). Rigorous development process of a safety-critical system: from ASM models to Java code [journal article - articolo]. In INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. Retrieved from http://hdl.handle.net/10446/50048
File allegato/i alla scheda:
File Dimensione del file Formato  
J_STTT.pdf

Solo gestori di archivio

Versione: publisher's version - versione editoriale
Licenza: Licenza default Aisberg
Dimensione del file 2.71 MB
Formato Adobe PDF
2.71 MB Adobe PDF   Visualizza/Apri
50048 Gargantini.pdf

Open Access dal 06/08/2016

Descrizione: This is a post-peer-review, pre-copyedit version of an article published in International Journal on Software Tools for Technology . The final authenticated version is available online at: http://dx.doi.org/10.1007/s10009-015-0394-x
Versione: postprint - versione referata/accettata senza referaggio
Licenza: Licenza default Aisberg
Dimensione del file 914.24 kB
Formato Adobe PDF
914.24 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

Aisberg ©2008 Servizi bibliotecari, Università degli studi di Bergamo | Terms of use/Condizioni di utilizzo

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10446/50048
Citazioni
  • Scopus 30
  • ???jsp.display-item.citation.isi??? 15
social impact