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. In this report, 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 network language.
| Limitations: |
 APPROVED FOR PUBLIC RELEASE |
| Description: |
Final technical rept. Aug 1997-Dec 2001 |
| Pages: |
30 |
| Report Date: |
AUG 2002 |
| Contract Number: |
F30602-97-C-0312, DARPA ORDER- |
| Report Number: |
A298604 |
|
|
|
|
Keywords relating to this report:
