@inproceedings{7e1abe9591914e6197b387eab74220dc,
title = "Software design, specification, and verification: Lessons learned from the Rether case study",
abstract = "RETHER is a software-based real-time ethernet protocol developed at SUNY Stony Brook. The purpose of this protocol is to provide guaranteed bandwidth and deterministic, periodic network access to multimedia applications over commodity ether-net hardware. It has been implemented in the FreeBSD 2.1.0 operating system, and is now being used to support the Stony Brook Video Server (SBVS), a low-cost, ethernet LAN-based server prodding real-time delivery of video to end-users from the server's disk subsystem. Using local model checking, as provided by the Concurrency Factory specification and verification environment, we showed (for a particular network configuration) that Rether indeed makes good on its bandwidth guarantees to real-time nodes without exposing non-real-time nodes to the possibility of starvation. In the course of specifying and verifying Rether, we identified an alternative design of the protocol that warranted further study due to potential efficiency gains. Again using model checking, we showed that this alternative design also possesses the properties of interest.",
author = "Xiaoqun Du and McDonnell, \{Kevin T.\} and Evangelos Nanos and Ramakrishna, \{Y. S.\} and Smolka, \{Scott A.\}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1997.; 6th International Algebraic Methodology and Software Technology Conference, AMAST 1997 ; Conference date: 13-12-1997 Through 17-12-1997",
year = "1997",
doi = "10.1007/bfb0000471",
language = "English",
isbn = "3540638881",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "185--198",
editor = "Michael Johnson",
booktitle = "Algebraic Methodology and Software Technology - 6th International Conference, AMAST 1997, Proceedings",
}