"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
2014
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.
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.
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
- Full paper with Appendicies: RRS_TACAS2014_full.pdf (includes: Correctness proofs, Proofs of Complexity Results, Example Simulation Traces)
- BibTeX: RRS14.bib
Hardware Simulations
Simulation Traces
- High-res simulation screenshots (full): simulationTraceFull.pdf
- High-res simulation screenshots (laser outage section): simulationTraceOutage.pdf
- Raw simulation data: rawSimulationData.7z
(allows to step through the simulation traces)
- Instructions: After starting model sim, change your working directory with file, change directory and point to the directory where the *.wlf files are located. Next, at the prompt:
> vsim -view filename.wlf
ModelSim will then load up the simulation information. However, it does not launch the waveform window. To do this, open the waveform window and add the list of signals to the wave window:
> do filename.do
Modelsim will then launch the wave window, list the signals and show the results as seen in the vsim.wlf file.
Tools
FPGA Target Platform
