From toasters to space-stations, computerized technology is pervasive in modern technology and society, therefore the need for truly correct, safe and optimal control algorithms is higher than ever. Techniques like model checking and synthesis have long promised, and to some extend delivered, correctness and optimality guarantees in limited and highly critical application areas like software for satellites, medical devices or powerplants. Common for many of the application areas is the criticality of timing; airbags, pacemakers and traffic-lights have timing constraints that should never be violated.
In this thesis, we attempt to improve the applicability of model checking and synthesis methods for timed systems by attacking three different inhibiting factors to their applicability; 1) speed of computation, 2) what can be synthesized and 3) tool integration and interaction.
All interested parties are welcome. After the defense the department will be hosting a small reception in cluster 1.