-
The vast majority of software systems today can be characterised as
concurrent and distributed systems as their operation inherently relies on protocols
executed between independently scheduled software components. The
engineering of correct protocols can be a challenging task due to their complex behaviour
which may result in subtle errors if not carefully designed. Ensuring
interoperability between independently made implementations is also challenging due to
ambiguous protocol specifications. Model-based software engineering offers
several attractive benefits for the implementation of protocols, including automated
code generation for different platforms from design-level models. Furthermore,
the use of formal modelling in combination with model checking provides
techniques to support the development of reliable protocol implementations.
Coloured Petri Nets (CPNs) [
3
] is formal language combining Petri Nets
with a programming language to obtain a modelling language that scales to
large systems. In CPNs, Petri Nets provide the primitives for modelling
concurrency and synchronisation while the Standard ML programming language
provides the primitives for modelling data and data manipulation. CPNs have
been successfully applied for the modelling and verification of many protocols,
including Internet protocols such as the TCP, DCCP, and DYMO protocols [
1,
4
]. Formal modelling and verification have been useful in gaining insight into the
operation of the protocols considered and have resulted in improved protocol
specifications. However, earlier work has not fully leveraged the investment in
modelling by also taking the step to automated code generation as a way to
obtain an implementation of the protocol under consideration.
In earlier work [
5
], we have proposed the PetriCode approach and a
supporting software tool [
7
] has been developed for automatically generating protocol
implementations based on CPN models. The basic idea of the approach is to
enforce particular modelling patterns and annotate the CPN models with code
generation pragmatics. The pragmatics are bound to code generation templates
and used to direct a template-based model-to-text transformation that generates
the protocol implementation. As part of earlier work, we have demonstrated the
use of the PetriCode approach on small protocols. In addition, it has been shown
that our approach supports code generation for multiple platforms, and that it
leads to code that is readable and also compatible with other software [
6
].
PNSE’14 – Petri Nets and Software Engineering
In the present work we consider the application of our code generation
approach as implemented in the PetriCode tool to obtain protocol software
implementing the IETF WebSocket protocol [
2
] protocol for the Groovy language
and platform. This demonstrates that our approach and tool scales to
industrialsized protocols. The WebSocket protocol is a relatively new protocol and makes
it possible to upgrade an HTTP connection to an efficient message-based
fullduplex connection. WebSocket has already become a popular protocol for several
web-based applications such as games and media streaming services where
bidirectional communication with low latency is needed.
The contributions of our work include showing how we have been able to
model the WebSocket protocol following the PetriCode modelling conventions.
Furthermore, we perform formal verification of the CPN model prior to code
generation, and test the implementation for interoperability against the Autobahn
WebSocket test-suite [
8
] resulting in 97% and 99% success rate for the client and
server implementation, respectively. The tests show that the cause of test
failures were mostly due to local and trivial errors in newly written code-generation
templates, and not related to the overall logical operation of the protocol as
specified by the CPN model. Finally, we demonstrate in this paper that the
generated code is interoperable with other WebSocket implementations.
Acknowledgement. The results presented in this invited talk is based on joint
work with Kent I.F. Simonsen, Bergen University College and the Technical
University of Denmark, and Ekkart Kindler, the Technical University of Denmark.