Early-stage Resource Estimation from
Functional Reliability Specifications in
Embedded Cyber-Physical Systems

With increasing dependence of safety-critical systems on software and embedded computing, the notions of reliability and fault tolerance have undergone a paradigm shift. While the traditional approach for enhancing reliability in electro-mechanical systems is based on replication of physical components [21, 24, 32, 39, 3, 30], safety-critical embedded cyber-physical systems (CPS) must also consider reliability of software executions, packet drops in networks, priority inversion in scheduling of control tasks on shared processors, and many other factors which are attributed to the computational platform which executes the cyber part of the system [7, 28].

In the domain of cyber-physical systems, reliability targets of embedded control can be met through fault-tolerant design of the underlying platform and its structural components or through fault-tolerant deployment of the control software on the underlying platform. The former looks at the necessary resource requirements for providing reliable service at the platform level without specific focus on individual control components [4]. For example, while designing the CAN matrix for an automobile, we choose the topology and number of CAN segments depending on the overall loading of the buses and the reliability concerns thereof. On the other hand, fault-tolerant deployment of control focuses on individual control tasks [15]. For example, it includes replication of software tasks on multiple cores [38] and sometimes on the same core (temporal redundancy) [14, 26, 23, 25], or provides fault-tolerant scheduling frameworks that involve cloning of a sequence of tasks for layered task graphs [10, 37]. Fault-tolerant deployment also influences the choice of the platform and its components, but with respect to the reliability requirements for individual functional components.

The design cycle of cyber-physical systems begin with the preparation of a specification of the functionalities of the system. The use of formal specifications for defining the functional safety properties of such systems has been widely recommended in most industrial standards, including aeronautics (DO-178C), automotive (ISO 26262), industrial process automation (IEC 61508), nuclear (IEC 60880), railway (EN 50128) and space (ECSS-Q-ST-80C), specifically for those functionalities that require a high safety-integrity level. Although reliability and fault tolerance are as important attributes of the system design as functional correctness [6, 8, 9, 11, 27, 34], or performance attributes such as timing [1, 2, 12, 13, 33], power [17, 18] and security [22], formal specification of reliability, especially with respect to the critical functional safety properties has so far received very little attention. This is largely due to the perception that reliability and fault tolerance need to be addressed at the platform level, not at the functional level [20, 40]. On the other hand, we believe that with the increasing cost of electronics and software in cyber-physical systems, investment on reliability needs to be prioritized on the basis of the safety-criticality of the system’s functions.

This paper presents, for the first time, a methodology for overlaying formal functional safety specifications with reliability annotations and estimating the resource requirement from such extended specifications. A formal specification enables the designer to lay out the strategy for redundant computations and/or actuations [16] and obtain a formal reliability guarantee for the strategy using the proposed method of analysis. Moreover since this is done at the specification level, our methodology provides early estimates of the resource requirements, thereby facilitating design space exploration, where the tradeoff between reliability and resource requirements can be studied using the proposed methodology until an acceptable balance is achieved.

In particular, our previous work [16] explores various reliable strategies enabled by the given reliability specifications and converges on a strategy that maximizes the reliability – thereby also pointing out whether the specified reliability targets are attainable for every functionality of the design. In our level of abstraction, an action represents a discrete control event which is enabled by a logically defined pre-condition (sense) and achieves a logically specified consequent (outcome) when executed successfully on the underlying computational platform. We use the term action-strategy to denote possible sequences of actions that lead to some desired outcome. An action-strategy is admissible with respect to a reliability target, if the sequence and timing of actions involved in that strategy guarantees the desired outcome with the specified reliability guarantee. It may be noted that, more than one admissible action-strategies may exist for a functionality and every participating action (at any time instant) in an admissible strategy requires one processor (computing resource) to execute.

In the early stage of design of a complex, multi-component embedded control system, the designer must plan the sense-control-actuation steps for each control loop along with the corresponding timing constraints. The formal safety specification at this stage defines the necessary outcomes of the closed loop system as a timed function of the sensed input events. For example, we may be given a safety property of the form:

where sense_A is a sense event and outcome_B is the desired outcome which must happen within the time interval [1:10] following the sense event. Now in order to ensure that outcome_B does actually happen in that window of time, the control system must perform appropriate actions (called actuations).

Suppose we have an action, called action_C which can cause outcome_B, but the causality is not fully guaranteed. Suppose:

which means that action_C, if used, can cause outcome_B 80% of the time. Now suppose our reliability target for the above safety property is $0.95$. If the sense event, sense_A, triggers one execution of the action, action_C, then the reliability with which outcome_B is guaranteed is only $0.8$. Therefore, in order to achieve the target of $0.95$, we must be prepared to repeat action_C more than once, either on different resources, or on the same resource but at different times. Moreover, all executions must be completed within the specified window of time, namely [1:10], following the event sense_A.

In a complex system, there can be many safety properties and therefore, many different actions may have to be repeated spatially and/or temporally to achieve the desired reliability. We provide a framework, where the system designer can overlay a chosen pattern of redundancy over the temporal fabric of the safety specification. For example, consider the following specification:

The above specification specifies that following a sense_A event, the action, action_C, will be executed in parallel at some time in the window [2:5], and will be again executed after $[1:2]$ units of time. It be noted that all three executions of action_C are constrained by time windows, but they can be executed in more than one way within the specified windows. A formal specification framework like this has two immediate advantages:

1. 1.

   We can verify whether the specified redundancy in the executions of the actions achieves the target reliability of the safety properties.

2. 2.

   Each possible schedules of the actions provides us an early estimate of the resource requirements. We can also find the schedule which has the optimal resource requirement. In a complex system, with many actions and replications, this is a non-trivial task and computationally beyond manual capacity.

It may also be noted that two admissible action-strategies with respect to two different reliability specifications may share some common actions. Given a set of admissible action-strategies with respect to various sensed-events, it is necessary to predict the amount of resources (processors) required in order to execute all of them in a worst-case scenario when all sensed-events, take place together. This estimation is non-trivial due to the sharing of actions and the redundancy provisions present in the strategies, and hence the choice of an appropriate admissible action-strategy with respect to every sensing is a key to reduce the number of resources. This paper presents a novel technique for selecting and grouping the set of admissible action-strategies attributed from various specifications with respect to different sensed-events, so that the number of resources needed in the worst case for executing the actions is minimized.

With the rapid growth in the number of features supported in modern appliances, the computing paradigm is shifting from a federated architecture where each feature runs on a dedicated processor to an integrated architecture where Electronic Control Units (ECUs) are shared among multiple features. While integrated architectures are able to reduce the costs of electronics and networking, the scheduling and fault tolerant deployment of control tasks has become more complex. We believe that having an early estimate of the resource requirements, as in the proposed approach, can help in taking rational decisions on the tradeoff between reliability and resource costs.

Our early work, presented in [16], introduces the formal framework for reliability specification. The problem of estimating resource requirements from such specifications is treated in this paper for the first time. The main contributions of this paper are as follows:

• •

  We extract all possible admissible reliability strategies from a given reliability specification, that meets the desired reliability target for a functional specification.

• •

  We formulate the resource optimization problem in terms of a constraint-satisfaction problem which can be solved using SMT / ILP solvers.

• •

  We have studied the proposed technique over test-cases from automotive domain and also shown the scalability of our approach over several experiments.

• •

  We illustrate the practicality of our proposed technique using a case-study (over Satellite Launch Vehicle Navigation, Guidance and Control (NGC) System) from avionics domain.

It is important to note that resource estimation is intricately related to the code volumes associated with the control tasks and their worst case execution times (WCET) on the chosen ECUs. In practice, the design of embedded systems is a process that goes through multiple generations of a product, and statistical knowledge about the execution times and the probability of their success in terms of providing the desired outcome are available from legacy data. Therefore early estimation of the tradeoff between functional reliability and resource requirements is feasible in practice, though not in established practice today.

The paper is organized as follows. Section 2 illustrates the preliminary concepts and the earlier works carried out to set up the premise for this work. In Section 3, we present the formal problem definition and methods to determine the optimal number of resources. The experimental results showing the efficacy of our proposed framework is given in Section 4. In Section 5, we demonstrate our proposed methodology using a practical case-study. Finally, Section 6 concludes the paper with a brief discussion on the ramifications of the proposed approach.

An embedded controller of a CPS comprises of three primary modules, namely Sensor, Controller and Actuator – which interacts with the Plant (or the environment) to perform desired behaviors. The sensor is responsible for sensing input scenarios from the plant (or the environment). The controller performs the control decision based on the sensed input. The actuator delivers actuation signals to the plant (or the environment). Some of the activities in CPS control may be implemented using software and the rest may be controlled via hardware. For example, sensing a scenario where the brake should be applied automatically, the computation of appropriate brake-pressure may be carried out using a software program. However, maintaining the same break-pressure for a certain amount of time is performed by a hardware-control. The resultant outcome while applying such actions is the application of the wheel-brakes and thereby reduction in the vehicle speed. We present a formal model for embedded CPS and such requirements in the following.

Figure 1 provides a schematic representation of the embedded CPS framework. Here, the events that are responsible for sensing inputs, actions (actuations) and outcome activities are termed as sensed-events ($\mathcal{E}_{I}$), action-events ($\mathcal{E}_{A}$) and outcome-events ($\mathcal{E}_{O}$), respectively. While interacting with the plant model, the controller receives the sensed-events and compute appropriate actions/actuations to produce the desired outcome-events. The outcome of an action may take place after many control cycles and may also be durable over a period of time. Typically, the control software execution platform is responsible to compute appropriate actuations for the desired outcomes being enabled.

The reliability of the CPS is governed by the fault-free execution from sensed to the outcome events. This intuitively means, after sensing an input scenario, how reliably an action (actuations) can be performed once the controller decision is undertaken properly. In this model, the reliability of the outcome activities are attributed from the unreliable computational platform where the action events are scheduled, computed and applied. To meet the desired reliability of the outcome behavior, the fine-grain control incorporates various physical redundancy attributes in the scheduled actions inside the control execution platform. It may be noted that the unreliability lies primarily in the execution of action-events (as per our model), though there can also be failures in the sensing and application of outcome activities or imperfections in message communications. However, this framework can be suitably extended to handle such uncertainties in other components of the embedded CPS framework.

From an abstract point of view, the activities of a CPS can be visualized in terms of sequence of events. The early-stage functional specification narrates the outcome-event based on a sensed scenario which is to be met with specific reliability targets. Such specifications describe the correctness requirements for a CPS. In addition to this, the meta-level action-strategy specifies the supervisory control orchestrated by the control software where the redundancies in actions are described for a sensed scenario. Such requirements are termed as CPS reliability specifications [16].

Now, let us revisit the formal model for such embedded CPS specifications as introduced in [16] using an elementary correctness requirement, $\mathcal{P}_{S}$, for the subsystem, $S$, with a sense-event, $E_{I}\in\mathcal{E}_{I}$, and an outcome-event, $E_{O}\in\mathcal{E}_{O}$ as follows:

It means that, whenever $E_{I}$ is sensed then the outcome-event $E_{O}$ is asserted within next ${\tt a}$ to ${\tt b}$ time-units¹¹1The formal expressions of the properties have syntactic (and semantic) similarity with SystemVerilog Assertions (SVA) [42].. Suppose, $E_{A}\in\mathcal{E}_{A}$ is the action-event responsible for producing the outcome $E_{O}$. If the probability of success for $E_{O}$ given the successful execution of $E_{A}$ is expressed as, $R_{E_{O}}=Prob(E_{O}\ |\ E_{A})$, then the current reliability ($R_{\mathcal{P}_{S}}$) of the property, $\mathcal{P}_{S}$, is also $R_{E_{O}}$. Since we have $R_{\mathcal{P}_{S}}=Prob(E_{O}\ |\ E_{A})\ast Prob(E_{A}\ |\ E_{I})\ast Prob(E_{I})$, so $R_{\mathcal{P}_{S}}=R_{E_{O}}$ happens under the assumption of a perfect sense and action scenario²²2We assume that the control system senses perfectly (without any false positives or false negatives) and also generates appropriate actions based on the sensed-event., where both $Prob(E_{A}\ |\ E_{I})=1$ and $Prob(E_{I})=1$.

At the design-level, the controller can leverage spatial and temporal redundancy provisions to improve the reliability of the outcome-events and thereby enhance the functional reliability of the design specifications. Figure 2(a) and Figure 2(b) show the schematic models where the spatial and temporal redundancy provisions are incorporated at the controller level. In the spacial redundancy model for a CPS control system, $S$, there are $n$ parallel instances of the controller, namely $C_{1},C_{2},\ldots,C_{n}$ and $n$ computational counterparts, $M_{1},M_{2},\ldots,M_{n}$. The controllers $C_{i},i\in[1,n]$ sense the same events ($E_{I}\in\mathcal{E}_{I}$) and produce the action-events $E_{A_{1}}(t),E_{A_{2}}(t),\ldots,E_{A_{n}}(t)$ ($\forall i\in[1,n],\ E_{A_{i}}(t)\in\mathcal{E}_{A}$), respectively, at time $t$. Each action-event $E_{A_{i}}$ goes into a possibly unreliable computational counterpart, $M_{i}$, respectively. On the other hand, in the temporal redundancy model, $m$ number of re-executions are made by a single controller within the time-window from ${\tt a}$ to ${\tt b}$. At time $t_{i}$ ($\forall i\in[1,m],\ a\leq t_{i}\leq b$), the controller, $C$, senses same input-event, $E_{I}\in\mathcal{E}_{I}$, and produces the action-event, $E_{A}(t_{i})\in\mathcal{E}_{A}$. This action-event goes into the possibly unreliable computational counterparts, $M(t_{i})\ (i\in[1,n])$, and produces an output-event at $t_{i}$. Finally, the outcome-event, $E_{O}\in\mathcal{E}_{O}$, produces successful (correct) outcome if one of the outputs of $M_{i}$ (or $M(t_{i})$) produces correct result for both these cases³³3We assume a fail-silent model here, where failure in any outcome implies discontinuation of that outcome – thereby it will not interfere with other correct outcomes and can possibly be distinguished from these correct outcomes..

Such design-level redundancy provisions can be captured from the functional specification-level as well. For example, we can formally represent the spatial and temporal redundancies (as shown in Figure 2) using the properties, $\mathcal{P}_{S}^{Srel}$ and $\mathcal{P}_{S}^{Trel}$, respectively, as follows:

Here, $\mathcal{P}_{S}^{Srel}$ asserts that, whenever $E_{I}$ is sensed then the action-event $E_{A}$ is asserted parallelly in $n$ execution units (denoted by the ${\tt[\sim n]}$ construct) within next ${\tt a}$ to ${\tt b}$ time-units. Similarly, $\mathcal{P}_{S}^{Trel}$ asserts that, whenever $E_{I}$ is sensed then the action-event $E_{A}$ is asserted $m$ times by multiple executions (denoted by the ${\tt[=m]}$ construct) within next ${\tt a}$ to ${\tt b}$ time-units. At this current setup, the reliability of the outcomes are also increased and these are represented as, $R_{E_{O}}^{Srel}=1-(1-R_{E_{O}})^{n}$ and $R_{E_{O}}^{Trel}=1-(1-R_{E_{O}})^{m}$, respectively.

Let us present an example to explain such functional correctness and reliability specifications.

In this section, we formally present the problem of reliability-aware resource estimation and illustrate the detailed resource allocation procedure.

In this section, the experimental results performed to check the scalability of this approach on an $8$-Core Intel Xeon Ivy bridge $E5-2650v2$ series processor ($20M$ Cache, $2.60GHz$) with $4\times 8GB$ RAM are presented. Figure 4 and  5 shows the 3D plots on the scalability experiments performed. We have used Z3 SMT solver [36] developed by Microsoft Corporation and CPLEX Optimizer (ILP solver) [19] developed by IBM. The time response of the proposed approach subject to varying sequential depth⁶⁶6The sequential depth of a property is the maximum number of cycles throughout which the property may span. and number of action-events were analyzed. The graphs depict exponential increase in execution time in determining the optimal resources as the sequential depth of the specifications increase. The time response with varying number of properties and varying number of action-events per property are also studied. This response also has exponential behavior as indicated in Figures 4-5.

In Figure 4, the responses of Z3 and CPLEX solvers are shown with respect to the variations in sequential depth of the properties. The Z-axis in all the graphs represents the time required to find the minimum number of resources in Micro-seconds. The X-axis indicates the sequential depth (varied upto $2000$ time units) and the Y-axis indicates the number of action-events in the specification (varied upto $50$). For smaller sequential depth, the variation in execution time with variation in the number of action-events is rather small. However, as the sequential depth increases, the execution time varies rapidly as the number of action-events increases. The increases in sequential depth also results in the increase in number of resource constraints. Moreover, the increase in number of action-events results in increase in the length and complexity of resource constraints as well. But for same number of action events, the number of timing constraints remains the same. The increase in number of resource constraints has higher impact in the increase of execution time than the increase in the length of resource constraints.

In Figure 5, the response of Z3 and CPLEX solvers are shown with respect to the variations in the number of specifications. The Z-axis in all the graphs represents the time required to find the minimum number of resources in Micro-seconds. The X-axis indicates the number of specifications (varied from $0$ to $200$/$500$) and the Y-axis indicates the number of action-events per specification (varied upto $80$/$100$). For smaller number of specifications, the variation in the execution time with the variation in number of action-events is rather small. However, as the number of specifications increases, the execution time varies rapidly. Here, the increase along the X-axis and Y-axis results in increase in the number of timing constraints. This increase in number of timing constraints can result in increase of the number of action-events and the number of specifications. There will be variation in the number of resource constraints, implied by both increase in the number of action-events as well as in the number of properties, since time of execution can vary in both these cases. Both X-axis and Y-axis has similar effects in increasing the length and number of resource constraints. Thus, the behavior is truly exponential in this case. The increase in timing constraints have lesser effect on the time of execution than the increase in the length/complexity of the resource constraints.

The satellite launch vehicle navigation, guidance and control (NGC) system is responsible for directing the propulsive forces and stabilizing the vehicle to achieve the orbit with the specified accuracy. The dispersions in propulsion parameters compared to expected values, variations of the estimated aerodynamic characteristics during the atmospheric flight phase, the fluctuating winds both at ground and upper atmosphere and a variety of internal and external disturbances during the flight can increase the loads on the vehicle beyond the permissible limit and also cause deviations in the vehicle trajectory from its intended path [41]. Under such environment, NGC system has to define the optimum trajectory in real time to reach the specified target and steer the vehicle along the desired path and inject the spacecraft into the mission targeted orbit within the specified dispersions while ensuring the vehicle loads remain within limits. NGC system is among the most crucial and challenging field in launch vehicle design. The objectives of a satellite launch vehicle NGC system include:

1. 1.

   Stabilization of the vehicle during its flight against various disturbance forces and moments due to aerodynamics, thrust misalignment, separation, liquid slosh, etc.

2. 2.

   Tracking the desired attitude of the vehicle so as to follow the desired trajectory with the specified accuracy to meet the final mission objectives.

3. 3.

   Receiving navigation data from sensors (navigation sensors) and desired attitude from guidance system and generating appropriate control commands.

Using the control commands generated by the autopilot system, the actuation system generates the necessary forces and moments to control and stabilize the vehicle as per the requirements. The inputs to the launch vehicle autopilot system are – navigation sensor data and health status, guidance data and health status, sequencing command execution status, feedback from vehicle autopilot filters, and feedback from Autopilot on the status of computation and validation.