Sciweavers

FMSD
2006

Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude

13 years 11 months ago
Specification and analysis of the AER/NCA active network protocol suite in Real-Time Maude
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. RealTime 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 i...
Peter Csaba Ölveczky, José Meseguer, C
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where FMSD
Authors Peter Csaba Ölveczky, José Meseguer, Carolyn L. Talcott
Comments (0)