From PUMA Graduiertenkolleg
The goal off this topic is to develop novel tool-based abstraction and analysis methods for parametric systems, in particular, of distributed real-time protocols. The methods should be as automatic as possible.
For that, the PhD project should identify logical/model-theoretic criteria which allow to represent a sufficiently homogeneous real-time system by systems of finite size or a suitable infinite model with "nice" algorithmic properties. The correctness of these representations should be proven by means of the theorem prover Isabelle.
In order to guarantee the practical relevance, the resulting methods and tools should be evaluated on industrial real-time protocols from the area of automotie or avionics.