|
| EPSRC Reference: |
GR/N22960/01 |
| Title: |
VERIFICATION OF QUALITY OF SERVICE PROPERTIES IN TIMED SYSTEMS |
| Principal Investigator: |
Professor MZ Kwiatkowska |
| Other Investigators: |
|
| Researcher Co-investigator: |
|
| Project Partner: |
|
| Department: |
School of Computer Science |
| Organisation: |
University of Birmingham |
| Scheme: |
Standard Research |
| 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 |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary |
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.
|
| Final Report Summary |
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.
NEW ABSTRACT
The widespread reliance on the Internet, Broadband and wireless networks, both in business and at home, has emphasised the need for reliable, efficient and easy to configurable communication protocols capable of working in a genuinely distributed fashion. Such protocols increasingly often use randomisation and timing to avoid the need for a centralised authority; examples include IEEE 1394 FireWire root contention or Ipv4 ZeroConf dynamic configuration protocol. This project has focused on the foundations of the verification technology for randomised real-time protocols that enables automated checking of early protocol desgins agains a range of Quality of Servce properties including "there is a 99% chance that the packet will be delivered within 10ms". The project outcomes have been languages, models, algorithms and software prototypes to enhance the software tool PRISM.
(www.cs.bham.ac.uk/~dxp/prism/) being developed at Birmingham. We have additionally studied and analysed a number of industrially relevant protocols (including FireWire and ZeroConf) with the help of PRISM, identiying design errors in some.
|
| Further Information: |
|
| Organisation Website: |
http://www.bham.ac.uk |
|
|