Presentation
Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems
20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
(2014)
Abstract
We propose a real-time, Realizable, Responsive, Unobtrusive Unit (rt-R2U2) to meet the emerging needs for System Health Management (SHM) of new safety-critical embedded systems like automated vehicles, Unmanned Aerial Systems (UAS), or small satellites. SHM for these systems must be able to handle unexpected situations and adapt specifications quickly during flight testing between closely-timed consecutive missions, not mid-mission, necessitating fast reconfiguration. They must enable more advanced probabilistic reasoning for diagnostics and prognostics while running aboard limited hardware without affecting the certified on-board software. We define and prove correct translations of two real-time projections of Linear Temporal Logic to two types of efficient observer algorithms to continuously assess the status of the system. A synchronous observer yields an instant abstraction of the satisfaction check, whereas an asynchronous observer concretizes this abstraction at a later, a priori known, time. By feeding the system’s real-time status into a statistical reasoning unit, e.g., based on Bayesian networks, we enable advanced health estimation and diagnosis. We experimentally demonstrate our novel framework on real flight data from NASA’s Swift UAS. By on-boarding rt-R2U2 aboard an existing FPGA already built into the standard UAS design and seamlessly intercepting sensor values through read-only observations of the system bus, we avoid system integration problems of software instrumentation or added hardware. The flexibility of our approach with regard to changes in the monitored specification is not due to the reconfigurability offered by FPGAs; it is a benefit of the modularity of our observers and would also be available on non-reconfigurable hardware platforms such as ASICs.
Keywords
- Bayesian Network,
- Field Programmable Gate Array,
- Time Stamp,
- Linear Temporal Logic,
- Execution Sequence
Disciplines
Publication Date
2014
Location
Grenoble, France
DOI
10.1007/978-3-642-54862-8_24
Comments
The final publication is available at Springer via https://doi.org/10.1007/978-3-642-54862-8_24.
Works produced by employees of the U.S. Government as part of their official duties are not copyrighted within the U.S. The content of this document is not copyrighted.
Citation Information
Thomas Reinbacher, Kristin Yvonne Rozier and Johann Schumann. "Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems" 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2014) Available at: http://works.bepress.com/kristin-yvonne-rozier/16/