Formal Specification and Analysis of Active Networks and
Communication Protocols: The Maude Experience
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.