Specification and Analysis of the AER/NCA Active Network Protocol Suite in Real-Time Maude

P. C. Ölveczky, M. Keaton, J. Meseguer, C. Talcott, and S. Zabele

This paper describes the application of the Real-Time Maude tool and the Maude formal methodology to the specification and analysis of the AER/NCA suite of active network multicast protocol components. Because of the time-sensitive and resource-sensitive behavior and the composability 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 modeling challenges, and its methods have been effective in uncovering subtle and important errors in the informal use case specification.

(BibTeX entry)    (gzip'ed Postscript)   

back   home   Formal Methods and Declarative Languages Laboratory   Computer Science Laboratory, SRI International