Formal Methods for Pattern Based Reliability Analysis in Embedded Systems

A wide variety of periodic tasks in embedded systems require reliable service guarantees under a given fault distribution. Reliable execution requires the periodic task to be replicated more often under normal circumstances so that the desired service throughput is achieved under the fault distribution. This paper presents a formal approach for verifying whether an input distribution meets the desired service guarantee under a fault distribution, where all the distributions are specified in real time calculus. The proposed methodology leverages the recently discovered relationship between real time calculus specifications and omega-regular languages.