Model Checking Timed Systems with Restricted Resources: Algorithms and Complexity

Computer software and hardware systems are among the most complex artifacts created by humans, thus it is not surprising that they often suffer costly or catastrophic failures due to errors in design. In 2002 a study by the US National Institute of Standard and Technology estimated that software failures alone cost the US economy 60 billion dollars per year. Against this background it is increasingly recognized that model checking - an approach to formally verifying the correctness of software and hardware systems - has an important role to play in meeting the challenge of producing correctly functioning systems. Intel, Lucent, Microsoft, Motorola, and NASA, among many others, already use model checking as part of their quality assurance process.

In a nutshell, model checking involves constructing a mathematical model of a given system and then checking, automatically or semi-automatically, that the model meets a given formal specification. One of the main challenges of this task is the so-called state explosion problem. For example, a 10 megabyte cache has 10^(20,000,000) states. The challenge presented by the state explosion problem has spurred the development of a rich body of techniques, incorporating ideas from automata theory, artificial intelligence, combinatorial optimization, game theory, graph theory and mathematical logic. In 2007 Clarke, Emerson and Sifakis were awarded a Turing award (the Computer Science equivalent of a Noble prize) for their pioneering work in model checking.

In this project we are concerned in particular with real-time systems, such as hardware, controllers and embedded systems. The correctness or acceptability of such systems can depend on real-time constraints, e.g., the response time of an anti-lock braking system or the latency in video transmission. The state explosion problem is particularly acute for real-time systems - indeed they are essentially infinite-state systems. As a consequence, in real-time model checking one must take great care in designing the modelling and specification formalisms. Apparently minor variations in these can lead to drastic changes in the tractability of model checking.

The aim of this project is to identify modelling and specification formalisms that can express the type of system requirements described above, that also permit model checking algorithms that have reasonable complexity. An important outcome of this project will be algorithms and tools for model checking real-time systems. Such algorithms will employ novel combinatorial and automata-theoretic ideas, and will use symbolic techniques to permit exhaustive search of infinite state spaces. Another outcome of this project will be to enhance understanding of the use of temporal logics for reasoning about real-time behaviours, building on the highly successful use of temporal logics for discrete-time systems.