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.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.