| EPSRC Reference: |
GR/N22960/01 |
| Title: |
VERIFICATION OF QUALITY OF SERVICE PROPERTIES IN TIMED SYSTEMS |
| Principal Investigator: |
Kwiatkowska, Professor MZ |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Birmingham |
| Scheme: |
Standard Research (Pre-FEC) |
| Starts: |
01 May 2000 |
Ends: |
31 July 2003 |
Value (£): |
184,387
|
| EPSRC Research Topic Classifications: |
| Fundamentals of Computing |
|
|
| EPSRC Industrial Sector Classifications: |
| Electronics |
Information Technologies |
| No relevance to Underpinning Sectors |
|
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
|
The design and analysis of many systems, eg embedded systems and multimedia protocols, requires knowledge of their real-time aspects, in addition to the functional requirements. Tools such as Uppaal and Kronos enable automatic verification of hard real-time constraints for such systems (eg the packet will be delivered within 10ms) but are unable at present to deal with soft deadlines. Soft deadlines are employed to establish if a certain target of quality of service is met mostly as opposed to always (eg the packet will be delivered with 10ms with probability 0.9). Probability is used to express the proportion of time during which the deadline will be met. Soft deadlines apply to models with exact as well as stochastic timing.This project aims to address the foundations of the verification of quality of service properties of real-time systems. The work will concentrate on the development of a suitable model, together with high-level specification languages and industrially-relevant case studies. Efficient model checking algorithms will be derived, with the view to inform the developers of the model checker FDR for CSP. The approach advocated here should be viewed as complementary to methods such as simulation, testing and verification via theorem proving.
|
|
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.bham.ac.uk |