Compositional Verification of Real-Time Fault-Tolerant Programs ∗
Borzoo Bonakdarpour, Sandeep S. Kulkarni · 2009
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 in- troduce 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 pro- grams. Preliminary model checking experiments show very encouraging results in both achieving speedups and reducing memory usage in verification of embedded systems.