In cooperation with Oxford we plan to develop a system specification notation and calculus for real-time systems based on the Duration Calculus [35]. Its relationship to models and notations for dynamic systems and control systems will also be investigated [15] [34] [43], as well as its relation to program specifications as investigated in Oldenburg [10].
This line of work will also investigate design paradigms for real-time systems, and especially study the links to control theory. We also hope to find verification techniques that can utilise mechanised proof support or model checking along the lines of the timed automatons of Dill and Alur or timed transition systems of Sifakis [41].