EPSRC logo

Details of Grant 

EPSRC Reference: EP/G069727/1
Title: Model Checking Timed Systems with Restricted Resources: Algorithms and Complexity
Principal Investigator: Worrell, Professor JB
Other Investigators:
Researcher Co-Investigators:
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 DatePanel NameOutcome
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 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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
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