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 it 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 a degraded mode