Funded by:
(grant reference GR/N22960/01)
Dates: 2000-2003
| Institutions: |  | University of Birmingham |
The design and analysis of many systems, to mention communication protocols, embedded systems and multimedia protocols, requires detailed knowledge of their real-time aspects, in addition to the functional requirements. Recent advances in software technology underpinning verification tools have brought automatic verification of real-time systems into the realm of industrial applications. This is evident through the success of case studies, ranging from the gear box controller to Philips audio protocol, performed with the help of model checkers such as Uppaal.
However, existing tools can only verify deterministic (hard) deadlines, i.e. properties such as "if the packet is sent then it will be delivered within 80 ms". In the presence of lossy media or faulty hardware, hard deadlines can be too restrictive. Probabilistic (soft) deadlines provide a viable alternative; these express the probability of a certain target of quality of service being achieved (here delivery occurring within 80 ms with probability at least 90%/at most 3%). For applications such as audio or multimedia protocols, which process and transmit continuous media data, it is often necessary to allow stochastic timing, in the sense that the user could specify that packets are sent according to exponential or normal distribution. In such cases, measures such as mean time to delivery are additionally required.
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, developed and marketed by Formal Systems (Europe) Ltd., for CSP. The approach advocated here should not be viewed as an alternative to methods such as simulation, testing and verification via theorem proving, but rather as a complementary technique.
This project aims to: