CINECA IRIS Institutional Research Information System
IRIS è l'Anagrafe della ricerca dell'Università degli Studi di Trento, e ha lo scopo di raccogliere, documentare, conservare e diffondere, anche ad accesso aperto, la produzione scientifica degli autori afferenti all'Università degli Studi di Trento.
EnglishThe correct operation of complex critical systems is increasingly relying on the ability to detect whether (and which) faults are occurring. This task, known as Fault Detection and Identification (FDI), is typically carried out by an FDI component that, observing the sequence of values conveyed by some predefined observables, triggers a set of predefined alarms. An effective FDI system can provide vital information to steer the containment and recovery of faults. We recently proposed a formal framework to support the design of FDI for discrete event systems. The framework is based on a logical language for the specification of FDI requirements and it captures problems such as local diagnosability and maximality, by relying on a semantics based on temporal epistemic logic. This enables the formal verification of the specification and the synthesis of correct-by-construction FDI components. In this paper, we show the merits of the framework by applying it on a simple example, working out the details of the synthesis algorithm, and by reporting the experience on an industrial case-study from the aerospace domain.
Scheda prodotto non validato
I dati visualizzati non sono stati ancora sottoposti a validazione formale da parte dello Staff di IRIS, ma sono stati ugualmente trasmessi al Sito Docente Cineca (Loginmiur).
| Titolo: | Formal Specification and Synthesis of FDI through an Example |
| Autori: | Bozzano, Marco; Cimatti, Alessandro; Gario, Marco Elio Gustavo; Stefano, Tonetta |
| Autori Unitn: | |
| Titolo del volume contenente il saggio: | Proceedings of the 24th International Workshop on Principles of Diagnosis |
| Luogo di edizione: | Jerusalem, Israel |
| Casa editrice: | DX |
| Anno di pubblicazione: | 2013 |
| Handle: | http://hdl.handle.net/11572/99531 |
| Appare nelle tipologie: | 04.1 Saggio in atti di convegno (Paper in proceedings) |
File in questo prodotto:
Copyright © 2020