Designing safety-critical cyber physical systems (CPS) was and remains a challenging task. CPS engineers are supposed to design solutions that are easy to modify, reusable, satisfy certification authorities, meet safety goals, separate between concerns, etc. With these partly contradicting demands it sometimes is even impossible to find a viable CPS design. The idea using contract-based design methods has been around for over two decades and enables automating the (re-)validation of the specification of CPS against the surrounding system or operational environment. In this work we extend the notion of contracts by component and interface contracts and give ideas on how to integrate them in a modular safety assurance approach. The explicit separation between these two types of contracts also better reflects the separation of concerns and reduces the overall modeling effort. We evaluate our approach with an automotive E-Drive case study.
When designing safety-critical cyber physical systems (CPS) we are dealing with a very difficult challenge. For a CPS, being safe means that the designer of that system must forsee everything that can lead to an unsafe situation. That being said, the designer not only has to install certain counter-acting mechanisms, increasing safety, he also must ensure that these mechanisms work correctly and that they actually increase the safety of that CPS. More precisely formulated, the designer of a safety-critical system has to guarantee its safety. ⋆ This work was supported by the Federal Ministry for Education and Research (BMBF) under support code 01IS12005M Copyright © 2015 by the authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors.
This fact is also mandatory when developing a system that has to be
compliant to safety standards like the ISO26262 [
Aside from the problem of ensuring the safety of embedded systems, there is another challenge in designing today’s CPS: The ever-growing complexity, caused by the inclusion of yet another new feature, greatly impacting the rest of the system. The last few decades saw tremendous effort to cope with this complexity as well as safety issues.
In order to master this complexity, we need to break it down to the essentials. There are many formalisms to model different aspects of complex safety-critical systems. One single formalism in isolation only represents a fraction of the actual system under design. While some of these formalisms in isolation are well understood, the combination of them turns out to be another challenge. The combination of different modelling aspects allows for more realistic representations of the actual embedded system. However, that also makes it harder to analyze the systems to assure certain properties of interest.
Safety requirements are fundamental artifacts in the specification of safetycritical CPS, as they document how the hazards and failure of the system are mitigated. They are produced by the hazard and safety analyses and may therefore suffice in various viewpoints and levels of abstraction. 1.1
Embedded systems are small computing systems deeply embedded into their
surroundings such that their existence is barely noticed. Since most embedded
systems are small devices reacting on changes in their environment the notion
cyber physical systems was coined to emphasize the necessity to take the
environment into account during design [
The intended control behavior and corresponding safety properties of CPS
can be specified with various formalisms. In this regard, the use of
contractbased modeling has proven to be beneficial [
Contracts represent a requirement in a structured way separating it into an assumption, stating the expected properties of the environment, and a guarantee, which describes the desired behavior of the component, provided the assumption is met by the environment. The introduced separation is the foundation for building a sound theory that allows the reasoning about the composition of systems in a formal way. Additionally, it reflects the very idea of CPS to explicitly consider the properties of the surrounding environment.
In this work we provide a method to distinguish between two contract types providing separation of concerns on the one hand and module decomposition and reusability on the other hand. This method may be applied in different domains allowing for the consideration of multiple aspects of CPS design and specification. In the context of safety-critical CPS design we describe how to integrate our proposed method into a modular safety assurance process. 1.2
Using Contracts for better specification of critical systems and partly for
improving safety analysis and verifications is currently a flourishing research domain.
For example, Safety ADD (see [
A tool for checking the refinement between contracts called OCRA
(Othello Contracts Refinement Analysis) was presented in [
A full range of safety mechanisms, such as, definitions of faults and failures,
fault containment, safety mechanisms, handling the degradation modes and safe
states at multiple abstraction levels is proposed in [
Temporal logic is also used in [
The paper is organized as follows: In Section 2 we give a basic overview over contracts-based design. Section 3 details our approach to differ component and interface contracts and how to apply them in a modular safety assurance process. We evaluate this approach with an automotive E-Drive case-study in Section 4. Finally, we conclude our paper in Section 5 and give an outlook.
In this section we will give a brief overview over contract-based design (informal and formal) and the pattern based RSL to specify contracts in a semantically sound way. In Subsection 2.3 we give a formal definition of the validation procedure that has to be performed in order to verify the correctness of contracts. Note that this procedure may differ in necessary effort or difficulty for different aspects. 2.1
Contracts are pairs consisting of an assumption (A) and a guarantee (G). The assumption specifies how the context of the component, i. e. the environment from the point of view of the component, should behave. Only if the assumption holds, then the component will behave as guaranteed. This kind of specification allows to replace components by more detailed ones, if they allow a less demanding environment, without re-validating the whole system. Thus, the system decomposition can be verified with respect to contracts without the knowledge of the concrete implementation. In this work, we use the RSL to specify the assumption and guarantee parts of contracts.
Assumption: a occurs each 50ms.
Guarantee: Whenever a occurs, b occurs during [5ms,8ms].
Assumption: a occurs each 50ms.
Guarantee: Whenever a occurs, c occurs during [10ms,14ms].
Assumption: b occurs each 50ms with jitter 8ms.
Guarantee: Whenever b occurs, c occurs during [5ms,6ms]. a
Subsystem A1
b System A
Subsystem A2 c
One advantage of using contracts is that they can help to decrease the complexity of verifying the implementation against its specification. For example, consider the system in Fig. 1, to which a contract is assigned. The system contract states, that the input port ’a’ is triggered each 50ms, and when it is triggered, the system has to respond by sending an event on port ’c’ within a specific time interval. The system is decomposed into two subsystems each with one contract, and some internal behavior modeled by, e. g. state machines. Assume that the functionality on subsystem A2 depends on the output of subsystem A1. Further, assume that the subsystems would not be annotated with contracts. Thus, to validate the contract of the overall system A, the composed behavior of both subsystems has to be computed, which generally leads to large state spaces. Using contracts for A1 and A2, we can omit the composition and validate the sub-contracts locally.
Formally, the semantics of a contract is defined as (1) where (X)Cmpl defines the complement of a set X in some universe U , and [[X]] is defined as the semantic interpretation of X. In our case, [[X]] is given in terms of sets of timed traces. A trace over an alphabet Σ is a sequence of events. Further, a time sequence τ is a monotonically increasing sequence of real values, such that for each t ∈ R there exist some i ≥ 1 such that τi > t. A timed trace is a sequence (ρ,τ ) where ρ is a sequence of events and τ a time sequence. The set of all timed traces over Σ is denoted by T r(Σ).
The specification S of a component is given in terms of a set of contracts, i. e. [[S]] := !n
i=1[[Ci]]. An implementation I of a component satisfies its specification S, if [[I]] ⊆ [[S]] holds. The refinement relation between two contracts C and C′ is defined as follows:
C′ refines C, if [[A]] ⊆ [[A′]] and [[G′]] ⊆ [[G]], (2) 2.2
Natural language requirements are often accompanied by ambiguity,
incompleteness or inconsistency; the reason for this resides in the very nature of a spoken
language. These unintended byproducts may not be detected until late phases of
the development process and therefore cause the realization to not fulfill the
intended goals of the specification or cause incompatibilities to other system parts.
A solution to this problem would be the use of formal languages to specify the
requirements. But these are often hard to understand and therefore difficult to use.
An alternative that bridges this gap is the pattern-based Requirements
Specification Language (RSL) [
Consisting of static text elements and attributes which are filled in by a requirements engineer, patterns have a well-defined semantic so that a consistent interpretation of the system specification between all stakeholders can be ensured. To cope with the needs of the different aspects of a design, various sets of patterns have been defined which are partly described in the following. 2.3
When a component is decomposed into a set of sub-components, we have to check whether the overall contract C = (A, G) (which also will be called global contract) and all subcontracts Ci = (Ai, Gi) (also called local contracts) for i ∈ {1, ..., n} are consistent. We have to check the following virtual integration condition: i) A ∧ G1 ∧ ... ∧ Gn ⇒
A1 ∧ ... ∧ An ii) A ∧ G1 ∧ ... ∧ Gn ⇒
G.
(3)
An in-depth discussion about virtual integration can be found in [
This section gives informal definitions of component and interface contracts. Furthermore, we describe how to transform them into each other and how to integrate them into a modular safety assurance process. The term multi-aspect thereby refers to the possibility to specify required properties concerning multiple views on the CPS (e. g. signal quality, timing, or reliability). 3.1
In contract-based design, contracts are used to systematically derive and document requirements and to conduct contract validation on the systems architecture. Such validation can serve as evidence for the correct allocation of functions which in turn constitute the overall function of a system, i. e. the allocation of the functions to a given CPS architecture and environment is correct and provably valid.
Component contracts are contracts between any system of consideration and
its operational context. Therefore, they are a key artifact in order to make
requirements allocated to a component modular and reusable, and to make
formerly tacit assumptions explicit. In the context of safety, contract-based
specifications aim at reasoning about the fault containment properties of components
in a modular, reusable way [
Fig. 2 depicts an excerpt of the architecture of an E-Drive system (more details in Section 4) and two exemplary contracts linked to the Microcontroller component. The functional contract e. g. states that under the assumption that the components power supply is sufficient and the temperature of the components environment is suitable, the component will start the calculation of the pWM signal within 5 milliseconds after the acceleration pedal has been pressed. A safety contract, focusing on failure propagation, states that the outputs of the Microcontroller component (shutOffSignal and pWM) will not fail, if the components input (phaseCurrentValue) or the component itself do not fail. These contracts are represented in a formal way using the predefined RSL (see Section 2.2).
Assumption: Always (Power = 12 V AND Temp_Env < 90°).
Guarantee: Whenever accelPedalPressed occurs, microControllerPWMCalc occurs within 5 ms.
Phase Current
Sensors phaseCurrent
Value
Microcontroller E-Drive
Assumption: None of {{phaseCurrentValue_fail}, {MicroController_internal_fail}} occurs.
Guarantee: None of {{shutOffSignal_fail, PWM_fail}} occurs. The relationship between assumptions of specific component to guarantees of its neighbors (and vice versa) can be defined by an interface contract. The difference to component contracts is mainly that assumptions refer to signal qualities provided at input ports of a component and promises refer to signal qualities provided at the output ports of the neighbor components. Interface contracts and component contracts can be transformed into each other canonically.
An interface contract is a combination or a pair consisting of an assumption
and a guarantee attached to the interfaces. Each contract is negotiated between
two respective neighbor components. Assumptions and guarantees may refer to
signal characteristics at a given port, as seen by an omniscient external observer,
e. g. the accuracy of a signal with respect to the real physical quantity, the
integrity of a signal, the delay of a port signal with respect to an event in the
outside world. It is obvious that some reusable component, taken out of its
environment, shall not refer to such context knowledge that is not directly related to
quantities observable at its direct interfaces - therefore the modularization to its
full extent is only achieved by later transforming interface contracts into
component contracts. Yet, interface contracts help verifying the architecture when
decomposing the system, because it can easily be checked along the signal flow
links whether or not the assumptions at the input of some component are fulfilled
by the guarantees at the linked output of its predecessor component. Unfulfilled
contracts, i. e. assumptions that are not satisfied by corresponding guarantees,
can be detected and highlighted automatically, which has been demonstrated by
a prototype tool in [
Ci-1 Guarantee: output.imprecision<10mA
Super Component
Ci
Ci+1 Assumption: input.imprecision<30Nm
Assumption: Contract input.imprecision<10mA
Guarantee:
output.imprecision<20Nm Contract
In order to use both types of contracts during the design of CPS, we propose
the following steps:
1. Let S be some CPS to be developed with its external interfaces, some
requirements (e. g. some signal to be provided with a required accuracy and
safety integrity, or an event to be triggered with a specified maximum delay
counted upon some internal condition, e. g. some failure condition) and some
assumptions about its environment. The job at hand is to decompose the
requirements and to allocate them onto the designated (sub-)components of
the system, thereby verifying that the refinement is correct.
2. The requirements engineer specifies the informal (textual) requirements
formally, or at least in a semi-formal notation, which allows to specify the target
properties unambiguously. A parametrized template language (like the RSL)
may be a semi-formal way to do so, temporal logics like LTL [
For the usage of component and interface contracts in an integrated safety process, we propose a three-step approach: – During conventional system design, functional requirements are analyzed and an initial system architecture is derived from these requirements. The architectural view allows for specifying system contracts, which cover in this step the decomposition and verification of the nominal behavior of the system. The system architecture is hence enriched by functional contracts. – The next step in the system engineering process is the safety analysis. The purpose of this analysis is to find failures, i. e. component behavior observable at the component interfaces that violates the specification of the nominal behavior and that might lead, if not handled appropriately, to some hazard or accident. The contracts defined in the previous step formalize the nominal behavior of the system, which aids in finding deviations. This means, that the failure mode definitions needed to aggregate different types of safety analysis, can be interpreted as contract violations: If, for instance, an output interface of some sensor component provides the value for a measured temperature and an interface contract promises for this output an accuracy of ±2◦C, then every value actually provided at the output which deviates from the true value by more than 2◦C is obviously considered as failure of the sensor component (to be precise, corresponding to failure modes “too high” or “too low” respectively, when applying the failure mode keywords known from the HAZOP analysis technique). The existing functional contracts together with the architecture design and the results of safety analysis serve as a basis to define safety contracts and thereby derive the functional safety requirements. – The final step in the safety process is to create the technical safety concept.
The systems architectural view is now updated to include additional safety components and mechanisms in addition to the system design, which may become necessary to detect and mitigate the identified component failures, or to achieve the required safety integrity level. To these new components, but also to the existing ones, additional contracts can be assigned, this time relating to safety properties. Examples for those properties can be promises for safety-relevant properties that hold with a defined safety integrity level or a minimum guaranteed probability, or the guarantee that despite certain failures at a component input, there will be no failures at its output (e. g. Assumption: Input can be any well-formed bus message; Guarantee: Output is an integer software variable either corresponding to the value transmitted by the bus message or the accompanying Boolean valid flag being set to FALSE.) Transforming such kind of safety-related interface contracts into component contracts leads to the formulation of the related technical safety requirements. As a result, the system architecture showing the nominal behavior design is enriched towards the final system safety architecture. 4
We evaluated our approach by applying the component and interface contract
modeling to an automotive E-Drive case study that has been introduced in [
Besides the architecture of the E-Drive, Fig. 4 also shows interface contracts (located on the left and right hand side above the architecture) as well as a component contract for the Microcontroller component (located in the center above the architecture).
Assumption: Microcontroller. phaseCurrentValue.
imprecision 1mA
Contract Guarantee: PhaseCurrentSensors. phaseCurrentValue. imprecision 1mA
Phase CurrentSensors E-Drive
Assumption: Temp_Env 90° Guarantee: Microcontroller.phaseCurrentValue. imprecision 1mA => Microcontroller.shutOffSignal. occurenceTime 100ms.
Microcontroller phaseCurrent CurrentPlausibility
Value Check
TorqueController
For this case study the interface contracts have been modeled along the signal flow from the Phase Current Sensors via the Microcontroller to the Emergency Shut-Off component. They specifically state which condition the signal property does fulfill or has to fulfill like for example the guarantee of the Phase Current Sensors output. This guarantee states that the imprecision of the phase current value is not allowed to exceed one milliampere. Following the signal flow, the next component to process the signal is the Microcontroller. This component itself has requirements regarding the input signals, which are stated as an assumption. In this case the component also demands the phase current value’s imprecisions to not exceed one milliampere. This pair of guarantee and assumption constitutes an interface contract between the two components regarding the phase current value’s imprecisions.
The same procedure was performed for the shut-off signal sent from the Microcontroller to the Emergency Shut-Off component (right hand side of Fig. 4). For this case, analyses like a compatibility check can be performed. Applying this kind of analysis to our case study showed that the compatibility between the components along this signal flow was given.
In the next process step the interface contracts were used to derive the component contracts for the components of the E-Drive system. The result, the component contract for the Microcontroller is depicted in the top center of Fig. 4. As can be seen the guarantee was derived by the previously defined assumption and guarantee of the Microcontroller, stating that if the left hand side of the implication is fulfilled, the right hand side can be guaranteed. The assumption in the example was added to state that the Microcontroller can just guarantee its correct functionality for an environmental temperature not exceeding 90◦Celsius.
The evaluation of the approach showed that besides the fact that forcing the engineer to capture requirements in a more structured and ultimately a more formal way decreases the ambiguity of the specification. Interface as well as component contracts enable analyses to validate the specification against the system context or the operational environment. Additionally, these approaches support a modular safety assessment by encapsulating the assumptions and guarantees relevant for the component that shall be changed or replaced. 5
Coping with specifications for CPS and validating them is a regular task that needs to be performed during system design. This paper described a new method to apply contract-based design in the context of a modular safety assurance process. We therefore distinguished between component and interface contracts to better support the system architect in validating the correctness of his design (including the specification and the structural composition). We evaluated our approach using an automotive E-Drive case-study which also showed an improvement in the usability and applicability of contracts in general. Future work will be conducted in the field of multi-aspect validation and verification of inseparable properties of CPS. There are still a lot of design concerns that have not yet been formalized or addressed at all. Optimizing one or more properties of interest (e. g. reduce costs, maximize safety, . . . ) is another topic which we will look into.