Skip to main content

Compositional Verification of Fault-Tolerant Real-Time Programs

Publication Type
Year of Publication
Conference/Journal Name
ACM/IEEE International Conference on Embedded Software (EMSOFT)
A hard-masking real-time program is one that satisfies safety (including timing constraints) and liveness properties in the absence and presence of faults. It has been shown that any hard-masking program can be decomposed into a fault-intolerant version and a set of fault-tolerance components known as detectors and δ-correctors. In this paper, we introduce a set of sufficient conditions for interference-freedom among fault-tolerance components and real-time programs. We demonstrate that such conditions elegantly enable us to compositionally verify the correctness of hard-masking programs. Preliminary model checking experiments show very encouraging results in both achieving speedups and reducing memory usage in verification of embedded systems.
Other Info.
Best paper award finalist