We present an effective approach to perform formal verification of properties of interest of production systems whose behavior is modeled through Stateflowdiagrams. The approach hinges on a semantics of Stateflow diagrams given in terms of formulae of a metric temporal logic. The semantics has been implemented in a fully automated tool through which users can define a wide range of properties of interest and then check if they hold for the system.We illustrate the approach and the use of the tool through a realistic case study. The verification technique allowed us to uncover a previously undetected error in the design of the system.

Automated formal verification for flexible manufacturing systems

FERRUCCI, LUCA;
2014-01-01

Abstract

We present an effective approach to perform formal verification of properties of interest of production systems whose behavior is modeled through Stateflowdiagrams. The approach hinges on a semantics of Stateflow diagrams given in terms of formulae of a metric temporal logic. The semantics has been implemented in a fully automated tool through which users can define a wide range of properties of interest and then check if they hold for the system.We illustrate the approach and the use of the tool through a realistic case study. The verification technique allowed us to uncover a previously undetected error in the design of the system.
2014
Carpanzano, E.; Ferrucci, Luca; Mandrioli, Dino; Mazzolini, M.; Morzenti, ANGELO CARLO; Rossi, MATTEO GIOVANNI
File in questo prodotto:
File Dimensione Formato  
Automated formal verification.pdf

solo utenti autorizzati

Tipologia: Versione finale editoriale
Licenza: NON PUBBLICO - accesso privato/ristretto
Dimensione 1.54 MB
Formato Adobe PDF
1.54 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/11568/1166187
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? 6
social impact