Model Transformations applied to Process Calculi

Djurre van der Wal, University of Twente

Domain Specific Languages (DSLs) are often used to model systems. While this facilitates work by domain experts, it also means that DSLs are not automatically supported by tools. To provide tool support for a DSL, one can either develop new tools from scratch, or link the DSL with an already available tool via a translation.

In this project we follow the latter approach; in particular, we look at a translation from AWN to mCRL2. AWN (Algebra for Wireless Networks) is a domain specific process algebra that has been particularly tailored to model routing and communication protocols in wireless mesh networks, but also finds application in other areas. mCRL2 is a model checking toolset that takes a process algebra by the same name as input. mCRL2 contains utilities for exploring, generating, manipulating, and visualizing state spaces, and can also be used to linearize, simulate, and optimize model specifications.

The project focuses on two goals: creating an automated translation from AWN to mCRL2 (which will provide the possibility to automatically verify AWN specifications with an existing model checking toolset) and formally proving the validity of this translation. The second goal also involves determining which conclusions can be safely drawn from feedback produced by mCRL2 by investigating which properties of a network specification (such as fairness) are preserved by the translation.

In the talk I will present our initial ideas for the translation, as well as our thoughts on which approach is most suitable for the implementation. One software methodology under consideration is Model Driven Engineering (MDE), a methodology that revolves around the design of models (in particular via a graphical tool or DSL) and defining transformations from model to model. Advantages of MDE include faster development, easier reuse of existing code, and fewer bugs