Real-time systems are systems that interact with their environment in such a way that for certain inputs the corresponding outputs have to occur within given time bounds. Many embedded systems, in particular those in safety critical applications, are of this type. The practical importance of this class of systems has led to a large body of research on the specification, verification and analysis of real-time systems.

Analysis and verification of real-time systems is based on computational models of such systems. Models with continuous time are close to the physical world and are well suited for dealing with the requirement and specification level; their automatic verification is performed using tools based on timed automata with real-valued clocks. To gain in efficiency also models with discrete time are considered; their automatic verification is performed using classical approaches
to temporal logic model checking. At the level of machine real-time systems are modeled as set of tasks that need to be scheduled to meet the required deadlines. While these real-time models have led to powerful analysis and verifications techniques, they turn out to be too idealistic or too simplistic to deal with the challenges of high-level specification languages, highly concurrent systems, and the intricacies of distributed computer architectures.

The AVACS projects R1--3 strive to overcome these restrictions by exploiting the structure of the real-time systems at all levels of abstraction ranging from specification level down to implementation level:

• project R1 will develop verification techniques for real-time requirements of high-level specifications based on constraint manipulation, predicate abstraction, and decision procedures for high-level data types;
• project R2 will develop task distribution and scheduling techniques taking the constraints of distributed computer architectures into account, in particular the combination of caches and pipelines;
• project R3 considers highly concurrent real-time systems and develops model checking techniques that combine heuristic search with abstraction.