The formal methods theme investigates the use of formal models and associated technologies for verification and validation to analyse critical properties of software and systems. Such properties may refer to potential safety issues that might occur if a system enters a hazardous state, or to security issues where confidential data is compromised. The methods and tools applied have a wide range including model checking, proof or simulation.

Often practical problems usually do not fit into the narrow margins set by single forms of formal analysis like model checking, proof or simulation.

Typically, formal modelling notations, tools and methods permit specific kinds of analysis but not a mix that is driven by the practical problems encountered. Often, the same problems are modelled in various modelling notations and analysed in various tools. For use outside academia, this appears impractical as the necessary skill sets are difficult to attain.

We seek tighter integration while not imposing a core set of analyses.

This will make the developed approaches easier to adopt as users can buy in required analyses remaining as lightweight in their application as possible.

One problem of formal verification is that verification results often do not come with comprehensible explanations. A formal proof generated by an automatic theorem prover is often impossible to follow for non-trivial statements. This means the proof does not yield an explanation for the truth of the statement that could be scrutinised by an engineer with reasonable effort. Model-checking suffers from a similar problem.

Now, if a statement has been verified, we should be able to validate why that statement is true. If a statement is false, then the source of the problem should be pinpointed as close as possible and incremental improvements supported. The generation of such explanations and incremental support to explore solutions are of high interest for the widespread use of formal verification in engineering.

To master complex systems it is often advantageous to consider smaller components of a system first and then draw conclusions on the complex system composed of those components. In practice, this is a difficult problem. Usually, abstractions of components not considered are needed.

These need to reduce overall complexity while preserving enough detail so that suitable properties can be verified. We are particularly interested in incremental approaches that permit us to sketch out abstractions gradually to make finding suitable abstractions easier.

With particular attention to security and safety criticality, verification and validation of software and system properties make use of formal models for their capture and analysis. Currently, the focus is placed on modelling of cyber security standards, automated compliance analysis against cyber security standards, property definition for cyber attacks and model guided secure architecture implementation.

Where possible the investigated problems and areas are backed up by tool developments when suitable tools are not available.