[Home] [CV] [Publications]


Minus 1a5aa4f1c08b567c9107cba729de26bc87c17ab2b2f690eb45059193a1d6f587 Maude as a Wide-Spectrum Framework for Formal Modeling and Analysis of Active Networks
Meseguer, J. and Olveczky, P. C. and Stehr, M.-O. and Talcott, C. L. - 2002

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.