Information Technology Reference
In-Depth Information
Constraint-Based Verification of Compositions
in Safety-Critical Component-Based Systems
Nermin Kajtazovic, Christopher Preschern, Andrea Holler, and Christian Kreiner
Abstract.
Component-based Software Engineering (CBSE) is currently a key
paradigm used for building safety-critical systems. Because these systems have to
undergo a rigorous development and qualification process, one of the main chal-
lenges of introducing CBSE in this area is to ensure the integrity of the overall
system after building it from reusable components. Many (formal) approaches for
verification of compositions have been proposed, and they generally focus on be-
havioural integrity of components and their data semantics. An important aspect of
this verification is a trade-off between scalability and completeness.
In this paper, we present a novel approach for verification of compositions for
safety-critical systems, based on data semantics of components. We describe the
composition and underlying safety-related properties of components as a Constraint
Satisfaction Problem (CSP) and perform the verification by solving that problem.
We show that CSP can be successfully applied for verification of compositions for
many types of properties. In our experimental setup we also show how the proposed
verification scales with regard to size of different system configurations.
Keywords:
component-based systems, safety-critical systems, compositional veri-
fication, constraint programming.
1
Introduction
Safety-critical systems drive the technical processes in which failures can cause
catastrophic consequences for humans and the operating environment. Automotive,
railway and avionics are exemplary domains here, just to name few. In order to
Search WWH ::
Custom Search