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 ...

• Type: Conference
• Year: 1999
• Where: ICECCS
• Authors: Yifei Dong, Scott A. Smolka, Eugene W. Stark, Stephanie M. White
• Keywords: Hardware, Hawkeye Early Warning, ICECCS 1999, Normal E-2c Operating, SPIN Verification Tool