A language-based approach to protocol construction
Anindya Basu · 1998
User-level network architectures that provide applications with direct access to network hardware have become popular with the emergence of high-speed networking technologies such as ATM and Fast Ethernet. However, experience with user-level network architectures such as U-Net [vEBBV95] has shown that building correct and efficient protocols on such architectures is a challenge. To address this problem, Promela++, an extension of the Promela protocol validation language has been developed. Promela++ allows automatic verification of protocol correctness against programmer specified safety requirements. Furthermore, Promela++ can be compiled to efficient C code. Thus far, the results are encouraging: the C code produced by the Promela++ compiler shows performance comparable to hand-coded versions of a relatively simple protocol. 1 Introduction Recent research in high-speed network interfaces has focused on removing the operating system from the critical path of communication. An effecti...