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

Olveczky, Peter C.; Meseguer, José; Talcott, Carolyn L.

Permalink

https://hdl.handle.net/2142/10892 Copy

Description

Title

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

Author(s)

• Olveczky, Peter C.
• Meseguer, José
• Talcott, Carolyn L.

Issue Date

2004-08

Keyword(s)

Formal Methods

Abstract

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, the presence of probabilistic algorithms, 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; breadth-first search for failures of safety properties in infinite-state systems; and linear temporal logic model checking of time-bounded temporal logic formulas. These methods complement those offered by network simulators on the one hand, and timed-automaton-based tools and general-purpose theorem provers on the other. Our experience shows that Real-Time Maude is well-suited to meet the AER/NCA modeling challenges, and that its methods have proved effective in uncovering subtle and important errors in the informal use case specification.

Type of Resource

text

Permalink

http://hdl.handle.net/2142/10892

Copyright and License Information

You are granted permission for the non-commercial reproduction, distribution, display, and performance of this technical report in any format, BUT this permission is only for a period of 45 (forty-five) days from the most recent time that you verified that this technical report is still available from the University of Illinois at Urbana-Champaign Computer Science Department under terms that include this permission. All other rights are reserved by the author(s).

Owning Collections