Sciweavers

POPL
2005
ACM

Formal prototyping in early stages of protocol design

14 years 5 months ago
Formal prototyping in early stages of protocol design
Network protocol design is usually an informal process where debugging is based on successive iterations of a prototype implementation. The feedback provided by a prototype can be indispensable since the requirements are often incomplete at the start. A drawback of this technique is that errors in protocols can be notoriously difficult to detect by testing alone. Applying formal methods such as theorem proving can greatly increase one's confidence that the protocol is correct. However, formal methods can be tedious to use, rarely support successive design iterations and prototyping, are difficult to scale to entire designs, and typically require a clear understanding of requirements in advance. We investigate how formal simulation based on Maude executable specifications overcomes many of these hurdles. We apply this technique in the early stages of the design of a new security protocol, known as Layer 3 Accounting (L3A), aimed at protecting known vulnerabilities in the wireless ...
Alwyn Goodloe, Carl A. Gunter, Mark-Oliver Stehr
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where POPL
Authors Alwyn Goodloe, Carl A. Gunter, Mark-Oliver Stehr
Comments (0)