Bozzano, Marco and Cimatti, Alessandro and Gario, Marco and Tonetta, Stefano - Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic

lmcs:1605 - Logical Methods in Computer Science, November 4, 2015, Volume 11, Issue 4
Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic

Authors: Bozzano, Marco and Cimatti, Alessandro and Gario, Marco and Tonetta, Stefano

Autonomous critical systems, such as satellites and space rovers, must be able to detect the occurrence of faults in order to ensure correct operation. This task is carried out by Fault Detection and Identification (FDI) components, that are embedded in those systems and are in charge of detecting faults in an automated and timely manner by reading data from sensors and triggering predefined alarms. The design of effective FDI components is an extremely hard problem, also due to the lack of a complete theoretical foundation, and of precise specification and validation techniques. In this paper, we present the first formal approach to the design of FDI components for discrete event systems, both in a synchronous and asynchronous setting. We propose a logical language for the specification of FDI requirements that accounts for a wide class of practical cases, and includes novel aspects such as maximality and trace-diagnosability. The language is equipped with a clear semantics based on temporal epistemic logic, and is proved to enjoy suitable properties. We discuss how to validate the requirements and how to verify that a given FDI component satisfies them. We propose an algorithm for the synthesis of correct-by-construction FDI components, and report on the applicability of the design approach on an industrial case-study coming from aerospace.


Source : oai:arXiv.org:1506.04871
DOI : 10.2168/LMCS-11(4:4)2015
Volume: Volume 11, Issue 4
Published on: November 4, 2015
Submitted on: November 16, 2014
Keywords: Computer Science - Logic in Computer Science


Share

Consultation statistics

This page has been seen 115 times.
This article's PDF has been downloaded 82 times.