Towards a CPN-Based Modelling Approach for Reconciling Verification and Implementation of Protocol Models

Kent Inge Simonsen, Lars Michael Kristensen

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

Abstract

Formal modelling of protocols is often aimed at one specific purpose such as verification or automatically generating an implementation. This leads to models that are useful for one purpose, but not for others. Being able to derive models for verification and implementation from a single model is beneficial both in terms of reduced total modelling effort and confidence that the verification results are valid also for the implementation model. In this paper we introduce the concept of a descriptive specification model and an approach based on refining a descriptive model to target both verification and implementation. Our approach has been developed in the context of the Coloured Petri Nets (CPNs) modelling language. We illustrate our approach by presenting a descriptive specification model of the Websocket protocol which is currently under development by the Internet Engineering Task Force (IETF), and we show how this model can be refined to target both verification and implementation.
Original languageEnglish
Title of host publicationModel-Based Methodologies for Pervasive and Embedded Software : 8th International Workshop, MOMPES 2012, Essen, Germany, September 4, 2012. Revised Papers
PublisherSpringer
Publication date2013
Pages106-125
ISBN (Print)978-3-642-38208-6
ISBN (Electronic)978-3-642-38209-3
DOIs
Publication statusPublished - 2013
Event8th International Workshop on Model-based Methodologies for Pervasive and Embedded Software (MOMPES 2012) - Essen, Germany
Duration: 4 Sep 2012 → …
http://www3.di.uminho.pt/mompes/2012/

Workshop

Workshop8th International Workshop on Model-based Methodologies for Pervasive and Embedded Software (MOMPES 2012)
Country/TerritoryGermany
CityEssen
Period04/09/2012 → …
Internet address
SeriesLecture Notes in Computer Science
Volume7706
ISSN0302-9743

Keywords

  • Protocol software for pervavise computing
  • Model-based protocol development
  • Protocol verification
  • Coloured Petri Nets

Fingerprint

Dive into the research topics of 'Towards a CPN-Based Modelling Approach for Reconciling Verification and Implementation of Protocol Models'. Together they form a unique fingerprint.

Cite this