EPSRC logo

Details of Grant 

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:
Information Technologies
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