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

make these systems acceptably safe, their hardware/software engineering has to be
rigorous and quality-assured.
Currently, rapid and continuous increase of system's complexity is one of the ma-
jor challenges when engineering safety-critical systems. For instance, the avionics
domain has seen an exponential growth of software-implemented functions in the
last two decades (Butz (-)), and a similar development has also occurred in other do-
mains with a focus on mass production (Kindel and Friedrich (2009)). In response,
many domains have shifted towards using component-based paradigm (Crnkovic
(2002)). The standards such as the automotive AUTOSAR and IEC 61131/61499
for industrial automation are examples of widely used component systems. This
paradigm shift enabled the improvement in reuse and reduction of costs in devel-
opment cycles. In some fields, the modularity of the system structure is utilized to
distribute the development across different roles, in order to perform many engineer-
ing tasks in parallel (e.g. the automotive manufacturers are supplied by individually
developed middleware and devices which can run their applications).
However, the new paradigm also introduced some new issues. One of the ma-
jor challenges when applying CBSE is to ensure the integrity of the system after
building it from reusable parts (components). The source of the problem is that
components are often developed in the isolation, and the context in which they shall
function is usually not considered in detail. In response, it is very difficult to localize
potential faults when components are wired to form a composition - an integrated
system (G ossler and Sifakis (2005)), even when using quality-assured components.
The focus of the current research with regard to this problem is to enrich compo-
nents with properties that characterize their correct behavior for particular context,
and in this way to provide a basis for the design-time analysis or verification 1 of

compositions (Clara Benac Earle et al (2013)).
This verification is also the subject of consideration in some current safety stan-
dards. For instance, the ISO 26262 standard defines the concept Safety Element out
of Context (SEooC), which describes a hardware/software component with neces-
sary information for reuse and integration into an existing system. Similarly, the
Reusable Software Components concept has been developed for systems that have
to follow the DO-178B standard for avionic software. These concepts both share the
same kind of strategy for compositional verification: contract-based design. Each
component expresses the assumptions under which it can guarantee to behave cor-
rectly. However, the definition of the specific contracts, component properties and
validity criteria for the composition is left to the domain experts.
From the viewpoint of the concrete and automated approaches for compositional
verification and reasoning, many investigations have focused on behavioural in-
tegrity, i.e. they model the behaviour of the components and verify whether the
composed behaviours are correctly synchronized (de Alfaro and Henzinger (2001)),
(Basu et al (2011)). On the other side, compositions are often made based on data
semantics shared between components (Benveniste et al (2012)). Here, the correct
behaviour is characterized by describing valid data profiles on component interfaces.

1

In the remainder of this paper, we use the term verification for static, design-time verifica-
tion (cf. static analysis (Tran (1999))).