A Formal Foundation of FDI Design via Temporal Epistemic Logic

Gario, Marco (2016) A Formal Foundation of FDI Design via Temporal Epistemic Logic. PhD thesis, University of Trento.

[img]PDF - Doctoral Thesis
Restricted to Repository staff only until 9999.



Autonomous systems must be able to detect and promptly react to faults. Fault Detection and Identification components (FDI) are in charge of detecting the occurrence of faults. The FDI depends on the concrete design of the system, needs to take into account how faults might interact, and can only have a partial view of the run-time state through sensors. For these reasons, the development of the FDI and certification of its correctness and quality are difficult tasks. This difficulty is compounded by the fact that current approaches for verification of the FDI rely on manual inspection and testing. Motivated by industrial case-studies from the European Space Agency, this thesis proposes a formal foundation for FDI design that covers specification, validation, verification, and synthesis. The Alarm Specification Language (ASLk) is introduced in order to formally capture a set of interesting and desirable properties of the FDI components. ASLk is equipped with a semantics based on Temporal Epistemic Logic, thus enabling reasoning about partially observable systems. Automated reasoning techniques can then be applied to perform validation, verification, and synthesis of the FDI. This formal process guarantees that the generated FDI satisfies the designer expectations. The problems deriving from this process were out of reach for existing model-checking techniques. Therefore, we develop novel and efficient techniques for model-checking temporal epistemic logic over infinite state systems.

Item Type:Doctoral Thesis (PhD)
Doctoral School:Information and Communication Technology
PhD Cycle:27
Subjects:Area 01 - Scienze matematiche e informatiche > INF/01 INFORMATICA
Area 09 - Ingegneria industriale e dell'informazione > ING-INF/05 SISTEMI DI ELABORAZIONE DELLE INFORMAZIONI
Area 01 - Scienze matematiche e informatiche > MAT/01 LOGICA MATEMATICA
Uncontrolled Keywords:Fault Detection Identification and Recovery Diagnosis Temporal Epistemic Logic Formal Methods Model Checking
Funders:Fondazione Bruno Kessler
Repository Staff approval on:04 Mar 2016 11:19

Repository Staff Only: item control page