Formal Methods and Tools — a contribution to ICT research at the UT
Formal methods are mathematical techniques for the construction and analysis of software systems. Our central goal is to increase the reliability of the software that we rely on, as individuals and as society. We primarily target complex concurrent ICT systems, embedded in a technological context or in a distributed environment.
We address two important scientific challenges. The first challenge is how reliability of software systems can be justified. We study a wide suite of technologies to guarantee or demonstrate reliability, ranging from theorem proving, model checking, quantitative evaluation, to systematic testing, synthesis and optimization.
The second challenge is to handle the ever-increasing complexity of software systems. To this end we develop new theory on concurrency, automata, graphs, logic, languages, and algorithms to scale automated analysis and synthesis methods.
We distinguish two focus areas:
- Verification of concurrent software. Here the goal is to automatically establish the correctness of software with respect to its specification. An important activity is to generate and discharge verification conditions for concurrent programs automatically. Other techniques, like high-performance model checking and systematic testing, apply to finite models of software systems.
Together, these activities contribute to the certification of safety critical applications, for instance in automated driving and healthcare, and to the increased security of critical infrastructure and the Internet of Things.
- Quantitative evaluation of ICT systems. Many reliability criteria have a quantitative nature, for instance performance, availability, resource consumption, risks and costs. A strength of our group is to translate domain specific models to mathematical models that address these metrics. A modular, compositional approach handles complexity. We synthesize optimal solutions that combine and trade-off various quantitative aspects, based on our expertise in probabilistic and timed automata. Together, these activities contribute to optimizing energy consumption, computing residual safety and security risks, and developing smart maintenance strategies.
A common approach in software technology, connecting many of our research projects, is the use of domain specific models and model transformation. It links models for various system aspects at several abstraction levels. Another unifying aspect is formed by the software tools that we construct, to benchmark our algorithms in competitions and challenges, and to validate new methods on realistic case studies.
Besides verification and optimization of the reliability of critical applications of ICT in health, robotics, infrastructure and the Internet of Things, we are open to new and emerging applications of our technology, for instance in systems biology, health management, and nano-programmable systems.
Our results are disseminated via publications in journals and peer-reviewed conferences.