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.
Chapter PDF
Similar content being viewed by others
Keywords
- Earthquake Early Warning
- Internal Service
- Earthquake Early Warning System
- Substitution Transition
- State Space Exploration
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Gupta, A.: Chat Sever using WebSocket in GlassFish 4, https://blogs.oracle.com/arungupta/entry/chat_sever_using_websocket_totd
Billington, J., Gallasch, G.E., Han, B.: A Coloured Petri Net Approach to Protocol Verification. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 210–290. Springer, Heidelberg (2004)
Brumbulli, M., Fischer, J.: SDL Code Generation for Network Simulators. In: Kraemer, F.A., Herrmann, P. (eds.) SAM 2010. LNCS, vol. 6598, pp. 144–155. Springer, Heidelberg (2011)
CPN Tools. Home Page, http://cpntools.org/ .
Fette, I., Melnikov, A.: The websocket protocol (2011), http://tools.ietf.org/html/rfc6455
Fischer, J., Kühnlenz, F., Ahrens, K., Eveslage, I.: Model-based Development of Self-organizing Earthquake Early Warning Systems. In: Proceedings of MATHMOD (2009)
Groovy. Project Web Site, http://groovy.codehaus.org
Jensen, K., Kristensen, L.M., Wells, L.: Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems. International Journal on Software Tools for Technology Transfer 9(3-4), 213–254 (2007)
Killian, C.E., Anderson, J.W., Braud, R., Jhala, R., Vahdat, A.M.: Mace: language support for building distributed systems. ACM SIGPLAN Notices 42, 179–188 (2007)
Kraemer, F.A., Bræk, R., Herrmann, P.: Compositional Service Engineering with Arctis. Telektronikk 105(2009.1) (2009)
Kristensen, L.M., Simonsen, K.I.F.: Applications of Coloured Petri Nets for Functional Validation of Protocol Designs. In: Jensen, K., van der Aalst, W.M.P., Balbo, G., Koutny, M., Wolf, K. (eds.) Transactions on Petri Nets and Other Models of Concurrency VII. LNCS, vol. 7480, pp. 56–115. Springer, Heidelberg (2013)
Kristensen, L.M., Westergaard, M.: Automatic Structure-Based Code Generation from Coloured Petri Nets: A Proof of Concept. In: Kowalewski, S., Roveri, M. (eds.) FMICS 2010. LNCS, vol. 6371, pp. 215–230. Springer, Heidelberg (2010)
Kummer, O., Wienberg, F., Duvigneau, M., Schumacher, J., Köhler, M., Moldt, D., Rölke, H., Valk, R.: An Extensible Editor and Simulation Engine for Petri Nets: Renew. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 484–493. Springer, Heidelberg (2004)
Oracle Corporation. GlassFish Application Server, https://glassfish.java.net/
Simonsen, K.I.F., Kristensen, L.M., Kindler, E.: Generating Protocol Software from CPN Models Annotated with Pragmatics. In: Iyoda, J., de Moura, L. (eds.) SBMF 2013. LNCS, vol. 8195, pp. 227–242. Springer, Heidelberg (2013)
Simonsen, K.I.F.: An Evaluation of Automated Code Generation with the PetriCode Approach. Submitted to: PNSE 2014 (2014)
Simonsen, K.I.F.: PetriCode: A Tool for Template-Based Code Generation from CPN Models. In: Counsell, S., Núñez, M. (eds.) SEFM 2013. LNCS, vol. 8368, pp. 151–163. Springer, Heidelberg (2014)
Tavendo GmbH. Autobahn|Testsuite, http://autobahn.ws/testsuite/
Tolvanen, J.-P.: Metaedit+: domain-specific modeling for full code generation demonstrated. In: Proc. of OOPSLA 2004, pp. 39–40. ACM (2004)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Simonsen, K.I.F., Kristensen, L.M. (2014). Implementing the WebSocket Protocol Based on Formal Modelling and Automated Code Generation. In: Magoutis, K., Pietzuch, P. (eds) Distributed Applications and Interoperable Systems. DAIS 2014. Lecture Notes in Computer Science(), vol 8460. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-43352-2_9
Download citation
DOI: https://doi.org/10.1007/978-3-662-43352-2_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-43351-5
Online ISBN: 978-3-662-43352-2
eBook Packages: Computer ScienceComputer Science (R0)