Reliability annotations to formal specifications of context-sensitive safety properties in embedded systems

As the aspect of reliability is becoming increasingly important in the context of safety-critical embedded systems, developing formalism for specifying the reliability requirements for such systems has become very relevant. We present a formalism for modeling the reliability requirement succinctly for safety-critical embedded systems and propose the semantics over the task schedule of the embedded systems controller. We introduce the notion of reliability deficiency to represent the difference between the specified and the actual value of the reliability achieved by a schedule and present techniques to make up the reliability deficiency. The presented approach is primarily applicable to specify the reliability requirements of context-sensitive tasks executed by a real-time software system so that they can overcome transient failures using temporal redundancy, i.e., repetitive execution of the same task. We illustrate our formalism and the proposed techniques using suitable scenarios from the automotive domain.