Formal Methods and Software Engineering

Introduction and scope

How to design systems that work reliably? In the track Formal methods and Software Engineering we will address techniques, tools, and domain-specific languages that help developers making high-quality software and software designs. The goal is in particular to construct software systems that are correct, robust, well-structured, and easy to evolve. Automated design and verification tools play an important role.

If you liked one of the following teaching modules of the University of Twente, you will probably like this research track as well:

  • Software Systems (software specification, software design patterns);

  • Discrete Structures and Efficient Algorithms (algorithms, languages & machines);

  • Programming Paradigms (compiler construction, concurrency);

  • Cyper-Physical Systems (timed automata, Markov chains).

Suggested topics

In this track research topics in the following categories are accepted:

  • Model-driven engineering (MDE) focuses on creating and exploiting domain models (abstract representations for a particular application domain). Often these models are represented in domain-specific languages, which need to be engineered properly. Using graph transformation, such models are used to (automatically) create implementations. An important issue is the traceability of requirements throughout design and implementation.

  • Program Verification: Can we use and improve automated reasoning techniques to really prove that a program meets its intended behaviour? And how can we specify our intents? Model checking checks automatically if a program model contains errors. Model checking algorithms are based on smart graph-search. Another flavour is Model-based Testing, which investigates techniques for automatic test generation, execution and evaluation. Some projects study quantitative methods, for instance to predict time and probability (risk).

  • Software composition relates to support in methods, notations and languages for composing large systems from smaller parts. Advanced examples include aspect-orientation, composition filters, 'free composition', and service-oriented architectures.

Further reading

A list of example project descriptions for this track, including links for further reading material, can be found at http://fmt.cs.utwente.nl/education/bachelor/

Information

For further information on the content of this track, you may contact the track chair Stefano Schivo.