From Biological Domain to Formal Methods: a model-driven approach

title:From Biological Domain to Formal Methods: a model-driven approach
company:
keywords:Model-Driven Software Engineering, Epsilon, Biological networks, Timed Automata
contact:dr. S. Schivo
to be started:any time

Internship in Formal Methods and Tools

Description

The study of biological networks is a very important task, as a better understanding of these biological processes would help researchers develop more effective medicines and cures for illnesses that today cannot be treated effectively. Apart from many types of cancer, some non-lethal illnesses such as diabetes or osteoarthritis have a big impact on the quality of life many people, yet no cure currently exists. Finding a non-invasive way to make life easier in these situations (or even completely cure the illnesses) requires a deep knowledge of how our cells work internally. As the processes deciding how a cell reacts to its environment are extremely complex, intuition alone cannot go very far: for this reason, biologists need a proper computational support.
ANIMO (Analysis of Networks with Interactive MOdeling) is a software tool developed to help researchers reason on complex biological networks. ANIMO models are built in a user-friendly interface implemented in Java, and made to be used directly by biologists. The user interface hides the formal model under the hood, allowing to access formal methods without the need to learn their inner workings. This is achieved through an automatic translation process of ANIMO models into Timed-Automata networks, which are then analyzed with the UPPAAL tool; the results of those analyses are then parsed and properly displayed to the users.
Currently, the translation from an ANIMO model into a Timed-Automata network is hard-coded in ANIMO's source code. This means that whenever a modification on an ANIMO model template is required, the programmer needs to directly change the code related to the translation. Such a process is highly error-prone, and requires a high degree of knowledge of both the ANIMO model and the UPPAAL model.
In order to deal with this problem, we propose to apply model-driven software engineering techniques. The modular implementation of the translation from ANIMO models to Timed-Automata networks via model transformations will avoid the burden of maintainance of hard-coded model translation. This will let us adapt ANIMO to different types of biological models much more easily than before, bringing code maintainability to high standards.
The project offers you the following opportunities:- work in an interdisciplinary academic setting,- experience a model-driven software engineering approach with most recent tools,- apply theoretical knowledge on a real practical case,- learn how to deal with domain-specific languages and models.

References

  1. ANIMO (Digital version available here)
  2. Epsilon (Digital version available here)
  3. UPPAAL (Digital version available here)