This is the official homepage of the MTA-BME Lendület Cyber-Physical Systems Research Group. The group was founded by Prof. Dániel Varró in 2015.

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 2^nd 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 2^nd 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

International Journal

• Szárnyas, G., Izsó, B., Ráth, I., and Varró, D., “The Train Benchmark: Cross-Technology Performance Evaluation of Continuous Model Validation”, Software and Systems Modeling, 2017.
• Szárnyas, G., Maginecz, J., and Varró, D., “Evaluation of Optimization Strategies for Incremental Graph Queries”, Periodica Polytechnica, Electrical Engineering and Computer Science, 2017.
• Semeráth, O., and Varró, D., “Evaluating Well-Formedness Constraints on Incomplete Models”, Acta Cybernetica Szeged, 2017. CSCS 2016 special issue
• Molnár V., Majzik I., “Model Checking-based Software-FMEA: Assessment of Fault Tolerance and Error Detection Mechanisms”, Periodica Polytechnica, Electrical Engineering and Computer Science, 2017.
• Varró D; Bergmann G; Horváth Á; Ráth I; Ujhelyi Z: Road to a reactive and incremental model transformation platform: three generations of the VIATRA framework, SOFTWARE AND SYSTEMS MODELING 15: (3) pp. 609-629. (2016). IF: 0.990
• Dávid, I., Ráth, I. & Varró, D. Foundations for Streaming Model Transformations by Complex Event Processing. SOFTWARE AND SYSTEMS MODELING (2016). doi:10.1007/s10270-016-0533-1. Appeared online, Expected IF: 0.990.

International Conference Proceedings

• Marussy, K., Molnár, V., Vörös, A., and Majzik, I., ” Getting the Priorities Right: Saturation for Prioritised Petri Nets”, Application and Theory of Petri Nets and Concurrency, vol. 10258: Springer, pp. 223-242, 2017. Acceptance rate: 48%, CORE Rank B.
• Czipó, B., Hajdu, Á., Tóth, T., and Majzik, I., “Exploiting Hierarchy in the Abstraction-Based Verification of Statecharts Using SMT Solvers”, Proceedings of the 14th International Workshop on Formal Engineering Approaches to Software Components and Architectures, vol. 245: Open Publishing Association, pp. 31–45, 2017.
• Sallai, Gy.; Hajdu, Á.; Tóth, T.; and Micskei, Z., “Towards Evaluating Size Reduction Techniques for Software Model Checking”, Proceedings of the Fifth International Workshop on Verification and Program Transformation, of Electronic Proceedings in Theoretical Computer Science: Open Publishing Association, 2017. (Accepted, in press)
• Semeráth, O., Debreceni, C., Horváth, Á., and Varró, D. “Incremental backward change propagation of view models by logic solvers.” In Proceedings of the ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems (pp. 306-316). ACM.
• Debreceni, C., Bergmann, G., Ráth, I., and Varró, D. “Deriving effective permissions for modeling artifacts from fine-grained access control rules”, Proceedings of the 1st International Workshop on Collaborative Modelling in MDE (COMMitMDE 2016) pp. 17-26, 2016. CEUR-WS
• Bergmann, G., Debreceni, C., Ráth, I. and Varró, D. Query-based access control for secure collaborative modeling using bidirectional transformations. In Proceedings of the ACM/IEEE 19th International Conference on Model Driven Engineering Languages and Systems (pp. 351-361). 2016. ACM.
• Semeráth, O., and Varró, D., “Graph Constraint Evaluation over Partial Models by Constraint Rewriting”, Proceedings of the 10th International Conference on Model Transformation, Marburg, Germany, Springer, 2017.
• Hajdu, Á., Tóth, T., Vörös, A., and Majzik, I., “A Configurable CEGAR Framework with Interpolation-Based Refinements”, Formal Techniques for Distributed Objects, Components, and Systems (FORTE 2016), vol. 9688: Springer, pp. 158-174, 2016. Acceptance rate: 40%, CORE Rank A.
• Debreceni, C., Ráth, I., Varró, D., Carlos, X D., Mendialdua, X., and Trujillo, S., “Automated Model Merge by Design Space Exploration”, 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016), Eindhoven, The Netherlands, 04/2016., Springer-Verlag, LNCS 9633, Acceptance rate: 30%, CORE Rank B.
• Semeráth, O., Vörös, A., and Varró, D., “Iterative and incremental model generation by logic solvers”, 19th International Conference on Fundamental Approaches to Software Engineering (FASE 2016), Eindhoven, The Netherlands, 04/2016. Springer-Verlag, LNCS 9633, Acceptance rate: 30%, CORE Rank B
• Marussy, K., Klenik, A., Molnár, V., Vörös, A., Majzik, I., and Telek, M., “Efficient decomposition algorithm for stationary analysis of complex stochastic Petri net models”, Application and Theory of Petri Nets and Concurrency, vol. 9698: Springer, pp. 281-300, 2016. Acceptance rate: 38%, CORE Rank B.
• Vörös, A., Darvas, D., Molnár, V., Klenik, A., Hajdu, Á., Jámbor, A., Bartha, T., and Majzik, I., “PetriDotNet 1.5: Extensible Petri Net Editor and Analyser for Education and Research”, Application and Theory of Petri Nets and Concurrency, vol. 9698: Springer, pp. 123-132, 2016. Acceptance rate: 38%, CORE Rank B.
• Varró D., Incremental Queries and Transformations: From Concepts to Industrial Applications In: SOFSEM 2016: z2nd International Conference on Current Trends in Theory and Practice of Computer Science, Harrachov, Czech Republic, January 23-28, 2016, Proceedings. Springer Verlag, 2016. pp. 51-59. (LNCS; 9587.) – Invited paper. CORE Rank B.
• Marussy, K., Klenik, A., Molnár, V., Vörös, A., Telek, M., and Majzik, I., “Configurable Numerical Analysis for Stochastic Systems”, Proceedings of the 2016 Workshop on Symbolic and Numerical Methods for Reachability Analysis (SNR): IEEE, 2016.
• Semeráth, O., Debreceni, C., Horváth, Á., and Varró, D., “Change Propagation of View Models by Logic Synthesis Using SAT Solvers”, Fifth International Workshop on Bidirectional Transformations (Bx 2016) @ETAPS2016, Eindhoven, The Netherlands, 04/2016.
• Makai, J., Szárnyas, G., Horváth, Á., Ráth, I., and Varró, D., “Optimization of Incremental Queries in the Cloud”, CloudMDE 2015: Model-Driven Engineering on and for the Cloud: Proceedings of the 3rd International Workshop on Model-Driven Engineering on and for the Cloud (at IEEE/ACM MoDELS 2015)2015.
• Chechik, M., Dalpiaz, F., Debreceni, C., Horkoff, J., Ráth, I., Salay, R., and Varró, D., “Property-Based Methods for Collaborative Model Development”, 3rd International Workshop on the Globalization Of Modeling Languages and the 9th International Workshop on Multi-Paradigm Modeling (at IEEE/ACM MoDELS 2015), Ottawa, Canada, 2015/09.

 

National Conference

• Sólyom, A A., and Nagy, A S., “Swarm Intelligence Meets Rule-Based Design Space Exploration”, Proceedings of the 23rd PhD Mini-Symposium, Budapest University of Technology and Economics, Department of Measurement and Information Systems, 02/2016.
• Maginecz, J., and Szárnyas, G., “Sharded Joins for Scalable Incremental Graph Queries”, Proceedings of the 23rd PhD Mini-Symposium, Budapest University of Technology and Economics, Department of Measurement and Information Systems, 02/2016.
• Búr, M., Vörös, A., Bergmann, G., and Varró, D., “Towards Modeling Cyber-Physical Systems From Multiple Approaches”, Proceedings of the 24th PhD Mini-Symposium, Budapest University of Technology and Economics, Department of Measurement and Information Systems, 02/2017.
• Szilágyi G., and Vörös, A., ” Distributed Runtime Verification of Cyber-Physical Systems Based on Graph Pattern Matching”, Proceedings of the 24th PhD Mini-Symposium, Budapest University of Technology and Economics, Department of Measurement and Information Systems, 02/2017.
• Gujgiczer, A., Elekes, M., Semeráth, O., Vörös, A., ” Towards Model-Based Support for Regression Testing”, Proceedings of the 24th PhD Mini-Symposium, Budapest University of Technology and Economics, Department of Measurement and Information Systems, 02/2017.
• Farkas, R., and Hajdu, Á., “Activity-Based Abstraction Refinement for Timed Systems”, Proceedings of the 24th PhD Mini-Symposium: Budapest University of Technology and Economics, Department of Measurement and Information Systems, pp. 18–21, 2017.
• Hajdu, Á., and Micskei, Z., “Exploratory Analysis of the Performance of a Configurable CEGAR Framework”, Proceedings of the 24th PhD Mini-Symposium: Budapest University of Technology and Economics, Department of Measurement and Information Systems, pp. 34–37, 2017.
• Debreceni, Cs., and Varró, D., “Approaches to Identify Object Correspondences Between Source Models and Their View Models”, Proceedings of the 24th PhD Mini-Symposium: Budapest University of Technology and Economics, Department of Measurement and Information Systems, pp. 14–17, 2017.
• Bence G., Molnár V., “Formal Compositional Semantics for Yakindu Statecharts”, Proceedings of the 24th PhD Mini-Symposium, Budapest University of Technology and Economics, Department of Measurement and Information Systems, 02/2017.

Sebastian Herzig  from Nasa JPL and Georgia Tech gave a talk at BME.

The title of the talk: Model-based Systems Engineering at the Jet Propulsion Laboratory: Past, Present, and Future

Abstract: JPL has a long history of robotic space exploration missions. From Explorer 1 orbiting the Earth, to the Voyager missions leaving the solar system and the Mars Science Laboratory rover landing on Mars under rocket power, JPL’s missions are well-known across the globe and an inspiration for many young engineers. The success of these missions is often attributed to effective and rigorous systems engineering practice. With future missions expected to become increasingly more complex, a need arose for evolving existing systems engineering practices to enable better information management, incorporate automation and actively support reuse. In this talk, JPL’s transition to Model-based Systems Engineering as well as current applications to space missions, and future directions, are described. The talk will also detail a current research and technology development effort led by the presenter, the aim of which are the introduction of design automation principles through application of model-driven engineering practice and artificial intelligence.

The talk is available: Herzig_BUTE_2017-06-29-003

We are glad to announce that the paper co-authored by G. Varró, A. Schürr and D. Varró on Benchmarking for graph transformation published at VL/HCC 2005 received a Most Influential Paper Award at the IEEE Symposium on Visual Languages and Human-Centric Computing (VL/HCC 2016).

Szárnyas, G., “Scalable Graph Query Evaluation and Benchmarking with Realistic Models”, ACM/IEEE MODELS conference, ACM Student Research Competition (SRC), co-located with the 19th International Conference on Model Driven Engineering Languages and Systems (MODELS 2016)

Semeráth, O., “Formal Validation and Model Synthesis for Domain-specific Languages by Logic Solvers”, ACM/IEEE MODELS conference, ACM Student Research Competition (SRC), co-located with the 19th International Conference on Model Driven Engineering Languages and Systems (MODELS 2016)

Nagy, A S., and Szárnyas, G., “Class Responsibility Assignment Case: a VIATRA-DSE Solution”, 9th Transformation Tool Contest, Vienna, Austria, 2016. – 1. place, http://www.transformation-tool-contest.eu/2016/solutions_cra.html

Eclipse IoT challenge 2016 – Third place

Csaba Debreceni: Advanced Techniques and Tools in Secure Collaborative Modeling, ACM Student Research Competition@MoDELS’17, Austin TX, USA, 2017 (supervisor: Dániel Varró, co-supervisors: Gábor Bergmann, István Ráth)