Name
Abstract | ||
|---|---|---|
This paper describes a local model-checking al- gorithm for the alternation-free fragment of the modal mu- calculus that has been implemented in the Concurrency Fac- tory and discusses its application to the analysis of a real- time communications protocol. The protocol considered is RETHER, a software-based, real-time Ethernet protocol de- veloped at SUNY at Stony Brook. Its purpose is to provide guaranteed bandwidth and deterministic, periodic network ac- cess to multimedia applications over commodity Ethernet hard- ware. Our model-checking results show that (for a particular network configuration) RETHER makes good on its band- width guarantees to real-time nodes without exposing non- real-time nodes to the possibility of starvation. Our data also indicate that, in many cases, the state-exploration overhead of the local model checker is significantly smaller than the total amount that would result from a global analysis of the protocol. In the course of specifying and verifying RETHER ,w e also identified an alternative design of the protocol that war- ranted further study due to its potentially smaller run-time overhead. Again, using local model checking, we showed that this alternative design also possesses the properties of inter- est. This observation points up one of the often-overlooked benefits of formal verification: by forcing designers to under- stand their designs rigorously and abstractly, these techniques often enable the designers to uncover interesting design alter- natives. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/s100090050031 | STTT |
Keywords | Field | DocType |
model checking,real-time,modal mu-calculus,state explosion,protocol verification,real time,protocol analysis,global analysis,formal verification | Model checking,Protocol analysis,Data transmission,Computer science,Concurrency,Real-time computing,Theoretical computer science,Ethernet,Access network,Distributed computing,Formal verification,Communications protocol | Journal |
Volume | Issue | Citations |
2 | 3 | 15 |
PageRank | References | Authors |
0.70 | 23 | 3 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Xiaoqun Du | 1 | 225 | 12.32 |
| Scott A. Smolka | 2 | 2959 | 249.22 |
| Rance Cleaveland | 3 | 2266 | 254.39 |