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 protocols 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: Case study, modelling, state spaces.
Modification Date?