基于时序认知逻辑的异步故障检测与识别组件形式化设计
Formal Design of Asynchronous Fault Detection and Identification Components using Temporal Epistemic Logic
摘要：
自主关键系统，如卫星和空间漫游者，必须能够检测故障的发生，以确保正确的操作。此任务由故障检测和识别（FDI）组件执行，这些组件嵌入在这些系统中，并负责通过从传感器读取数据并触发预定义的警报来自动及时地检测故障。设计有效的外国直接投资成分是一个极其困难的问题，也是由于缺乏完整的理论基础，以及精确的规范和验证技术。在本文中，我们提出了第一个正式的方法来设计的FDI组件的离散事件系统，无论是在同步和异步设置。我们提出了一个逻辑语言的规范的外国直接投资的要求，占了广泛的实际案例，并包括新的方面，如最大化和跟踪诊断。该语言配备了一个明确的语义的时间认知逻辑的基础上，并被证明享有适当的属性。我们将讨论如何验证需求，以及如何验证给定的FDI组件是否满足这些需求。我们提出了一种算法，正确的建设FDI组件的合成，并报告的适用性的设计方法的工业案例研究来自航空航天。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
