Sciweavers

Share
ICECCS
1999
IEEE

Practical Considerations in Protocol Verification: The E-2C Case Study

12 years 2 months ago
Practical Considerations in Protocol Verification: The E-2C Case Study
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 datagram 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 ...
Yifei Dong, Scott A. Smolka, Eugene W. Stark, Step
Added 03 Aug 2010
Updated 03 Aug 2010
Type Conference
Year 1999
Where ICECCS
Authors Yifei Dong, Scott A. Smolka, Eugene W. Stark, Stephanie M. White
Comments (0)
books