University of Illinois Urbana-Champaign

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

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

Content Files
Specification and Analysis of the AER-NCA Active Network Protocol Suite in Real-Time Maude.pdf

Permalink

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

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
Date of Ingest
2009-04-16T19:02:18Z
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
Genre of Resource
Technical Report
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

Research and Tech Reports - Computer Science PRIMARY