Formal Modeling and Analysis of an IETF Multicast Protocol

This paper describes the application of Real-Time Maude to the formal modeling, simulation, and model checking analysis of the NORM multicast protocol standard being developed by the Internet Engineering Task Force. Because of its size and sophistication, real-time features, and the need to model and analyze subcomponents of NORM both in isolation and in combination, NORM poses a set of challenging problems for its formal specification and analysis. Our formal modeling and analysis efforts made its aware of ambiguities, inconsistencies, and cases of under-specification in the informal specification of NORM. Our work indicates that formal methods can successfully be applied by non-experts during the development of advanced Internet protocol standards.