Specification and analysis of the AER/NCA active network protocol suite in real-time maude

Abstract

This paper describes the application of the Real-Time Maude tool and the Maude formal methodology to the specification and analy- sis of the AER/NCA suite of active network multicast protocol compo- nents. Because of the time-sensitive and resource-sensitive behavior and the components of its components, AER/NCA poses challenging new problems for its formal specification and analysis. Real-Time Maude is a natural extension of the Maude rewriting logic language and tool for the specification and analysis of real-time object-based distributed systems. It supports a wide spectrum of formal methods, including: executable specification; symbolic simulation; and infinite-state model checking of temporal logic formulas. These methods complement those offered by finite-state model checkers and general-purpose theorem provers. Real- Time Maude has proved to be well-suited to meet the AER/NCA model- ing challenges, and its methods have been effective in uncovering subtle and important errors in the informal use case specification.