Keywords

1 Software Tools in Model-Based Systems Engineering

Model-driven engineering plays an increasingly important role in the design of critical embedded and cyber-physical systems in various application domains including automotive, avionics or telecommunication. Advanced design and verification tools aim to simultaneously improve quality and decrease costs by early validation to highlight conceptual design flaws well before traditional testing phases in accordance with the correct-by-construction principle. Furthermore, they improve productivity of engineers by automatically synthesizing different design artifacts (source code, configuration tables, test cases, fault trees, etc.) necessitated by certification standards (like DO-178C or ISO 26262).

There are two main trends nowadays in the software tool market of systems engineering. On the one hand, certain market shares are dominated by very few industrial tools (e.g. Matlab Simulink, Dymola, MagicDraw, DOORS) each of which typically supports a specific development stage (requirements engineering, simulation, allocation, test generation, etc.). In order to protect the important intellectual property rights, these tools are of closed nature, which implies such huge tool integration costs for system integrators (like airframers or car manufacturers) that can easily exceed the total licensing costs of individual tools. On the other hand, recent initiatives (like PolarSys) have started to promote the development of open language standards and the systematic use of open source software components in tools for critical systems to reduce licensing costs and the risks of vendor lock-in.

When software tools are used for developing a critical system, the tools themselves need to be validated with the same scrutiny as the system under design by software tool qualification, especially, when no further human checking is carried out on the outputs of such tools. Software tool qualification distinguishes between design tools which, by definition, may introduce new errors to the system and verification tools which may fail to reveal existing errors of the system.

Unsurprisingly, software tool qualification is extremely costly due to the high algorithmic complexity, tightly couple architecture and unexpected feature interaction of such tools. In fact, most companies rather opt for using tools just as aids to highlight errors quickly and then they carry out the traditional verification& validation process with thorough simulation and testing. Anyhow, systematic software engineering techniques to simultaneously improve quality and reduce the costs of software tool qualification would be highly beneficial. Existing software engineering practices may guarantee the quality of the system itself, but they frequently fail to ensure the quality of the software tool used in systems engineering. Furthermore, the rapid increase in the size and complexity of systems models introduces significant scalability challenges for these tools.

Language engineering aims to provide foundations, techniques and tools for domain-specific modeling languages to capture the models. Model transformation engineering aims to systematically develop queries and transformations used in automated code generators, debuggers to process these models. Of course, a seamless integration of these techniques is needed when developing real tools.

In this paper, I overview two open source Eclipse projects supporting model query and transformation techniques integrated into in various industrial tools for model-based systems engineering. EMF-IncQuery is an incremental model query framework while Viatra supports reactive, event-based transformations. Their scientifically well-founded basis enables semantic integration of different tool features to (i) complement structural integration provided by the component (plugin) architecture of Eclipse and to (ii) support tool qualification by precise specification and execution semantics of those features.

2 Incremental Model Queries in EMF-IncQuery 

EMF-IncQuery is an open source Eclipse projectFootnote 1 to define declarative graph queries over EMF models [33] without manual coding and execute them efficiently using incremental graph pattern matching techniques over an imperative programming language such as Java. The benefits of EMF-IncQuery include:

  1. (i)

    a high-level and powerful declarative graph query language [8, 39];

  2. (ii)

    a highly efficient incremental query engine capable of evaluating queries over models with millions of elements [7, 39];

  3. (iii)

    an advanced integrated development environment [39] to construct and validate model queries supported by state-of-the-art Xtext tooling.

  4. (iv)

    its modular architecture enables easy integration with existing EMF-based modeling tools [39].

The primary use case for model queries is to support the live validation of well-formedness constraints and design rules of a domain in order to highlight and report inconsistencies as soon as they are introduced. Efficient incremental evaluation is based on adapting Rete networks [13] to change notifications sent by EMF-based models. Additional main use cases include advanced support for incremental calculation and maintenance of base model indexers [39], derived features [26], soft traceability links [14], or incremental view maintenance [12].

Detailed scalability assessment of EMF-IncQuery is carried out in numerous papers for validation of well-formedness constraints [7, 39], detection of source code anti-patterns [40] or maintenance of soft traceability links [14] over models with 10 million elements. Ongoing development within the MONDO European projectFootnote 2 aims to develop a distributed and incremental query engine [30] deployed over cloud based storages to further improve scalability.

Example. The definition of a sample well-formedness constraint (taken from [20]) for checking valid allocations of application instances to host instances (e.g. in a cloud application or a cyber-physical system) is listed in Fig. 1. The query notAllocatedButRunning captures an erroneous situation for allocation when an application app is running, but not allocated to a host instance (using another graph pattern allocatedApplication by negative composition). When checking this constraint on the instance model depicted in Fig. 2, app2 is the only ApplicationInstance which matches the pattern (thus violates the constraint) since app1 is allocated to a host instance ht1 while app3 is stopped.

Fig. 1.
figure 1

Sample queries for well-formedness constraints (adapted from [20])

Full size image
Fig. 2.
figure 2

Sample instance model

Full size image

By using a @Constraint annotation, EMF-IncQuery will automatically integrate the query into a model editor using the Eclipse Modeling Framework (EMF) [33] as underlying model representation. As a result, an error marker will immediately be placed on the model whenever this consistency constraint is violated, which is removed automatically once the source of the problem is corrected (e.g. the application instance is stopped or allocated to a host instance).

3 VIATRA: A Reactive Transformation Platform

Viatra is a reactive, event-driven model transformation platform [6] where transformations are executed continuously as reactions to changes of the underlying model. The Viatra projectFootnote 3 provides:

  1. (1)

    An internal domain-specific language over Xtend [38] to specify both batch and event-driven, reactive transformations.

  2. (2)

    A complex event-processing engine [11] over EMF models to specify reactions upon detecting complex chains of events.

  3. (3)

    A rule-based design space exploration framework [4, 15] to explore design candidates as models satisfying multiple criteria over states and trajectories.

  4. (4)

    A model obfuscator to remove sensitive information from a confidential model (e.g. to create bug reports).

Viatra adopted the principles of reactive programming [5]. The core concept of reactive programming is event-driven behavior: components are connected to event sources and their behavior is determined by the event instances observed on event streams. Compared to sequential programming, the benefits of reactive programming are remarkable especially in cases when continuous interaction with the environment has to be maintained by the application based on external events without a priori knowledge on their sequence.

The specification of a Viatra transformation program contains (1) rule specifications consisting of model queries, which serve as a precondition to the transformation, and actions, which typically prescribe model manipulations. Furthermore, (2) execution schemas are defined in order to orchestrate the reactive behavior. Viatra uses an internal domain-specific language for specifying transformations, i.e. an advanced API over Java and Xtend [38]. Viatra has proven to be an efficient execution platform for incremental transformations in [20, 24].

Example. A sample event-driven transformation rule (adapted from [20]) is illustrated in Fig. 3, which removes a stopped ApplicationInstance from the model if it is no longer allocated to a host instance. The execution of this rule is triggered by a disappearance of a match of its precondition pattern stoppedApplInstance. If the application instance is still stopped after the observed change, then we remove appInst from appType.

When executing the rule over the model of Fig. 2, the rule is triggered when the allocatedTo reference is removed between app3 and host2. Then the rule action removes app3 together with the incoming instances reference from app (illustrated by dotted lines in Fig. 2).

Fig. 3.
figure 3

A sample event-driven transformation rule

Full size image

4 Selected Recent Applications

The EMF-IncQuery and Viatra frameworks have actively been used in different research and industrial projects carried out by various researchers and practitioners. Below we provide a short overview of selected applications of these frameworks within our own projects.

  • A recent project aimed to define a model-driven approach and tool chain for the synthesis of complex, integrated Matlab Simulink models capable of simulating the software and hardware architecture of an airplane [14, 16].

  • As a bi-product of the project, the Massif (Matlab Simulink Integration Framework for Eclipse)Footnote 4 framework [16, 19] was developed, which provides a bidirectional bridge between Matlab Simulink models and their EMF model counterpart by calling the Matlab API.

  • Formal validation of domain-specific languages is carried out in [29] by using back-end logic solvers where derived features and well-formedness constraints are captured by queries.

  • Incremental queries and transformations provide foundations for incremental code generators [18] to avoid complete regeneration in case of small changes.

  • Incremental recomputation of graphical views of Sirius [17] can be also be driven by reactive transformations.

  • Live detection of human gestures and movements are carried out in [11] by using streaming transformations and complex event processing. Similar technology is used in ongoing work for runtime verification of cyber-physical systems and detecting critical situations in IoT applications [27].

In addition, EMF-IncQuery and/or Viatra is known to be integrated into popular open source modeling tools such as Papyrus UML [36], Capella [25], mbeddr [3], Sirius [37] or Artop [1].

5 Related Work

There are, of course, other open source technologies which support model queries or transformation used in Eclipse based tooling.

Query Technologies. EMF Model Query 2 [31] provides simple query primitives for selecting model elements that satisfy a set of conditions. The OCL development environment of the Eclipse OCL project [34] provides different ways to edit OCL constraints: an Xtext-based editor for file-based editing, an embedded editor inside Ecore model editors. The Epsilon Validation Language is dedicated to support the construction of validation rules within the Epsilon family [22], while the Acceleo Query Language (AQL) is heavily used within the Sirius project [37] to populate views from underlying models. However, relatively few academic approaches support incremental evaluation [10, 28].

Transformation Technologies. The development environment of EMF-based model transformation tools provide support for specifying, executing and evaluation of transformations including frameworks such as ATL [32], Henshin [9], QVTo [35] or eMoflon [2]. Many industrial applications rely on Xtend [38] as a code generation and transformation language based on Java. Epsilon [22] provides the Epsilon Transformation Language and the low-level Epsilon Object Language with an advanced execution platform. Recently introduced new features of ATL include target incremental computation [21] combined into the ReactiveATL transformation engine.

6 Conclusions

While a multitude of design are verification tools is used in model-driven systems engineering of critical systems, the complexity of those tools is frequently comparable to the system under design. Certification standards of critical systems necessitate to qualify those tools, i.e. to justify that the tools themselves do not introduce new errors to the design. The complexity of the tools makes tool qualification extremely costly, and provides a strong motivation for solid foundations of integrated tool features. The paper overviews two open source projects, EMF-IncQuery and Viatra to serve as a precise and efficient basis by incremental model queries and reactive transformations as illustrated on various industrial applications.

Our ongoing research and development aims to develop systematic approaches to the verification and validation of tool features and language specifications. This primarily includes the automated synthesis of a large, well-formed and diverse set of instance models to serve as test cases or scalability benchmarks. Furthermore, as distinction between design-time and run-time models are being more and more blurred [23] for smart cyber-physical systems, incremental query and transformation techniques will likely be used as part of the underlying middleware, which triggers further open challenges.