In this paper we present an effective approach to perform formal verification of properties of interest of production systems whose behavior is modeled through Stateflow diagrams. 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 which allows users to define a wide range of properties of interest and then to check whether they hold for the system or not. We also point out an error in the design of the system that has been detected by applying the technique.

Automated Formal Verification for Flexible Manufacturing Systems

FERRUCCI, LUCA;
2012-01-01

Abstract

In this paper we present an effective approach to perform formal verification of properties of interest of production systems whose behavior is modeled through Stateflow diagrams. 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 which allows users to define a wide range of properties of interest and then to check whether they hold for the system or not. We also point out an error in the design of the system that has been detected by applying the technique.
2012
9783902661982
File in questo prodotto:
File Dimensione Formato  
IFAC.pdf

solo utenti autorizzati

Tipologia: Versione finale editoriale
Licenza: NON PUBBLICO - accesso privato/ristretto
Dimensione 437.87 kB
Formato Adobe PDF
437.87 kB 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/1166190
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 5
social impact