Name
Abstract | ||
|---|---|---|
In this paper we present a case-study in which the tool Uppaal is extended and applied to verify an audio-control protocol developed by Philips. The size of the protocol studied in this paper is significantly larger than case studies, including various abstract versions of the same protocol without bus-collision handling, reported previously in the community of real-time verification. We have checked that the protocol will function correctly if the timing error of its components is bound to ±5%, and incorrectly if the error is ±6%. In addition, using Uppaal’s ability of generating diagnostic traces, we have studied an erroneous version of the protocol actually implemented by Philips, and constructed a possible execution sequence explaining the error. During the case-study, Uppaal was extended with the notion of committed locations. It allows for accurate modelling of atomic behaviours, and more importantly, it is utilised to guide the state-space exploration of the model checker to avoid exploring unnecessary interleavings of independent transitions. Our experimental results demonstrate considerable time and space-savings of the modified model checking algorithm. In fact, due to the huge time and memory-requirement, it was impossible to check a simple reachability property of the protocol before the introduction of committed locations, and now it takes only seconds. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1016/S1567-8326(02)00036-X | The Journal of Logic and Algebraic Programming |
Keywords | Field | DocType |
Protocol verification,Requirements/specifications,Design tools and techniques,Software/program verification | Functional verification,Programming language,Model checking,Computer science,Timing error,Verification,Real-time computing,Theoretical computer science,Reachability,Protocol verification | Journal |
Volume | ISSN | Citations |
52 | 1567-8326 | 20 |
PageRank | References | Authors |
1.09 | 17 | 7 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Johan Bengtsson | 1 | 1048 | 60.86 |
| W. O. David Griffioen | 2 | 160 | 17.33 |
| Kåre J. Kristoffersen | 3 | 143 | 19.32 |
| Kim G. Larsen | 4 | 3922 | 254.03 |
| Fredrik Larsson | 5 | 577 | 45.55 |
| Paul Pettersson | 6 | 2636 | 174.89 |
| Wang Yi | 7 | 4232 | 332.05 |