Maude as a wide-spectrum framework for formal modeling and analysis of active networks

J. Meseguer, P. C. Olveczky, M. O. Stehr, C. Talcott

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

Abstract

Modeling and formally analyzing active network systems and protocols is quite challenging, due to their highly dynamic nature and the need for new network models. We propose a wide-spectrum methodology using executable rewriting logic specifications to address this challenge. We also show how, using the Maude rewriting logic language and tools, active network systems, languages, and protocols can be formally specified and analyzed using a wide range of formal methods. Benefits include precise documentation of designs, early discovery of many bugs and omissions, and higher assurance of correct behavior. In this paper we illustrate these methods and their practical usefulness through two case studies: the AER/NCA protocol suite and the PLAN active networks language.

Original languageEnglish (US)
Title of host publicationProceedings - DARPA Active Networks Conference and Exposition, DANCE 2002
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages494-510
Number of pages17
ISBN (Electronic)0769515649, 9780769515649
DOIs
StatePublished - Jan 1 2002
EventDARPA Active Networks Conference and Exposition, DANCE 2002 - San Francisco, United States
Duration: May 29 2002May 30 2002

Publication series

NameProceedings - DARPA Active Networks Conference and Exposition, DANCE 2002

Other

OtherDARPA Active Networks Conference and Exposition, DANCE 2002
Country/TerritoryUnited States
CitySan Francisco
Period5/29/025/30/02

Keywords

  • Computer bugs
  • Computer science
  • Documentation
  • Electronic switching systems
  • Informatics
  • Laboratories
  • Logic testing
  • Protocols
  • Prototypes
  • Routing

ASJC Scopus subject areas

  • Computer Networks and Communications

Fingerprint

Dive into the research topics of 'Maude as a wide-spectrum framework for formal modeling and analysis of active networks'. Together they form a unique fingerprint.

Cite this