In this task the consortium will study the application of abstraction, compositionality and structure exploitation as key techniques in controlling and reducing the complexity involved in analysing real-time system models.

Abstraction and Composition are well established for model checking and theorem proving approaches to discrete state system verification. Abstraction -- either based on generic principles (like from timed to untimed systems, infinite data domains to finite one) or on case-specific user suggested simplifications -- serves to simplify the models by omitting aspects that are not relevant for analysis. Compositionality provides a divide and-conquer to manage complexity: properties of complicated systems are inferred from properties of components.

In particular the consortium will work on the following reduction strategy: consider a system consisting of many interacting timed automata such that the size of the global state- and clock-space is prohibitively large. One can take a sub-system consisting of a subset of the components and analyse it in isolation, treating the rest of the components as under-specified inputs. The set of behaviours exhibited by the reduced system, when projected on the variables that interact with the rest of the system, is an over-approximation of the actual behaviour, however is may have a much smaller model which can be plugged to the rest of the system and yield a tractable model. If the verification results hold for this smaller model then it hold for the real system. The consortium will develop techniques to perform automatic decomposition and approximation in this spirit.

For the verification of finite-state systems a number of techniques for exploiting the composite structure of the model exists. Partial order reduction and compositional backwards reachability are methods which help to reduce search spaces for loosely coupled concurrent components. Likewise, methods exploiting symmetries and hierarchical structure have shown to be very successful.

The consortium aims at developing similar structure exploiting techniques in the real time setting. The main difficulty is that the strong synchrony on time between the components of a real-time system is an obstacle in transferring directly the successful techniques from the finite-state setting. The consortium intends to identify practically useful restrictions of the timed automata formalism that will allow the development of similar structure exploiting techniques in the presence of real-time.

responsible partner: KUN