When applying formal verification to a system that interacts with the real world we must use a model of the environment. This model represents an abstraction of the actual environment, so it is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well-behaved. A solution to this problem consists in exploiting the model of the environment used for statically verifying the system’s behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The paper discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies, an autonomous cruise control system, and a simulation of the Mars Curiosity rover.

Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems / Ferrando, Angelo; Dennis, Louise A.; Cardoso, Rafael C.; Fisher, Michael; Ancona, Davide; Mascardi, Viviana. - In: ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY. - ISSN 1049-331X. - 30:(2021), pp. 1-43. [10.1145/3447246]

Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems

Ferrando, Angelo;
2021

Abstract

When applying formal verification to a system that interacts with the real world we must use a model of the environment. This model represents an abstraction of the actual environment, so it is necessarily incomplete and hence presents an issue for system verification. If the actual environment matches the model, then the verification is correct; however, if the environment falls outside the abstraction captured by the model, then we cannot guarantee that the system is well-behaved. A solution to this problem consists in exploiting the model of the environment used for statically verifying the system’s behaviour and, if the verification succeeds, using it also for validating the model against the real environment via runtime verification. The paper discusses this approach and demonstrates its feasibility by presenting its implementation on top of a framework integrating the Agent Java PathFinder model checker. A high-level Domain Specific Language is used to model the environment in a user-friendly way; the latter is then compiled to trace expressions for both static formal verification and runtime verification. To evaluate our approach, we apply it to two different case studies, an autonomous cruise control system, and a simulation of the Mars Curiosity rover.
2021
30
1
43
Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems / Ferrando, Angelo; Dennis, Louise A.; Cardoso, Rafael C.; Fisher, Michael; Ancona, Davide; Mascardi, Viviana. - In: ACM TRANSACTIONS ON SOFTWARE ENGINEERING AND METHODOLOGY. - ISSN 1049-331X. - 30:(2021), pp. 1-43. [10.1145/3447246]
Ferrando, Angelo; Dennis, Louise A.; Cardoso, Rafael C.; Fisher, Michael; Ancona, Davide; Mascardi, Viviana
File in questo prodotto:
File Dimensione Formato  
Towards_a_Holistic_Approach_to_Verification_and_Validation_of_Autonomous_Cognitive_Systems__Journal_(1).pdf

Open access

Tipologia: Versione dell'autore revisionata e accettata per la pubblicazione
Dimensione 1.05 MB
Formato Adobe PDF
1.05 MB Adobe PDF Visualizza/Apri
3447246.pdf

Accesso riservato

Tipologia: Versione pubblicata dall'editore
Dimensione 4.7 MB
Formato Adobe PDF
4.7 MB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Licenza Creative Commons
I metadati presenti in IRIS UNIMORE sono rilasciati con licenza Creative Commons CC0 1.0 Universal, mentre i file delle pubblicazioni sono rilasciati con licenza Attribuzione 4.0 Internazionale (CC BY 4.0), salvo diversa indicazione.
In caso di violazione di copyright, contattare Supporto Iris

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11380/1331894
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 6
social impact