Information Technology Reference
In-Depth Information
In both cases, many properties can be required to describe a single component and
therefore scalability of the verification method is crucial here.
In this paper, we present a novel approach for verification of compositions based
on the data semantics shared between components. We transform the modelled com-
position along with properties into a Constraint Satisfaction Problem (CSP), and
perform the verification by solving that problem. To realize this, we provide the
following contributions:
•
We define a component-based system that allows modelling properties within a
complete system hierarchy.
•
We define a structural representation of our modelled component-based system
as a CSP, which provides us a basis to verify the preservation of properties.
•
We realize the process that conducts the transformation of the modelled
component-based system into a CSP and its verification automatically.
The CSP is a way to define the decision and optimization problems in the con-
text of Constraint Programming paradigm (CP) (Apt (2003)). Using this paradigm
for our component-based system, many types of properties can be supported. Also,
various parameters that influence the scalability of the verification can be controlled
(used policy to search for solutions for example). In the end of paper, we discuss the
feasibility of the approach with regard to its performance.
The remainder of this paper is organized as follows: Section 2 describes the prob-
lem statement more in detail and gives some important requirements with regard to
modelling a system. In Section 3 the proposed verification method is described. Sec-
tion 4 describes the experimental results. A brief overview of relevant related work
is given in Section 5. Finally, concluding remarks are given in Section 6 .
2
Problem Statement
Properties are an important means to characterize functional and extra-functional as-
pects of components. Safety, timing and resource budgets are examples here, just to
name few (Sentilles et al (2009)). Recently, they get more and more attention in the
safety community, since efficient (an practical) reuse methods are crucial in order
to reduce costs in development cycles and costs for certification of today's safety-
critical systems (i.e. their extensive qualification process). In this section, we give
an insight into the main challenges when using properties to verify compositions,
and based on these challenges, we outline the main objectives that we handle in this
paper.
2.1
Motivating Example
In our work, we address properties that in general describe data semantics. To clar-
ify this, let us consider now the example from Figure 1. The system in this figure
shows the composition of four components that form the automotive engine control
application on a higher abstraction level. The basic function of this application is
Search WWH ::
Custom Search