Verifying Model Transformations for Real
Levi Lucio - Research Associate with the Modelling, Simulation and Design Laboratory at McGill University
July 31, 2015, 2 p.m. - July 31, 2015, 4 p.m.
MC 103
Model transformations are computations performed on models. They are increasingly used by software engineers, in particular within teams that make use of use model-driven development. In this talk I will highlight the challenges posed when attempting to verify real-world model transformations, based on our 5-year experience when developing the SyVOLT model transformation contract prover.
I will start by providing an overview of our verification technique from a theoretical and and implementation point of view. I will present some of the challenges encountered during the development period and discuss how iterations between theory and practice have allowed us to advance while reinforcing both. In particular, the architecture of SyVOLT will be laid out and discussed and I will point out the encountered limitations and benefits of having used model-driven development techniques when building the tool’s codebase.
Among other examples, I will describe a large industrial model transformation we are currently verifying, part of the mbeddr tool (http://mbeddr.com), that is developed by German companies Itemis and fortiss. Advantages and limitations of the contract language we currently use will be highlighted. Also, I will describe some of the strategies we have employed to allow SyVOLT to scale to real-life sized problems.
I will conclude by presenting our tool’s performance when verifying the model transformations described during the talk, identifying SyVOLT’s current limitations, and describing current or future work on improving the tool in terms of scalability, performance and features.
Levi Lúcio is currently a Research Associate with the Modelling, Simulation and Design Laboratory at McGill University. He was awarded a PhD from the University of Geneva in Switzerland in 2008 for his work on model-based testing. His research today is about bridging software engineering and formal modelling techniques. Levi believes that the future of Software Engineering will include more and more tools that will make available to developers abstractions of data and computations that will be domain-specific, simple and intuitive to use, less error prone, easier to verify, and will make software development more efficient and cost-effective.
