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

Kent Inge Simonsen; Lars Michael Kristensen

doi:10.1007/978-3-642-38209-3_7

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

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

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 language	English
Title of host publication	Model-Based Methodologies for Pervasive and Embedded Software : 8th International Workshop, MOMPES 2012, Essen, Germany, September 4, 2012. Revised Papers
Publisher	Springer
Publication date	2013
Pages	106-125
ISBN (Print)	978-3-642-38208-6
ISBN (Electronic)	978-3-642-38209-3
DOIs	https://doi.org/10.1007/978-3-642-38209-3_7
Publication status	Published - 2013
Event	8th International Workshop on Model-based Methodologies for Pervasive and Embedded Software (MOMPES 2012) - Essen, Germany Duration: 4 Sept 2012 → … http://www3.di.uminho.pt/mompes/2012/

Workshop

Workshop	8th International Workshop on Model-based Methodologies for Pervasive and Embedded Software (MOMPES 2012)
Country/Territory	Germany
City	Essen
Period	04/09/2012 → …
Internet address	http://www3.di.uminho.pt/mompes/2012/

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

Keywords

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

Access to Document

10.1007/978-3-642-38209-3_7

OpenUrl availability

Full text

Cite this

Simonsen, K. I., & Kristensen, L. M. (2013). Towards a CPN-Based Modelling Approach for Reconciling Verification and Implementation of Protocol Models. In Model-Based Methodologies for Pervasive and Embedded Software: 8th International Workshop, MOMPES 2012, Essen, Germany, September 4, 2012. Revised Papers (pp. 106-125). Springer. https://doi.org/10.1007/978-3-642-38209-3_7

Simonsen, Kent Inge ; Kristensen, Lars Michael. / Towards a CPN-Based Modelling Approach for Reconciling Verification and Implementation of Protocol Models. Model-Based Methodologies for Pervasive and Embedded Software: 8th International Workshop, MOMPES 2012, Essen, Germany, September 4, 2012. Revised Papers. Springer, 2013. pp. 106-125 (Lecture Notes in Computer Science, Vol. 7706).

@inproceedings{2c96ddb6903f4283a1c6ea3746fb2ab9,

title = "Towards a CPN-Based Modelling Approach for Reconciling Verification and Implementation of Protocol Models",

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

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

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

year = "2013",

doi = "10.1007/978-3-642-38209-3_7",

language = "English",

isbn = "978-3-642-38208-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "106--125",

booktitle = "Model-Based Methodologies for Pervasive and Embedded Software",

note = "8th International Workshop on Model-based Methodologies for Pervasive and Embedded Software (MOMPES 2012) ; Conference date: 04-09-2012",

url = "http://www3.di.uminho.pt/mompes/2012/",

}

Simonsen, KI & Kristensen, LM 2013, Towards a CPN-Based Modelling Approach for Reconciling Verification and Implementation of Protocol Models. in Model-Based Methodologies for Pervasive and Embedded Software: 8th International Workshop, MOMPES 2012, Essen, Germany, September 4, 2012. Revised Papers. Springer, Lecture Notes in Computer Science, vol. 7706, pp. 106-125, 8th International Workshop on Model-based Methodologies for Pervasive and Embedded Software (MOMPES 2012), Essen, Germany, 04/09/2012. https://doi.org/10.1007/978-3-642-38209-3_7

Towards a CPN-Based Modelling Approach for Reconciling Verification and Implementation of Protocol Models. / Simonsen, Kent Inge; Kristensen, Lars Michael.
Model-Based Methodologies for Pervasive and Embedded Software: 8th International Workshop, MOMPES 2012, Essen, Germany, September 4, 2012. Revised Papers. Springer, 2013. p. 106-125 (Lecture Notes in Computer Science, Vol. 7706).

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

TY - GEN

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

AU - Simonsen, Kent Inge

AU - Kristensen, Lars Michael

PY - 2013

Y1 - 2013

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

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

KW - Protocol software for pervavise computing

KW - Model-based protocol development

KW - Protocol verification

KW - Coloured Petri Nets

U2 - 10.1007/978-3-642-38209-3_7

DO - 10.1007/978-3-642-38209-3_7

M3 - Article in proceedings

SN - 978-3-642-38208-6

T3 - Lecture Notes in Computer Science

SP - 106

EP - 125

BT - Model-Based Methodologies for Pervasive and Embedded Software

PB - Springer

T2 - 8th International Workshop on Model-based Methodologies for Pervasive and Embedded Software (MOMPES 2012)

Y2 - 4 September 2012

ER -

Simonsen KI, Kristensen LM. Towards a CPN-Based Modelling Approach for Reconciling Verification and Implementation of Protocol Models. In Model-Based Methodologies for Pervasive and Embedded Software: 8th International Workshop, MOMPES 2012, Essen, Germany, September 4, 2012. Revised Papers. Springer. 2013. p. 106-125. (Lecture Notes in Computer Science, Vol. 7706). doi: 10.1007/978-3-642-38209-3_7

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

Abstract

Workshop

Keywords

Access to Document

OpenUrl availability

Fingerprint

Cite this