EPSRC Reference: 
EP/G069727/1 
Title: 
Model Checking Timed Systems with Restricted Resources: Algorithms and Complexity 
Principal Investigator: 
Worrell, Professor JB 
Other Investigators: 

Researcher CoInvestigators: 

Project Partners: 

Department: 
Computer Science 
Organisation: 
University of Oxford 
Scheme: 
First Grant Scheme 
Starts: 
10 January 2010 
Ends: 
09 September 2013 
Value (£): 
212,217

EPSRC Research Topic Classifications: 
Fundamentals of Computing 


EPSRC Industrial Sector Classifications: 
No relevance to Underpinning Sectors 


Related Grants: 

Panel History: 
Panel Date  Panel Name  Outcome 
24 Apr 2009

ICT Prioritisation Panel (April 09)

Announced


Summary on Grant Application Form 
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 checkingan approach to formally verifying the correctness of software and hardware systemshas 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 orsemiautomatically, that the model meets a given formal specification.One of the main challenges of this task is the socalled stateexplosion problem. For example, a 10 megabyte 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 realtime systems,such as hardware, controllers and embedded systems. The correctnessor acceptability of such systems can depend on realtime constraints,e.g., the response time of an antilock braking system or the latencyin video transmission. The state explosion problem is particularlyacute for realtime systemsindeed they are essentiallyinfinitestate systems. As a consequence, in realtime 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 realtime systems. Such algorithms will employ novel combinatorial and automatatheoretic 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 realtime behaviours, building on the highly successful use of temporal logics for discretetime systems.

Key Findings 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Potential use in nonacademic contexts 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Impacts 
Description 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk 
Summary 

Date Materialised 


Sectors submitted by the Researcher 
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk

Project URL: 

Further Information: 

Organisation Website: 
http://www.ox.ac.uk 