Embedded software systems are highly configurable and consist of many software components in different variants and versions. However, component updates or upgrades often result in unpredictable incompatibilities with its environment. Existing research addresses this challenge by employing formal methods with a fixed set of encoded static compatibility checks, making it nearly impossible for engineers to add new or modify existing ones. This paper presents a highly adaptable infrastructure to define constraints for compatibility checks. The underlying approach transforms software components into instances of a C&C meta-model, enriched with OCL compatibility constraints at runtime, then evaluated by a solver. The result is transformed back into a C&C model showing compatibility or incompatibility. The easy to integrate infrastructure is based on industrial requirements and allows to add, modify or delete constraints without restarting the tool infrastructure.
Software systems for embedded devices are highly configurable consisting of a
variety of components in different variants and versions [
ECU_V1 «turn off urea amount if speed sensor > 135» urea amount changed constraint
ECU_V2
«turn off urea amount
if speed sensor > 125»
on a counter-example [
Next is an example in Sec. 2 which is followed by a set of industrial requirements in Sec. 3. Sec. 4 introduces the tools and languages used by the infrastructure proposed in Sec. 5. Sec. 6 describes the technical realization. Finally, Sec. 7 and Sec. 8 compare our approach to existing work and conclude this paper. 2
As a motivating example, we use a simplified emission control system as used in automotive industry. The Electronic Control Unit (ECU) has an input for the pressure value of the exhaust system, a speed sensor for the current velocity, and an oxygen sensor. Using these values, the urea amount is triggered to clean emissions. Now a team of developers is responsible to develop a new version of the controller to maximize gas mileage. In this context, ECU V2 has been developed. It has the same ranges for all input ports but the constraint when to turn off the emission control has been changed from 135 km/h to 125 km/h (see Fig. 1).
Due to varying regulations in different countries (in Germany the emission control can be turned off if the speed is greater 120 km/h, whereas in the US it can be turned off if speed is greater 128 km/h), a developer team member is unsure if the new version can be used in the US and in Germany. Her doubts are justified: on the component’s type level the different versions seem to be compatible. However, due to the additional constraint they are not. In particular, for the German market, the newer version is compatible (requires a turn off if speed > 120 km/h), whereas in the US the new version is not compatible because the emission control is turned off too early. Our proposed solution does not only allow to check such compatibilities between different component versions, but it also allows to dynamically en-/disable OCL constraints, e.g. local market regulations such as emission control, during tool runtime. 3
The proposed approach is developed with respect to a set of requirements, which are derived from the SPES XT project1. They indicate that a differentiation be1 http://spes2020.informatik.tu-muenchen.de/spes_xt-home.html tween engineers (who are using the toolchain) and developers (who are extending the toolchain), is required. Subsequently, a set of the main requirements is introduced:
(R1) Compatibility constraints have to be defined in comprehensive and concise notation: Most engineers are only familiar with Java- or C-like syntax. Therefore, specifying constraints must hide all model-checking aspects.
(R2) The tool should support heterogeneous C&C architecture models: Since in industry various C&C architectures including third party plugins or in-house developments are used, the tool should be easily extendable.
(R3) Developers should be able to modify structural compatibility constraints: Compatibility rules must be adaptable instead of hardwire them to support different local markets and to be flexible for changing laws.
(R4) Meaningful and model related error messages: Reported violations must be easy to comprehend for engineers, having no deep knowledge of formal methods. Therefore, expressive descriptions relating to source C&C models should point to components being affected with incompatibility.
(R5) C&C model files should not be modified: The tool should also derive compatibility statements (probably weaker ones, because of missing information) between older (without touching them) and newer Simulink models.
(R6) Compatibility checking should be easy for engineers: A seamless integration into existing C&C modeling tools such as Simulink should be supported. 4
The realization of the proposed approach is based on the MontiCore (MC)
framework [
A language family, realized with the MC framework, is the UML/P language
family [
An approach has been developed to check for structural compatibility of two components, which satisfies the requirements described in Sec. 3 and is based
➁ metamodel.cd «consistent» «instantiation» compatibility.ocl «uses» V1.od V2.od ➈ ccoouunnteterErExxaammppl eleN1..oodd ➇ eerrrororMrMeessssaaggeeN1..ttxxtt plug-in points ④ ④ ➂ ➂ eerrrroorrCClalassssN1..ooccll eerrrororCrCl alassssN1..ssmmtt22 q u e .r y s m t 2 metamodel.smt2 compatibility.smt2
➄ ➆
V1.smt2 V2.smt2 ➄ ➄ ➄ ➄
➅ answer.smt2
V1.slx V2.slx ➀ ➀ ccoouunnteterErExxaammppl eleN1..mm
➉
counterExample.slx
on C&C architectures and user-friendly (R1) constraint modeling language. The
proposed approach, shown in Fig. 2, is composed of five plug-in points, which
enable dynamic support for different modeling languages such as Simulink ,
TargetLink and Modelica and solvers such as Alloy [
The numbers (1) to (10) in Fig. 2 represent the processing steps: (1)
transforms C&C input models to ODs, which are an instantiation of the meta-model
for all well-established and commonly used C&C modeling languages. More
information about this meta-model can be found in one of our previous work [
The toolchain is divided into a C&C Engineer Frontend, a MC Developer
Frontend, and a Solver Backend, each of which addressed by either an
automotive engineer modeling Advanced Driver Assisted System (ADAS) functionality
(gray-slashed artifacts) or a quality control/assurance (QA/QC) developer
specifying compatibility constraints and different error classes (gray-lined artifacts).
Engineer View The automotive engineer initiates the compatibility check in
Simulink (R6), therefore the engineer must not learn a new tool. The result
annotated with error descriptions is presented as a Simulink model (R4), since
the engineer already knows Simulink with its syntax and semantics, thus, he
is able to understand the error messages. The witness generation algorithm is
based on previous work done by Ringert [
Developer View The developer defines compatibility constraints and
counterexamples as well as additional regional constraints as presented in Sec. 2 in
OCL/P using the MC developer frontend. These counterexample specifications
are used to generate useful feedback for automotive engineers in case of
component incompatibility as shown in Fig. 3. Fig. 4 illustrates how MC transforms
OCL/P code to SMT code for use with the Z3 solver. A more detailed textual
description of the code and how a counterexample in OCL/P looks like can be
found in [
The overall performance of this approach mainly depends on the generator. In particular, how it generates solver-specific code from the UML/P language family artifacts. Since our motivating example is too small, a bigger model comparing interface compatibility of two ADAS is taken from the SPES XT project. Tab. 12 shows the impact of the generator where model A is compatible to model B, and model A has 126 components as well as model B has 97 components. Note that all artifacts are translated into SMT code using different generator strategies, and then evaluated by Microsoft’s Z3 solver.
This table underlines that the verification execution time mainly depends on the optimizations implemented by the generator. The difference between the 2nd and 3rd column is that in the 2nd one no simplify constraints had been generated and the 3rd one added the simplify solve-eqs smt command to the generated SMT code. Due to the highly customizable toolchain infrastructure providing several plug-in points, it is possible to integrate different optimization steps. Tab. 1 also shows that it was a good idea to introduce CDs and OCL constraints as intermediate layer, because this layer is independent of all solver specific optimizations; translating Simulink models directly to SMT code and formulating the compatibility constraints directly in Z3 code would probably result in changing them all the time and polluting the model with solver strategy annotations just for performance reasons - which would make them very hard to read and nearly impossible to reuse at the end. model time [s] time* [s] change in generated Z3 code m1 timeout 10.08 m2 126.68 10.44 remove custom datatypes m3 93.55 12.86 change encoding of meta-model m4 138.38 10.47 use ite (if-then-else) instead of implies after quantifier m5 70.74 8.34 replace enumeration datatypes by integers m6 19.05 4.33 replace id hash with an unique id starting at zero m7 15.17 4.23 remove unnecessary ites when translating OCL to Z3
In the first version (m1) the meta-model, the ODs and the OCL constraints were nearly one by one translated to SMT code. The result was quite readable SMT code, as this code shows for the Connector element, which connects a source port, (List Name) represents its full qualified name, with a target port (see Fig. 5). Note that accessing some parts of a C&C model element could also be done very intuitively, e.g. (source con) where con is a Connector variable.
In the last generated model version (m7) all meta-model element structures were flattened to integers. This means there is no such Connector element in Z3 code; instead of every element is represented by an unique id and accessing a C&C element part is now done by accessing a function (see Fig. 5). Additionally, all names, e.g. port names, have been replaced by an unique integer. 2 measured by Nicolai Strodthoff in his bachelor thesis 1; meta-model definition 2(declare-datatypes () ((Connector (mk-connector (source (List Name)) 3 (target (List Name)) (id ID))))) (code is an excerpt) 4; instance creation 5(mk-connector (insert n_switch1 (insert n_out1 nil)) 6 (insert n_mul (insert n_in2 nil)) id_1593458942) 1(define-fun getConnectorSourceFromId ((id Int)) (List Int) 2(declare-datatypes () ((Connector (mk-connector (source (List Name)) 3 (ite (= id 2) (insert 2 (insert 56 nil)) 4 (ite (= id 14) (insert 0 (insert 56 nil)) The entire post-processing step such as flattening data structures and replacing names by integer number is done by using the plug-in point (5) in Fig. 2 after all documents have been merged to one query document. The last optimization from m6 to m7 used the plug-in point (6) by removing ites in Boolean OCL constraints. The code (ite cond1 true (ite cond2 false (ite cond3 true ...)) true) will be replaced by (or cond1 cond3 ...).
This study shows that the modular and extendable architecture supports flexibility, i.e., replace the Z3 solver with another one like Alloy, and adaptations of generator algorithms to optimize performance. 7
Besides our toolchain, there exist several frameworks for compatibility
analysis. We want to mention here six representatives: (1) Dajsuren’s architectural
framework [
Update of software components are very unpredictable due to different versions, variants, and configuration options. Based on a set of industrial requirements and on running example, a highly adaptable infrastructure to check compatibility constraints is presented. It is based on a generic meta-model and employs OCL at runtime, which allows high customizability and heterogeneous support for C&C architectures. The underlying approach supports different requirements of engineers and QA/QC developers to satisfy future infrastructure extensions and provide a user friendly witness-based error interface.