Cyber Physical Systems (CPSs) consist of hardware and software components. To verify that the whole (i.e., software + hardware) system meets the given specifications, exhaustive simulation-based approaches (Hardware In the Loop Simulation, HILS) can be effectively used by first generating all relevant simulation scenarios (i.e., sequences of disturbances) and then actually simulating all of them (verification phase). When considering the whole verification activity, we see that the above mentioned verification phase is repeated until no error is found. Accordingly, in order to minimise the time taken by the whole verification activity, in each verification phase we should, ideally, start by simulating scenarios witnessing errors (counterexamples). Of course, to know beforehand the set of such scenarios is not feasible. In this paper we show how to select scenarios so as to minimise the Worst Case Expected Verification Time

On minimising the maximum expected verification time / Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Salvo, Ivano; Tronci, Enrico. - In: INFORMATION PROCESSING LETTERS. - ISSN 0020-0190. - STAMPA. - 122:(2017), pp. 8-16. [10.1016/j.ipl.2017.02.001]

On minimising the maximum expected verification time

MANCINI, Toni;MARI, FEDERICO;MASSINI, Annalisa;MELATTI, IGOR;SALVO, Ivano;TRONCI, Enrico
2017

Abstract

Cyber Physical Systems (CPSs) consist of hardware and software components. To verify that the whole (i.e., software + hardware) system meets the given specifications, exhaustive simulation-based approaches (Hardware In the Loop Simulation, HILS) can be effectively used by first generating all relevant simulation scenarios (i.e., sequences of disturbances) and then actually simulating all of them (verification phase). When considering the whole verification activity, we see that the above mentioned verification phase is repeated until no error is found. Accordingly, in order to minimise the time taken by the whole verification activity, in each verification phase we should, ideally, start by simulating scenarios witnessing errors (counterexamples). Of course, to know beforehand the set of such scenarios is not feasible. In this paper we show how to select scenarios so as to minimise the Worst Case Expected Verification Time
2017
Explicit model checking; Formal methods; Formal verification; Software engineering; System-level formal verification; Theoretical Computer Science; Signal Processing; Information Systems
01 Pubblicazione su rivista::01a Articolo in rivista
On minimising the maximum expected verification time / Mancini, Toni; Mari, Federico; Massini, Annalisa; Melatti, Igor; Salvo, Ivano; Tronci, Enrico. - In: INFORMATION PROCESSING LETTERS. - ISSN 0020-0190. - STAMPA. - 122:(2017), pp. 8-16. [10.1016/j.ipl.2017.02.001]
File allegati a questo prodotto
File Dimensione Formato  
Massini_Minimising_2017.pdf

accesso aperto

Tipologia: Documento in Post-print (versione successiva alla peer review e accettata per la pubblicazione)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 424.17 kB
Formato Adobe PDF
424.17 kB Adobe PDF
Massini_Minimising_2017.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 396.36 kB
Formato Adobe PDF
396.36 kB Adobe PDF   Contatta l'autore

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

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