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

Kent Inge Simonsen; Lars Michael Kristensen

doi:10.1007/978-3-662-43352-2_9

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

Kent Inge Simonsen
, Lars Michael Kristensen

Department of Applied Mathematics and Computer Science

Western Norway University of Applied Sciences

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Distributed Applications and Interoperable Systems : Proceedings of the 14th IFIP WG 6.1 International Conference, DAIS 2014
Editors	Kostas Magoutis, Peter Pietzuch
Publisher	Springer
Publication date	2014
Pages	104-118
ISBN (Print)	978-3-662-43351-5
ISBN (Electronic)	978-3-662-43352-2
DOIs	https://doi.org/10.1007/978-3-662-43352-2_9
Publication status	Published - 2014
Event	14th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS) 2014, DAIS 2014 - Berlin, Germany Duration: 3 Jun 2014 → 5 Jun 2014 Conference number: 14 http://www.ics.forth.gr/dais14/

Conference

Conference	14th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS) 2014, DAIS 2014
Number	14
Country/Territory	Germany
City	Berlin
Period	03/06/2014 → 05/06/2014
Other	Part of the 9th International Federated Conference on Distributed Computing Techniques (DisCoTec) 2014
Internet address	http://www.ics.forth.gr/dais14/

Series	Lecture Notes in Computer Science
Volume	8460
ISSN	0302-9743

Keywords

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

Access to Document

10.1007/978-3-662-43352-2_9

OpenUrl availability

Check availability in DTU Findit

Cite this

Simonsen, Kent Inge ; Kristensen, Lars Michael. / Implementing the WebSocket Protocol Based on Formal Modelling and Automated Code Generation. Distributed Applications and Interoperable Systems: Proceedings of the 14th IFIP WG 6.1 International Conference, DAIS 2014. editor / Kostas Magoutis ; Peter Pietzuch. Springer, 2014. pp. 104-118 (Lecture Notes in Computer Science, Vol. 8460).

@inproceedings{e33a2b07f871416bb28ea82de4928916,

title = "Implementing the WebSocket Protocol Based on Formal Modelling and Automated Code Generation",

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.",

keywords = "Protocol software for pervavise computing, odel-based protocol developmen, protocol verification, Coloured Petri Nets",

author = "Simonsen, \{Kent Inge\} and Kristensen, \{Lars Michael\}",

year = "2014",

doi = "10.1007/978-3-662-43352-2\_9",

language = "English",

isbn = "978-3-662-43351-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "104--118",

editor = "Kostas Magoutis and Peter Pietzuch",

booktitle = "Distributed Applications and Interoperable Systems",

note = "14th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS) 2014, DAIS 2014, DAIS 2014 ; Conference date: 03-06-2014 Through 05-06-2014",

url = "http://www.ics.forth.gr/dais14/",

}

Simonsen, KI & Kristensen, LM 2014, Implementing the WebSocket Protocol Based on Formal Modelling and Automated Code Generation. in K Magoutis & P Pietzuch (eds), Distributed Applications and Interoperable Systems: Proceedings of the 14th IFIP WG 6.1 International Conference, DAIS 2014. Springer, Lecture Notes in Computer Science, vol. 8460, pp. 104-118, 14th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS) 2014, DAIS 2014, Berlin, Germany, 03/06/2014. https://doi.org/10.1007/978-3-662-43352-2_9

Implementing the WebSocket Protocol Based on Formal Modelling and Automated Code Generation. / Simonsen, Kent Inge; Kristensen, Lars Michael.
Distributed Applications and Interoperable Systems: Proceedings of the 14th IFIP WG 6.1 International Conference, DAIS 2014. ed. / Kostas Magoutis; Peter Pietzuch. Springer, 2014. p. 104-118 (Lecture Notes in Computer Science, Vol. 8460).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

TY - GEN

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

AU - Simonsen, Kent Inge

AU - Kristensen, Lars Michael

N1 - Conference code: 14

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

KW - Protocol software for pervavise computing

KW - odel-based protocol developmen

KW - protocol verification

KW - Coloured Petri Nets

U2 - 10.1007/978-3-662-43352-2_9

DO - 10.1007/978-3-662-43352-2_9

M3 - Article in proceedings

SN - 978-3-662-43351-5

T3 - Lecture Notes in Computer Science

SP - 104

EP - 118

BT - Distributed Applications and Interoperable Systems

A2 - Magoutis, Kostas

A2 - Pietzuch, Peter

PB - Springer

T2 - 14th IFIP International Conference on Distributed Applications and Interoperable Systems (DAIS) 2014, DAIS 2014

Y2 - 3 June 2014 through 5 June 2014

ER -

Simonsen KI, Kristensen LM. Implementing the WebSocket Protocol Based on Formal Modelling and Automated Code Generation. In Magoutis K, Pietzuch P, editors, Distributed Applications and Interoperable Systems: Proceedings of the 14th IFIP WG 6.1 International Conference, DAIS 2014. Springer. 2014. p. 104-118. (Lecture Notes in Computer Science, Vol. 8460). doi: 10.1007/978-3-662-43352-2_9

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

Abstract

Conference

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this