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

Peter Csaba Ölveczky, Mark Keaton, José Meseguer, Carolyn Talcott, Steve Zabele

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationFundamental Approaches to Software Engineering - 4th International Conference, FASE 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Proceedings
EditorsHeinrich Hussmann
PublisherSpringer-Verlag Berlin Heidelberg
Pages333-347
Number of pages15
ISBN (Print)3540418636, 9783540418634
DOIs
StatePublished - 2001
Externally publishedYes
Event4th International Conference on Fundamental Approaches to Software Engineering, FASE 2001, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 - Genova, Italy
Duration: Apr 2 2001Apr 6 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2029
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other4th International Conference on Fundamental Approaches to Software Engineering, FASE 2001, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001
CountryItaly
CityGenova
Period4/2/014/6/01

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Specification and analysis of the AER/NCA active network protocol suite in real-time maude'. Together they form a unique fingerprint.

  • Cite this

    Ölveczky, P. C., Keaton, M., Meseguer, J., Talcott, C., & Zabele, S. (2001). Specification and analysis of the AER/NCA active network protocol suite in real-time maude. In H. Hussmann (Ed.), Fundamental Approaches to Software Engineering - 4th International Conference, FASE 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Proceedings (pp. 333-347). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2029). Springer-Verlag Berlin Heidelberg. https://doi.org/10.1007/3-540-45314-8_24