MoDeVVa’17 Model Driven Engineering, Verification and Validation Integrating Verification and Validation in MDE Ernesto Posse◦ , Daniel Ratiu+ , Gehan M. K. Selim• , Faiez Zalila? ◦ Zeligsoft, Canadaeposse@zeligsoft.com + Siemens, Germany daniel.ratiu@siemens.com • McMaster University, Canada selimg@mcmaster.ca ? Inria, France faiez.zalila@inria.fr Abstract—Models are purposeful abstractions of systems and ”Building Self-aware Systems for Continual Self-Testing and their environments. They can be used to understand, simulate, Development”. and validate complex systems at different abstraction levels. The call for papers of MoDeVVa’2017 attracted 9 submis- Thus, the use of models is of increasing importance for industrial applications. Model-Driven Engineering (MDE) is a development sions covering both MDE and V&V activities. These papers methodology that is based on models, metamodels, and model range on a wide spectrum covering fundamental contributions, transformations. The shift from code-centric software develop- applications and tool development and improvements. Each ment to model-centric software development in MDE opens up paper was reviewed by at least three reviewers and the promising opportunities for the verification and validation (V&V) program committee accepted 6 papers. We congratulate the of software. On the other hand, the growing complexity of models and model transformations requires efficient V&V techniques in authors of these 6 papers and thank all authors who submitted the context of MDE. articles to MoDeVVa’2017. The research papers presented at The workshop on Model Driven Engineering, Verification MoDeVVa’2017 covered research topics in the areas of: and Validation (MoDeVVa) offers a forum for researchers and • The integration of V&V approaches into MDE. practitioners who are working on V&V and MDE. The main • The definition of V&V approaches that rely on MDE. goals of the workshop are to identify, investigate, and discuss mutual impacts of MDE and V&V. • Modeling the rules for combining sub-models in order to For the 2017 edition of the MoDeVVa workshop, we put improve compositionality. an emphasis on combining heterogeneous (possibly incomplete) • Modeling conformance relations for checking the refine- V&V techniques of MDE artifacts, and using their combined ment of models. verification results to increase the confidence in the V&V pro- • Modeling transformations between models used for de- cess. We have compared the used techniques with respect to different criteria (e.g., time efficiency, memory usage, soundness, sign and models used for V&V. completeness, user-friendliness). • Incremental V&V (reuse as many V&V results as possi- Keywords: Model-Driven Engineering (MDE), models, meta- ble after a change in a model). models, model transformations, verification and validation • The application of the above topics to MDE itself (V&V (V&V). of meta-models, models and model transformations). • Continuous V&V of models. I. I NTRODUCTION • V&V of models and modeling tools (e.g. generators) for safety critical systems using models to increase practica- The fourteenth Workshop on Model Driven Engineering, bility of formal verification. Verification and Validation (MoDeVVa) co-located with the • Experience reports. twentieth International Conference on Model Driven Engineer- ing Languages and Systems (MODELS) was held in Austin, II. W ORKSHOP CONTENTS TX, USA, in September 2017. The objective of MoDeVVa The MoDeVVa’2017 featured two keynotes and six papers is to offer a forum for researchers and practitioners who are as briefly described in the following. working on verification and validation (V&V) and/or Model- Driven Engineering (MDE). A. Keynotes Each year, MoDeVVa invites outstanding researchers from a) Keynote 1: The first keynote of MoDeVVa’17, Build- both MDE and V&V to present their work. For MoD- ing Self-aware Systems for Continual Self-Testing and Devel- eVVa’2017 edition, two keynotes speakers were invited. Prof. opment, was given by Dr. Kristie Bellman. During the talk, Marc Pantel from the University of Toulouse, France, gave a Dr. Bellman presented the challenges to continual testing and talk entitled ”Property driven approaches to formal verification verification of self-aware systems. Dr. Bellman discussed the for domain specific modeling languages ”. Also Dr. Kirstie L. roles of models in such self-aware systems and how a self- Bellman, from Topcy House Consulting gave a talk entitled aware system can perform continual monitoring and testing of its models and other components. As an example, she The sixth paper is entitled ”Hierarchical Model Exploration described the CARS robotic cars testbed that was used to study for Exposing Off-Nominal Behaviors” [2]. It presents a the development of self-aware systems that can partly develop model-driven requirements analysis approach that reduces and correct their own models. state and rule explosion problems using a hierarchical b) Keynote 2: The second keynote of MoDeVVa’17, model exploration strategy, and its empirical results with the Property Driven Approaches to Formal Verification for Do- pacemaker requirements. main Specific Modeling Languages, was given by Prof. Marc Pantel from the University of Tolouse. During this keynote Prof. Pantel advocated the use of languages or tools dedicated R EFERENCES to specific kind of properties in order to translate automati- cally design models to verification models whose automated [1] K ANAV, S., AND A RAVANTINOS , V. Modular transformation from AF3 to nuxmv. In Proceedings of the 14th Workshop on Model-Driven verification scales better that the one of generic approaches. Engineering, Verification and Validation co-located with ACM/IEEE 20th International Conference on Model Driven Engineering Languages and B. Technical Papers Systems (MODELS 2017), Austin, Texas, USA, September, 2017. (2017). [2] K AUSHIK M ADALA , H. D., AND ACEITUNA , D. Hierarchical model The first paper, entitled ”Modular transformation from AF3 exploration for exposing off-nominal behaviors. In Proceedings of the to nuXmv” [1] presents an approach to modularize and reuse 14th Workshop on Model-Driven Engineering, Verification and Validation bi-directional model-to-model transformations between AF3 co-located with ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MODELS 2017), Austin, models and the input language of the nuXmv model checker. Texas, USA, September, 2017. (2017). Parts of the forward transformations are reused when the [3] O LIVEIRA , R., AND D INGEL , J. Supporting model refinement with counterexamples provided by nuXmv are lifted into AF3. equivalence checking in the context of model-driven engineering with UML-RT. In Proceedings of the 14th Workshop on Model-Driven Engineering, Verification and Validation co-located with ACM/IEEE 20th International Conference on Model Driven Engineering Languages and The second paper, entitled ”Supporting Model Refinement Systems (MODELS 2017), Austin, Texas, USA, September, 2017. (2017). [4] S TEFAN K LIKOVITS , J OACHIM D ENIL , A. M., AND S ALAY, R. Mod- with Equivalence Checking in the Context of Model-Driven eling frames. In Proceedings of the 14th Workshop on Model-Driven Engineering with UML-RT” [3] proposes a framework to Engineering, Verification and Validation co-located with ACM/IEEE 20th provide a formal approach to check the refinement relation International Conference on Model Driven Engineering Languages and Systems (MODELS 2017), Austin, Texas, USA, September, 2017. (2017). between two models expressed with UML-RT. The checking [5] VALLECILLO , A., AND G OGOLLA , M. Adding random operations to was performed via a translation of the UML-RT models into ocl. In Proceedings of the 14th Workshop on Model-Driven Engineering, the LNT formal language and then checking the equivalence Verification and Validation co-located with ACM/IEEE 20th International Conference on Model Driven Engineering Languages and Systems (MOD- by using the CADP formal verification tool. ELS 2017), Austin, Texas, USA, September, 2017. (2017). [6] Y URCHENKO , K., B EHR , M., K LARE , H., K RAMER , M., AND R EUSS - NER , R. Architecture-driven reduction of specification overhead for verifying confidentiality in component-based software systems. In Pro- The third paper, entitled ”Modeling Frames” [4] is focused ceedings of the 14th Workshop on Model-Driven Engineering, Verification on the contexts for modeling activities. Modeling frames and Validation co-located with ACM/IEEE 20th International Conference capture the implicit knowledge and assumptions made during on Model Driven Engineering Languages and Systems (MODELS 2017), Austin, Texas, USA, September, 2017. (2017). the modeling process, which help assessing the quality of the result of a modeling activity. It also provides information about the context in which a modeling artifact is valid and can be reused. The fourth paper is entitled ”Architecture-Driven Reduction of Specification Overhead for Verifying Confidentiality in Component-Based Software Systems” [6]. It presents a model- driven approach that facilitates the creation and maintenance of confidentiality specifications for the verification of component-based software. The fifth paper is entitled ”Adding Random Operations to OCL” [5]. This paper presents an extension of OCL to allow modellers to deal with random numbers and probability distributions in their OCL specifications. It shows its implementation in the tool USE and discuss some advantages of this new feature for the validation and verification of models.