@inbook{3b655010937e11dcbee902004c4f4f50,
title = "Specification and Validation of an Edge Router Discovery Protocol for Mobile Ad Hoc Networks",
abstract = "We present an industrial project at Ericsson Telebit A/S where Coloured Petri Nets (CP-nets or CPNs) have been used for the design and specification of an edge router discovery protocol for mobile ad-hoc networks. The Edge Router Discovery Protocol (ERDP) supports an edge router in a stationary core network in assigning network address prefixes to gateways in mobile ad-hoc networks. This paper focuses on how CP-nets and the CPN computer tools have been applied in the development of ERDP. A CPN model has been constructed that constitutes a formal executable specification of ERDP. Simulation and message sequence charts were used for initial investigations of the protocol's behaviour. Then state space analysis was applied to conduct a formal verification of the key properties of ERDP. Both the modelling, simulation, and subsequent state space analysis helped in identifying several omissions and errors in the design, demonstrating the benefits of using formal modelling and analysis in a protocol design process.",
keywords = "Message sequence chart, Wireless network, State space, Router, Transmission protocol, Information gateway, Distributed system, Ad hoc network, Formal specification, Formal verification, Message passing, Mobile computing, Design process, Colored Petri net",
author = "Kristensen, {Lars Michael} and Kurt Jensen",
year = "2004",
language = "English",
isbn = "3-540-23135-8",
volume = "3147",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "248--269",
editor = "H. Ehrig and W. Damm and J. Desel and M. Grosse-Rhode and W. Reif and E. Schneider and E. Westk{\"a}mper",
booktitle = "Integration of Software Specification Techniques for Applications in Engineering",
address = "Netherlands",
}