Modelling techniques for CPS
Cross-technology benchmark for query technologies for evolving graphs
In model-driven development of critical cyber-physical systems, early validation of the system under design is an important challenge to highlight design flaws early and provide feedback to systems engineers. Validation rules are frequently captured concisely as queries over graph models, which are rapidly increasing in size and complexity. Therefore, efficient query execution, especially, over evolving models is a challenging task for modeling and simulation tools.
Contributions. We introduced a cross-technology benchmark framework to systematically assess the scalability of validating and revalidating well-formedness constraints over large graph models. The benchmark case defines a typical well-formedness validation scenario in the railway domain including the metamodel, an instance model generator, and a set of well-formedness constraints captured by queries and repair operations (imitating the work of systems engineers by model transformations). The benchmark case focuses on the execution time of the query evaluations with a special emphasis on reevaluations, as well as simple repair transformations. More than 10 different technologies have been compared so far with fundamentally different knowledge representation (EMF, RDF, property graphs, relational databases). We continuously maintain a web page for the benchmark results: https://github.com/FTSRG/trainbenchmark. A journal paper has been submitted to Software and Systems Modeling (Springer), which is currently under review.
Query evaluation for runtime models over heterogeneous smart platforms
The runtime assurance of smart and trusted CPS is important during the operation as errors in such systems can lead to serious financial loss or damage in human life. These systems typically have complex autonomous behavior which makes design time verification infeasible. In addition, complex interactions with their environment makes the analysis even more difficult especially when the environment is not completely known in advance. To ensure the safe operation of CPS, one can rely on run-time monitoring of both high-level safety properties and assumptions on the context since hazardous cases may emerge during interactions with the environment.
Contributions: As ongoing research, we aim to derive monitors from high-level query specifications capturing hazardous interactions, and allocate them to the various platform components. We will investigate how query languages can be extended to specify allocations of certain subqueries to dedicated nodes over a heterogeneous IoT/ CPS execution platform. Initial results will be reported during the 2nd year of the project.
Bidirectional viewpoint synchronization by logic solvers
Domain-specific modeling languages are frequently used means to capture CPS from different viewpoints. View models are key concepts of domain-specific modeling to provide task-specific focus to the designers by highlighting only the relevant aspects of the system. View models can be specified by unidirectional forward transformations which are incrementally executed upon changes of the source model to automatically maintain the view models.
Contribution. For backward change propagation, we developed a novel state based backward transformation technique using SAT solvers to synthetize valid and consistent change candidates in the source model, where only forward transformation rules are specified for the view models. Initial results were reported at the BX’15 workshop at ETAPS 2015 and will be presented in the IEEE/ACM MODELS’16 conference (during the 2nd year of the project). Conflicting view model changes can be merged by an automated technique driven by design space exploration reported in.
Bidirectional synchronization between secure views
Large-scale system development efforts require the collaboration of multiple engineers, possibly from multiple organizations. For traditional, source code-based software engineering, there already are several off-the-shelf collaborative software development tools capable of supporting multiple engineers in collaborating on the same piece of software, while obeying access control policies that determine who can read or modify the various pieces of source code. Essentially, each user accesses a secure view of the engineering repository that contains a filtered and/or obfuscated set of artifacts; some of which may be modifiable, in which case the changes are bidirectionally propagated to the views of other collaborators. There are, however, challenges in extending these workflows from traditional development processes to model-driven or CPS design tasks.
Contribution. As a follow up of research started in the MONDO EU FP7 research project, we developed a collaborative modeling framework with the distinguishing features of fine-grained, rule-based model-level access control. The synchronization between secure views is achieved by incremental and bidirectional model transformations. A peer-reviewed conference paper is accepted and will be presented at the IEEE/ACM MODELS’16 conference in Year 2.
Formal analysis of dynamic and adaptable CPS
Synthesis of instance models by logic solvers
The generation of sample instance models of Domain-Specific Language (DSL) specifications has become an active research line due to its increasing industrial relevance for synthesizing prototypical contexts for testing autonomous CPS or for validating complex CPS modeling tools with large metamodels and complex well-formedness constraints. However, the synthesis of scalable, consistent, diverse and realistic models is a major foundational research challenge.
Contributions. We developed an iterative process for generating consistent instance models by calling existing logic solvers as black-box components using various approximations of metamodels and constraints to improve overall scalability. (1) First, we apply enhanced metamodel pruning and partial instance models to reduce the complexity of model generation subtasks and the retrieved partial solutions initiated in each step. (2) Then we propose an (over-)approximation technique for well-formedness constraints in order to interpret and evaluate them on partial (pruned) metamodels. (3) Finally, we defined a workflow that incrementally generates a sequence of instance models by refining and extending partial models in multiple steps, where each step is an independent call to the underlying solver. Our results were published and presented at the FASE 2016 conference.
Complex event processing techniques over evolving models
Many distributed systems in smart cyber-physical systems implement the control logic over a stream of events which may offer extreme scalability in a distributed environment with a massive number of nodes. Complex event processing (CEP) offers well-founded techniques to capture critical event sequences observed on the event streams within a given time window which require immediate reaction. As a smart CPS also needs to autonomously perceive its operational context and adapt to changes in an open, heterogeneous and distributed environment, the current snapshot of the system and its operational context can be formally captured as a live model (or runtime model), which continuously gets updated to reflect relevant changes in the underlying real system.
Contributions. To handle a novel class of streaming transformations for live models where models evolve at a very fast rate, we innovatively combine complex event processing techniques with live model queries and transformations. We developed (1) a high-level integrated domain-specific language for capturing complex event sequences over model changes defined by queries and specifying reactions as streaming transformations; (2) precise foundations of this event processing DSL including syntax and semantics; (3) a complex event processing engine tightly integrated into the open source VIATRA reactive and incremental transformation framework, and (4) a case study with initial scalability assessment of the performance of the framework for live gesture recognition. Our results have been published as open access in Software and Systems Modeling (SoSyM) peer reviewed international journal.
Characterization of realistic models
Graph-based models are used in design-time CPS modeling tools for many purposes such as functional testing and performance benchmarking of modeling environments to ensure the correctness and scalability of tools. However, while existing graph-based model generators may generate large models in increasing size, these models are claimed to be simple and synthetic, which hinders their credibility for industrial and research benchmarking purposes. But how to characterize a realistic model used in the engineering of CPS?
Contributions. In our ongoing research, we examined the key factors of generating realistic models of software and systems engineering. During the investigation, we collected 17 different graph metrics from other disciplines (e.g. network theory) and evaluated them on 75 instance models originating from six modeling domains. Our preliminary results show that certain metrics are similar within a domain, but differ greatly between domains, which makes them suitable input for future instance model generators to derive more realistic models. These results will be reported in Year 2.
Incremental verification techniques
Traditional verification tools are tailored to the safety-critical domain, however, recent CPSs yield new challenges as they commonly have dynamic structure and autonomous behavior. In addition, they have to react to the environment, where the behavior of the environment is not known in advance, only some assumptions are available. The dynamic changes of the structure of such autonomous reconfigurable systems and their adaptation to their environment yields a huge set of potential behavior, which is a major challenge.
Contributions. We propose incremental verification that might provide an efficient solution to the analysis of dynamic CPS. The first step we did in the first year was to develop a prototype framework providing various symbolic verification algorithms. The framework also supports the development of the models. In the next year, we plan to extend the algorithm library to be able to efficiently process the changes of the model and to decrease the time to do the revalidation/verification of the systems during runtime. Our results have been published at the “37th International Conference on Applications and Theory of Petri Nets and Concurrency” in a peer reviewed international conference paper .
Configurable Abstractions for verification and validation
Context. In the past decades, various efficient formal analysis techniques were developed for various domains, including software and hardware verification. However, due to the heterogeneity of cyber-physical systems, there is no single technique that can analyze and verify all of their aspects (e.g., hardware, software, communication) in a combined way.
Contributions. Our research aims to integrate different, abstraction-based techniques into a common, configurable framework, enabling to select the most appropriate analysis method for each aspect. We also experimented with possible analysis techniques and developed the foundations of the framework. We presented our preliminary results in a peer reviewed international conference paper at the 36th IFIP International Conference on Formal Techniques for Distributed Objects, Components and Systems.
Stochastic analysis of extra-functional CPS properties
Extra-functional properties of dynamic CPS systems impose new challenges on the traditional stochastic algorithms. Stochastic aspects of complex CPS-s require more and more involved analysis approaches. Answering reliability, performability and related analysis questions can often be reduced to steady state, transient, reward or sensitivity value analysis of stochastic models.
Contributions. Our goal is to design a configurable stochastic analysis framework which supports the user to combine explicit, symbolic and numerical algorithms to efficiently compute the measures of stochastic CPS models. Beyond the well-known algorithms from the field, we also developed an experimental version of an Induced Dimensionality Reduction Stabilized numerical solver to compute steady-state probabilities of Markovian models. As far as we know, this is the first attempt to exploit this algorithm in stochastic analysis. We have conducted experiments on different combinations of the algorithms on various models to assess their advantages and disadvantages in the analysis. This information can be used by the user to choose the combination of algorithms being efficient solving the analysis problem.
We designed a framework supporting and combining different symbolic and numerical algorithms to compute reward and engineering measures of stochastic CPSs. Our results have been published at the “37th International Conference on Applications and Theory of Petri Nets and Concurrency” in a peer reviewed international conference paper and in a peer-reviewed workshop paper.
Design space exploration for dynamic and adaptable CPS
Multi-objective optimization for DSE
An important aspect of CPSs is to find an optimal configuration either at design time or at runtime that can drive decisions on implementing self-* behavior. However, in case of CPSs, optimality can include multiple objectives such as performance, maintenance cost, etc. The main goal of this year was to continue the initial results we achieved in multi-objective rule-based design space exploration and to develop a prototype of the approach.
Contribution: We extended our framework with genericity to genetic algorithms (also adding a new algorithm PESA besides NSGA-II) and experimented with additional enhancements on selecting the initial set of solutions and adaptiveness to the mutation rate. Furthermore, we investigated the application of swarm intelligence based algorithms. We have published the results in an peer-reviewed workshop paper, furthermore, we have submitted a journal paper. We also participated at the Transformation Tool Contest (TTC 2016), which is an international event in Year 2.
Case studies and demonstrators for CPS
Initial version of demonstrator
Our goal is to develop a CPS demonstrator systems which can 1) show the challenges in designing and verifying CPS 2) demonstrate best practices for the development and 3) it can serve as a benchmark application for CPS related techniques. In the first year, we started to build a Model-based Demonstrator for Smart and Safe Systems (MoDeS3 for short) to simultaneously demonstrate the specificities of traditional safety-critical systems and smart and dynamic CPS. The first prototype was introduced at the Open IoT Developer Challenge which is an annual challenge organized by the Eclipse IoT Working Group of EclipseCon North America. From the 89 participating teams, the MoDeS3 team won the third price. In addition, the solution was also presented at the Ericsson University Day