Information Technology Reference
In-Depth Information
(Kindel and Friedrich (2009)). However, it is still possible to support these config-
urations, since each such sub-system can be provided to verification independently,
and also, not all components are massively interconnected as in Figure 5. For exam-
ple, the simplified system from Figure 1 is modelled using 13 software components
(is just one option to realize that system).
5
Related Work
Now we turn to a brief overview of related studies. We summarize here some rele-
vant articles that handle compositional verification based on data semantics.
Similar problems to those described in our problem statement were identified by
Sun et. al (Sun et al (2009)) in their work on verifying the composition of analogue
circuits for analogue system design. In their approach, each analogue element (re-
sistor, capacitor, etc.) is characterized by its performance profile and this profile is
used to build the contract; that is, for certain values of the inputs the element re-
sponds with certain output values. Using contracts made from performance profiles,
it was possible to eliminate many integration failures early in the system design
phase. These structural compositions of analogue elements are very similar to the
compositions in CBSE. However, the model of Sun et al. only considers connections
between elements (horizontal relations).
Another article describes a runtime framework for dynamic adaptation of safety-
critical systems in the automotive domain (Adler et al (2011)). In the event of fail-
ures or degradation of quality, the intent is to reconfigure the automotive system
while it is operating. In contrast to the previous approach, the compositional verifi-
cation in this case is based on a common quality type system shared among compo-
nents. Two components can form a composition only when their interfaces or ports
have the compatible type qualities. In this way, wrong type castings between com-
ponents can be avoided. However, using a type system in our case would just verify
the syntax but not the semantics of data (i.e. the concrete values).
A more advanced framework for dynamic adaptation of avionics systems was
developed by Montano (Montano (2011)). The goal is to adapt the system to new,
correct configurations, in case of failures. To perform this, a common quality system
defines the contracts between functions and available static resources (e.g. memory
consumption, CPU utilization, etc.) and in this way it restricts the possible set of cor-
rect configurations. An important aspect of this work is that it demonstrates the CSP
approach to solving the composition problem. However, the quality type system
only considers static resources, and does not consider contracts between functions.
Ultimately, the approach is strongly focused on dynamic adaptation with human-
assisted decision making.
In the field of industrial automation, the authors in (de Sousa (2012)) propose
the static verification of compositions based on data types of the IEC 61131-3
component model (or standard). This model defines the standard data types but it
also allows definition of customized data types (derived from existing ones) and
combination of existing data types into complex structures. The authors identified
Search WWH ::
Custom Search