Information Technology Reference
In-Depth Information
ambiguities in the standard for user-defined data types and defined a proper compat-
ibility criteria. Like the adaptation approach in the automotive domain (Adler et al
(2011)), this work considers only a type system. However, the approach verifies not
only compositions, but also the use of variables in IEC 61131-related languages.
In the last few years, several research projects have begun to handle the topics
of compositional verification (SPEEDS (2006-2012)), (COMPASS (2011-2014)),
(SAFECER (2011-2015)) by formalizing system models (component models) and
languages for specification of contracts. These approaches share many concepts, es-
pecially contract-based design and formal behavioural verification of compositions.
Although our model is conceptually very similar, it differs in that it considers the
data semantics of property values, and it addresses a specific type of component-
based systems in which data semantics can be used to express the validity criteria
for compositions.
6Conluion
In this paper, we presented a method for the verification of compositions in
component-based systems. The components modelled here are enriched with prop-
erties, which describe the data semantics of components. The novelty of our ver-
ification lies in representing the composition along with modelled properties as a
Constraint Satisfaction Problem (CSP), which allows us to achieve two important
objectives. First, using relational, logical and more advanced operators on data,
many types of properties can be supported. Second, for properties that use basic
logical and arithmetic operators, the verification can scale up to several hundreds
of components, each of them consisting of few tens of properties, which makes the
approach promising for the use in practice.
As part of our ongoing work, we want to characterize the runtime performance
based on different types of properties, since they impact the scalability at most. In
addition, we also want to investigate other parameters such as solver search policy,
solver engine, etc., in order to find best configuration for the verification method.
References
Adler, R., Schaefer, I., Trapp, M., Poetzsch-Heffter, A.: Component-based modeling and ver-
ification of dynamic adaptation in safety-critical embedded systems. ACM Trans. Embed.
Comput. Syst. 10(2), 20:1-20:39 (2011),
doi:10.1145/1880050.1880056
de Alfaro, L., Henzinger, T.A.: Interface automata. SIGSOFT Softw. Eng. Notes 26(5), 109-
doi:10.1145/503271.503226
Apt, K.: Principles of Constraint Programming. Cambridge University Press, New York
(2003)
Search WWH ::
Custom Search