Early-Stage Resource Estimation from Functional Reliability Specification in Embedded Cyber-Physical Systems
Reliability and fault tolerance are critical attributes of embedded cyber-physical systems that require a high safety-integrity level. For such systems, the use of formal functional safety specifications has been strongly advocated in most industrial safety standards, but reliability and fault tolerance have traditionally been treated as platform issues. We believe that addressing reliability and fault tolerance at the functional safety level widens the scope for resource optimization, targeting those functionalities that are safety-critical, rather than the entire platform. Moreover, for software based control functionalities, temporal redundancies have become just as important as replication of physical resources, and such redundancies can be modeled at the functional specification level. The ability to formally model functional reliability at a specification level enables early estimation of physical resources and computation bandwidth requirements. In this paper we propose, for the first time, a resource estimation methodology from a formal functional safety specification augmented by reliability annotations. The proposed reliability specification is overlaid on the safety-critical functional specification and our methodology extracts a constraint satisfaction problem for determining the optimal set of resources for meeting the reliability target for the safety-critical behaviors. We use SMT (Satisfiability Modulo Theories) / ILP (Integer Linear Programming) solvers at the back end to solve the optimization problem, and demonstrate the feasibility of our methodology on a Satellite Launch Vehicle Navigation, Guidance and Control (NGC) System.