|
| EPSRC Reference: |
EP/G069727/1 |
| Title: |
Model Checking Timed Systems with Restricted Resources: Algorithms and Complexity |
| Principal Investigator: |
Dr JB Worrell |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
Computing Laboratory |
| Organisation: |
University of Oxford |
| Scheme: |
First Grant Scheme |
| Starts: |
10 January 2010 |
Ends: |
09 July 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 |
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 mega-byte 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.
|
| Final Report Summary |
|
No final report summary is available for this grant.
|
| Further Information: |
|
| Organisation Website: |
http://www.ox.ac.uk |
|
|