Formal specification and analysis of active networks and communication protocols: The Maude experience

G. Denker, J. Meseguer, C. Talcott

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

Abstract

Rewriting logic and the Maude language make possible a new methodology in which formal modeling and analysis can be used from the earliest phases of system design to uncover many errors and inconsistencies, and to reach high assurance for critical components. Our methodology is arranged as a sequence of increasingly stronger methods, including formal modeling, executable specification, model-checking analysis, narrowing, and formal proof, some of which can be used selectively according to the specific needs of each application. The paper reports on a number of experiments and case studies applying this formal methodology to active networks, communication protocols, and security protocols.

Original languageEnglish (US)
Title of host publicationProceedings - DARPA Information Survivability Conference and Exposition, DISCEX 2000
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages251-265
Number of pages15
ISBN (Electronic)0769504906, 9780769504902
DOIs
StatePublished - 2000
Externally publishedYes
EventDARPA Information Survivability Conference and Exposition, DISCEX 2000 - Hilton Head, United States
Duration: Jan 25 2000Jan 27 2000

Publication series

NameProceedings - DARPA Information Survivability Conference and Exposition, DISCEX 2000
Volume1

Other

OtherDARPA Information Survivability Conference and Exposition, DISCEX 2000
CountryUnited States
CityHilton Head
Period1/25/001/27/00

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Information Systems
  • Information Systems and Management
  • Electrical and Electronic Engineering
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'Formal specification and analysis of active networks and communication protocols: The Maude experience'. Together they form a unique fingerprint.

Cite this