"Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems"

TACAS'14 Publication

Thomas Reinbacher, Kristin Yvonne Rozier, and Johann Schumann


These pages contain further details of the experiments described in "Temporal-Logic Based Runtime Observer Pairs for System Health Management of Real-Time Systems" by Thomas Reinbacher, Kristin Yvonne Rozier, and Johann Schumann. The BibTeX for this paper is available here.


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.

Results from this paper were featured in the NASA Ames 2014 Director's Colloquium Summer Series "Dr. Kristin Yvonne Rozier - No More Helicopter Parenting: Intelligent, Autonomous UAS" on the NASA Ames YouTube Channel, June 10, 2014.

Supplementary material

Hardware Simulations

Simulation Traces


FPGA Target Platform