Local model checking and protocol analysis |
| |
Authors: | Xiaoqun Du Scott A Smolka Rance Cleaveland |
| |
Affiliation: | (1) Department of Computer Science, SUNY at Stony Brook, Stony Brook, NY 11794-4400, USA, US |
| |
Abstract: | This paper describes a local model-checking algorithm for the alternation-free fragment of the modal mu-calculus that has
been implemented in the Concurrency Factory 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 developed at SUNY at Stony Brook. Its purpose is to provide guaranteed bandwidth
and deterministic, periodic network access to multimedia applications over commodity Ethernet hardware. Our model-checking
results show that (for a particular network configuration) RETHER makes good on its bandwidth 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, we also identified an alternative design of the protocol that warranted further study due to its potentially smaller run-time
overhead in servicing requests for data transmission. Again, using local model checking, we showed that this alternative design
also possesses the properties of interest. This observation points out one of the often-overlooked benefits of formal verification:
by forcing designers to understand their designs rigorously and abstractly, these techniques often enable the designers to
uncover interesting design alternatives. |
| |
Keywords: | : Model checking – Modal mu-calculus – Protocol verification – State explosion – Real-time |
本文献已被 SpringerLink 等数据库收录! |
|