Specification and Validation of an Edge Router Discovery Protocol for Mobile Ad Hoc Networks

Research output: Contribution to book/anthology/report/proceedingReport chapterResearch

  • Department of Computer Science
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.
Original languageEnglish
Title of host publicationIntegration of Software Specification Techniques for Applications in Engineering : Priority Program SoftSpez of the German Research Foundation. Final Report
EditorsH. Ehrig, W. Damm, J. Desel, M. Grosse-Rhode, W. Reif, E. Schneider, E. Westkämper
Number of pages20
Volume3147
PublisherSpringer
Publication year2004
Pages248-269
ISBN (print)3-540-23135-8
Publication statusPublished - 2004
SeriesLecture Notes in Computer Science
Volume3147
ISSN0302-9743

    Research areas

  • 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

See relations at Aarhus University Citationformats

ID: 8987343