Implementing the WebSocket Protocol Based on Formal Modelling and Automated Code Generation

Kent Inge Simonsen, Lars Michael Kristensen

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

Model-based software engineering offers several attractive benefits for the implementation of protocols, including automated code generation for different platforms from design-level models. In earlier work, we have proposed a template-based approach using Coloured Petri Net formal models with pragmatic annotations for automated code generation of protocol software. The contribution of this paper is an application of the approach as implemented in the PetriCode tool to obtain protocol software implementing the IETF WebSocket protocol. This demonstrates the scalability of our approach to real protocols. 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 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.
Original languageEnglish
Title of host publicationDistributed Applications and Interoperable Systems : Proceedings of the 14th IFIP WG 6.1 International Conference, DAIS 2014
EditorsKostas Magoutis, Peter Pietzuch
PublisherSpringer
Publication date2014
Pages104-118
ISBN (Print)978-3-662-43351-5
ISBN (Electronic)978-3-662-43352-2
DOIs
Publication statusPublished - 2014
Event14th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS) 2014, DAIS 2014 - Berlin, Germany
Duration: 3 Jun 20145 Jun 2014
Conference number: 14
http://www.ics.forth.gr/dais14/

Conference

Conference14th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS) 2014, DAIS 2014
Number14
Country/TerritoryGermany
CityBerlin
Period03/06/201405/06/2014
OtherPart of the 9th International Federated Conference on Distributed Computing Techniques (DisCoTec) 2014
Internet address
SeriesLecture Notes in Computer Science
Volume8460
ISSN0302-9743

Keywords

  • Protocol software for pervavise computing
  • odel-based protocol developmen
  • protocol verification
  • Coloured Petri Nets

Fingerprint

Dive into the research topics of 'Implementing the WebSocket Protocol Based on Formal Modelling and Automated Code Generation'. Together they form a unique fingerprint.

Cite this