Constraint-Based Verification of Compositions in Safety-Critical Component-Based Systems - Software Engineering, Artificial Intelligence, Networking and Parallel/Distributed Computing - page 112

a specification is given in Figure 1, bottom. Here, the context for the component Ig-
nition System is defined in terms of the syntax and semantics related to component
inputs, outputs and parameters. With the properties shown below, the concrete be-
havior can be roughly described - in this example, for certain intervals of inputs,
the component can guarantee that the output t ig lies within the interval ]

(note that pseudo syntax is used here). When building compositions based on such
properties, the developer has to consider their influence on the remaining, depen-
dent components - in this case, it has to be decided whether the M IIAS component
can accept such values of the t ig and what should components M FS and M AFS pro-
vide so that higher delay than 40 ms between t ig and t in can be achieved. This can be
very tedious and error prone task when doing it manually, because of the following
reasons:

[ 50 , 150

• Many components may be required to build a complete system, depending

on their granularity. For example, current automotive systems comprise sev-
eral hundreds of components, and many of them may depend on each other
(Kindel and Friedrich (2009)).

• Some components that directly influence the safety-critical process are usually

certified, i.e. developed according to rigorous rules from safety standards. Be-
cause of costs for such a certification, the practice is to develop components for
different context and to certify them just once (e.g. to support different engine
types in our example). In response, many properties have to be defined for a
single component to capture all context information.

The main problem here is how to define and to inter-relate all properties thorough
the complete system hierarchy in a way that the preservation of properties of all
components can be verified automatically? Another problem is how to complete
with such a verification in a ”reasonable time”?

2.2 Modelling and Verification Aspects

To narrow the problem statement above, very important prerequisite to structure
properties within a system hierarchy consistently is to define basic relations among
them. For example, properties of the component M IS are related with properties
of the component M IIAS , because of direct connections between their output and
input variables. On the other hand, properties of all four components influence the
semantics of the mentioned top-level property. We summarize different types of
these relations as following:

• Composition : hierarchical building of composed properties based on their con-

tained properties (e.g. the top-level timing property is composed of properties
contained in components M AFS , M IS , M FS and M IIAS ). We discuss this later in
more detail.

• Refinement/abstraction : properties characterize the component behaviour at cer-

tain abstraction level. With refined properties, more specialized behaviours can