Modelling and Verification of Real-Time Systems Using Timed Automata : Theory and Practice

Sammanfattning: During the last decade, model-checking techniques for the verification of timed system have been developed baaed on the theory of timed automata. The practical limitation in applying these techniques to industrial-size systems is the huge amount of time and memory needed to explore and store the state-space of the system model.In this thesis, we improve the current status of model-checking techniques for timed systems by developing symbolic, on-the-fly and compositional verification techniques for timed automata. A common characteristics of the model-checking techniques presented is that they use efficient constraint-solving techniques to symbolically represent and manipulate the state-space. To avoid construction of the full state-space of the system model two techniques are used: on-the-fly generation of the state-space and a compositional model-checking technique. The memory-usage is further reduced by developing a minimal and canonical data structure for the class of constraints used in the model-checking algorithm, which reduces the size of each individual state. Two other techniques to reduce the total number of states explored and stored during verification are also presented.The developed techniques have been implemented in the verification tool UPPAAL. To demonstrate the potential applications of our model-checking techniques, we present three industrial-size case studies where the UPPAAL tool is applied.