|
Published Articles >> Table of Contents >> Abstract
Fifth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'99)
p. 153
Practical Considerations in Protocol Verification: The E-2C Case Study
Yifei Dong, State University of New York at Stony Brook
Scott A. Smolka, State University of New York at Stony Brook
Eugene W. Stark, State University of New York at Stony Brook
Stephanie M. White, Long Island University
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ICECCS.1999.802859
Send link to a friend
| Abstract |
|
We report on our efforts to formally specify and verify a new protocol of the E-2C Hawkeye Early Warning Aircraft. The protocol, which is currently in test at Northrop Grumman, supports communication between a Mission Computer (MC) and three or more Tactical Workstations (TWSs), connected by a single-segment LAN. We modeled the protocol in the PROMELA specification language of the SPIN verification tool, and used SPIN to analyze a number of properties of the protocol. Our investigation revealed a race condition that can lead to a disconnect of an MC/TWS connection when there is one lost UDP data-gram and significant timing delays. Such delays are virtually impossible under normal E-2C operating conditions, but could be due to noise on the MC/TWS LAN. A simple modification was proposed that avoids the disconnect in many situations. Practical considerations, however, mandated that the protocol be left as is: shutting down a noisy connection and reinitializing the TWS, with minimal delay and loss of information to the operator, was deemed preferable to operating in degraded mode.
|
 Additional Information
|
Citation:
Yifei Dong, Scott A. Smolka, Eugene W. Stark, Stephanie M. White,
"Practical Considerations in Protocol Verification: The E-2C Case Study,"
iceccs,
p. 153,
Fifth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'99),
1999
|
|
