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 | |
Publication status | Published - 2013 |
Event | 8th 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
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 |
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