Formal methods in real-time systems

The design of intricate real-time systems typically involves several notations that describe the system at different levels of abstraction. Graphical notations inspired by timing diagrams are helpful at the requirements' level, structured automata are common at the design level and dedicated languages are used at the programming level. The question arises how these different notations are linked together in a semantically meaningful way. We argue that a logic-based approach is making a real contribution here.