Model Checking Timed Systems with Restricted Resources: Algorithms and Complexity

Computer software and hardware systems are among the most complexartifacts created by humans, thus it is not surprising that they often suffercostly 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 mathematicalmodel of a given system and then checking, automatically orsemi-automatically, that the model meets a given formal specification.One of the main challenges of this task is the so-called stateexplosion problem. For example, a 10 mega-byte cache has10^(20,000,000) states. The challenge presented by the stateexplosion problem has spurred the development of a rich body oftechniques, incorporating ideas from automata theory, artificialintelligence, combinatorial optimization, game theory, graph theoryand mathematical logic. In 2007 Clarke, Emerson and Sifakis wereawarded a Turing award (the Computer Science equivalent of a Nobleprize) 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 correctnessor acceptability of such systems can depend on real-time constraints,e.g., the response time of an anti-lock braking system or the latencyin video transmission. The state explosion problem is particularlyacute for real-time systems--indeed they are essentiallyinfinite-state systems. As a consequence, in real-time model checkingone must take great care in designing the modelling and specificationformalisms. Apparently minor variations in these can lead to drasticchanges 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 modelchecking 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.