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.

• discexMaude99.ps