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, but 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 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. Trace expressions are used to model the environment for both static formal verification and runtime verification.

Verifying and validating autonomous systems: Towards an integrated approach / Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; Mascardi, V.. - 11237:(2019), pp. 263-281. (Intervento presentato al convegno 18th International Conference on Runtime Verification, RV 2018 tenutosi a Limassol, Cyprus nel 10 novembre 2018) [10.1007/978-3-030-03769-7_15].

Verifying and validating autonomous systems: Towards an integrated approach

Ferrando A.;
2019

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, but 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 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. Trace expressions are used to model the environment for both static formal verification and runtime verification.
2019
18th International Conference on Runtime Verification, RV 2018
Limassol, Cyprus
10 novembre 2018
11237
263
281
Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; Mascardi, V.
Verifying and validating autonomous systems: Towards an integrated approach / Ferrando, A.; Dennis, L. A.; Ancona, D.; Fisher, M.; Mascardi, V.. - 11237:(2019), pp. 263-281. (Intervento presentato al convegno 18th International Conference on Runtime Verification, RV 2018 tenutosi a Limassol, Cyprus nel 10 novembre 2018) [10.1007/978-3-030-03769-7_15].
File in questo prodotto:
File Dimensione Formato  
Ferrando2018_Chapter_VerifyingAndValidatingAutonomo.pdf

Accesso riservato

Dimensione 1.25 MB
Formato Adobe PDF
1.25 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/1331839
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 22
  • ???jsp.display-item.citation.isi??? 17
social impact