| EPSRC Reference: |
EP/E049028/1 |
| Title: |
Model-Checking Algorithms for Timed Systems |
| Principal Investigator: |
Ouaknine, Professor J |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Computer Science |
| Organisation: |
University of Oxford |
| Scheme: |
First Grant Scheme |
| Starts: |
01 October 2007 |
Ends: |
31 March 2011 |
Value (£): |
126,822
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
As computer systems become ubiquitous, it becomes increasingly urgent todevelop analysis techniques and tools to guarantee that they operate asintended. Many safety-critical systems deployed today, from ABS brakingtechnology in cars to avionics control, can be viewed as timed systems, in thattheir correct behaviour depends crucially on their meeting various timingconstraints.There is by now healthy body of techniques and tools dedicated to the analysisof untimed systems. Formal analysis methods for timed systems, however, arestill in their infancy. The goal of this project is to investigate thetheoretical underpinnings and practical applicability of algorithms foranalysing timed systems. More specifically, we intend to study a well-knownformalism for expressing timed specifications, called Metric Temporal Logic,and develop efficient algorithms for verifying that a given timed system(suitably represented mathematically as a so-called timed automaton) meets agiven Metric Temporal Logic formula.The project is based on very recent algorithmic breakthroughs concerning theanalysis of Metric Temporal Logic. We intend to study the complexity of suchalgorithms, as well as various heuristics for accelerating them. The flavour ofthe project is mainly theoretical; however, we aim to implement our work andtest it on various case studies to evaluate how well our algorithms work inpractice.
|
|
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
|
|
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 |