Logical Reliability of Interacting Real-Time Tasks
Arkadeb Ghosal, Krishnendu Chatterjee, Thomas A. Henzinger, Daniel Iercan, Christoph Kirsch, Claudio Pinello and Alberto L. Sangiovanni-Vincentelli
We propose an abstract notion of logical reliability for real-time program tasks that interact through periodically updated program variables. Logical reliability is a requirement on possibly distributed implementations to provide, in the long run, reliable updates of program variables. We describe a reliability analysis approach that checks if the given short-term (e.g., single-period) reliability of a program variable update in an implementation is sufficient to meet the logical reliability requirement (of the program variable) in the long run. We then present a notion of design by refinement where a task can be refined by another task that writes to program variables with less logical reliability. The notion of refinement preserves the reliability analysis, i.e., if an implementation is reliable for the refined task, then the implementation is reliable for the refining task. The resulting analysis can be readily combined with an incremental schedulability analysis for interacting real-time tasks that was proposed earlier for Hierarchical Timing Language (HTL), a hierarchical coordination language for distributed real-time systems. We have implemented a logical-reliability-enhanced prototype of the compiler and runtime infrastructure for HTL, and tested the system on a real (i.e., not simulated) control application.