Ensuring the correctness of model transformations via static and dynamic analysis (EPSRC DTA)

Safety-critical systems are software-intensive systems, whose failure could give rise to, or contribute to, a fatal accident or environmental damage. Such systems can be found in many domains such as railway, healthcare and medicine, robotics, aerospace, or automotive. To build confidence in the proper functioning of these systems, engineers have to use rigorous and well-defined development processes.

Model-Driven Engineering (MDE) is a popular approach to the development of safety-critical systems. In MDE, engineers model different aspects of a system (e.g. structural, behavioural, timing) and then they use dedicated analysis and transformation languages to derive other models or code. One limitation of this approach though is that faulty model and code transformations can introduce system errors, that are not present in the initial models. Existing research has focused mainly on defining model manipulation and transformation languages, as well as accompanying tools such as editors and debuggers. However, substantially less work exists on ensuring that model transformations and code generators are actually correct.

The aim of this PhD project is to devise and develop techniques and tools that combine static and dynamic analysis for gaining confidence on the correctness of model transformations and code generators.

The proposed research lies at the intersection of software engineering and programming languages, and it will make contributions to both of these areas.

Research supervision
If successful, you will conduct your research under the supervision of Dr Nicholas Matragkas, Lecturer in Software Engineering.

Interested applicants are encouraged to contact the project supervisor Dr Matragkas at [Email Address Removed] for further information.