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

3.1 General: Components and Compositions

In our system, we define a component M as follows:

Σ M c

in out par

M : = , Σ , Σ , (1)

in , out ,and par

,where Σ Σ Σ are inputs, outputs and parameters respectively (i.e.

Σ -alphabets define input, output and parameter variables in terms of datatypes, val-

ues, and some additional attributes), whereby M c is an optional set of contained
components, and is defined according to relation (1). To clarify this, we distinguish
between following two types of components:

• Atomic components : components that can not be further divided to form hierar-

chies, i.e. components for which M c =

0. They perform the concrete computation.
The Ignition System for example may contain many atomic components, such as
integrators, limiters, simple logical elements and other.

• Composite components : hierarchical components that may contain one or more

atomic and composite components, i.e. M c = 0. Note that we use the term com-

position to indicate composite components, which also may represent a complete
component-based system (cf. our system in Figure 1).

The component model introduced above is typical for data-flow systems such as
the ones modelled in the Matlab Simulink for example. Similar models are used
when considering properties for resource budgets (Benveniste et al (2012)).

3.2 Modelling Compositions Enriched with Properties

As illustrated in Figure 1, properties are defined as expressions over component
variables. In order to be able to interpret these expressions during the verification,
we formulate them in a SMT form 3 : each expression can be represented in terms of
basic symbols, such as 0 min . Using this form, various expres-

sions can be supported for our system, including logical, arithmetic, and other. The
property from Figure 1 for instance,

, 1 , ... s en , ..., + ,−,/,...

( 0 ≥ s en ≤ 6400 ) ∧ ( 0 ≥ f fl ≤ 100 ) , conforms

to the SMT form.
In order to link properties throughout the system hierarchy with regard to three
basic relations introduced in Section 2.2, we encapsulate them in assume/guaran-
tee (A/G) contracts. According to the general contract theory in (Benveniste et al
(2012)), a contract C is a tuple of assumption/guarantee pairs, i.e.:

C : = Σ , A , G , (2)

where A and G are expressions over sets of variables . In this way, we can split

properties for each component in (a) part that has to be satisfied, i.e. assumptions ,
and (b) part that is guaranteed if assumptions hold, i.e. guarantees . For example, the

Σ

3

Syntax in SMT (Satisfiability Modulo Theories) allows to define advanced expressions,
e.g. on integers, reals, etc.