We present an industrial project conducted at Ericsson Danmark A/S, Telebit where formal methods in the form of Coloured Petri Nets (CP-nets or CPNs) have been used for the specification of an interoperability protocol for routing packets between fixed core networks and mobile ad-hoc networks. The interoperability protocol ensures that a packet flow between a host in a core network and a mobile node in an ad-hoc network is always relayed via one of the closest gateways connecting the core network and the mobile ad-hoc network. This paper shows how integrated use of CP-nets and application-specific visualisation have been applied to build a model-based prototype of the interoperability protocol. The prototype consists of two parts: a CPN model that formally specifies the protocol mechanisms and a graphical user interface for experimenting with the protocol. The project demonstrates that the use of formal modelling combined with the use of application-specific visualisation can be an effective approach to rapidly construct an executable prototype of a communication protocol.
|Title of host publication||Proceedings of the 5th International Conference on Integrated Formal Methods (IFM 2005), 29 November - 02 December 2005, Eindhoven, The Netherlands|
|Editors||J. Romijn, G. Smith, J. Pol, van de|
|Place of Publication||Berlin|
|Publication status||Published - 2005|
|Name||Lecture Notes in Computer Science|