Model Checking Timed Automata - Techniques and Applications

Abstract

Model checking is a technique to automatically analyse systems that have been modeled in a formal language. The timed automaton framework is such a formal language. It is suitable to model many realistic problems in which time plays a central role. Examples are distributed algorithms, protocols, embedded software and scheduling problems. The main problem with model checking is the exponential growth of the state space as models become larger (also known as the 'state space explosion' problem). This thesis consists of six research papers. Three of these contribute theory to alleviate the state space explosion problem. The other three demonstrate the practical use of model checking technology by applying it to realistic case studies.