Verification of a dynamic channel model using the SPIN model checker

Rune Møllegaard Friborg; Brian Vinter

doi:10.3233/978-1-60750-774-1-35

Verification of a dynamic channel model using the SPIN model checker

Rune Møllegaard Friborg, Brian Vinter

eScience

Abstract

This paper presents the central elements of a new dynamic channel leading towards a flexible CSP design suited for high-level languages. This channel is separated into three models: a shared-memory channel, a distributed channel and a dynamic synchronisation layer. The models are described such that they may function as a basis for implementing a CSP library, though many of the common features known in available CSP libraries have been excluded from the models. The SPIN model checker has been used to check for the presence of deadlocks, livelocks, starvation, race conditions and correct channel communication behaviour. The three models are separately verified for a variety of different process configurations. This verification is performed automatically by doing an exhaustive verification of all possible transitions using SPIN. The joint result of the models is a single dynamic channel type which supports both local and distributed any-to-any communication. This model has not been verified and the large state-space may make it unsuited for exhaustive verification using a model checker. An implementation of the dynamic channel will be able to change the internal synchronisation mechanisms on-the-fly, depending on the number of channel-ends connected or their location.

Original language	English
Title of host publication	Communicating Process Architectures 2011 : Proceedings of the 33rd WoTUG Technical Meeting, 19–22 June 2011, University of Limerick, Ireland
Editors	Peter H. Welch, Adam T. Sampson, Jan Baekgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
Number of pages	20
Publisher	IOS Press
Publication date	2011
Pages	35-54
ISBN (Print)	978-1-60750-773-4
ISBN (Electronic)	978-1-60750-774-1
DOIs	https://doi.org/10.3233/978-1-60750-774-1-35
Publication status	Published - 2011
Event	33rd WoTUG Conference on Concurrent and Parallel Programming: communicating process architectures 2011 - University of Limerick, Limerick, Ireland Duration: 19 Jun 2011 → 22 Jun 2011 Conference number: 33

Conference

Conference	33rd WoTUG Conference on Concurrent and Parallel Programming
Number	33
Location	University of Limerick
Country/Territory	Ireland
City	Limerick
Period	19/06/2011 → 22/06/2011

Series	Concurrent Systems Engineering Series
Volume	68
ISSN	1383-7575

Access to Document

10.3233/978-1-60750-774-1-35

http://wotug.org/papers/CPA-2011/FriborgVinter11/FriborgVinter11.pdf

Cite this

Friborg, R. M., & Vinter, B. (2011). Verification of a dynamic channel model using the SPIN model checker. In P. H. Welch, A. T. Sampson, J. B. Pedersen, J. Kerridge, J. F. Broenink, & F. R. M. Barnes (Eds.), Communicating Process Architectures 2011: Proceedings of the 33rd WoTUG Technical Meeting, 19–22 June 2011, University of Limerick, Ireland (pp. 35-54). IOS Press. Concurrent Systems Engineering Series Vol. 68 https://doi.org/10.3233/978-1-60750-774-1-35

Verification of a dynamic channel model using the SPIN model checker. / Friborg, Rune Møllegaard; Vinter, Brian.

Communicating Process Architectures 2011: Proceedings of the 33rd WoTUG Technical Meeting, 19–22 June 2011, University of Limerick, Ireland. ed. / Peter H. Welch; Adam T. Sampson; Jan Baekgaard Pedersen; Jon Kerridge; Jan F. Broenink; Frederick R. M. Barnes. IOS Press, 2011. p. 35-54 (Concurrent Systems Engineering Series, Vol. 68).

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

Friborg, RM & Vinter, B 2011, Verification of a dynamic channel model using the SPIN model checker. in PH Welch, AT Sampson, JB Pedersen, J Kerridge, JF Broenink & FRM Barnes (eds), Communicating Process Architectures 2011: Proceedings of the 33rd WoTUG Technical Meeting, 19–22 June 2011, University of Limerick, Ireland. IOS Press, Concurrent Systems Engineering Series, vol. 68, pp. 35-54, 33rd WoTUG Conference on Concurrent and Parallel Programming, Limerick, Ireland, 19/06/2011. https://doi.org/10.3233/978-1-60750-774-1-35

Friborg RM, Vinter B. Verification of a dynamic channel model using the SPIN model checker. In Welch PH, Sampson AT, Pedersen JB, Kerridge J, Broenink JF, Barnes FRM, editors, Communicating Process Architectures 2011: Proceedings of the 33rd WoTUG Technical Meeting, 19–22 June 2011, University of Limerick, Ireland. IOS Press. 2011. p. 35-54. (Concurrent Systems Engineering Series, Vol. 68). doi: 10.3233/978-1-60750-774-1-35

Friborg, Rune Møllegaard ; Vinter, Brian. / Verification of a dynamic channel model using the SPIN model checker. Communicating Process Architectures 2011: Proceedings of the 33rd WoTUG Technical Meeting, 19–22 June 2011, University of Limerick, Ireland. editor / Peter H. Welch ; Adam T. Sampson ; Jan Baekgaard Pedersen ; Jon Kerridge ; Jan F. Broenink ; Frederick R. M. Barnes. IOS Press, 2011. pp. 35-54 (Concurrent Systems Engineering Series, Vol. 68).

@inproceedings{4fe4af0abc59436a9a575d7161944414,

title = "Verification of a dynamic channel model using the SPIN model checker",

abstract = "This paper presents the central elements of a new dynamic channel leading towards a flexible CSP design suited for high-level languages. This channel is separated into three models: a shared-memory channel, a distributed channel and a dynamic synchronisation layer. The models are described such that they may function as a basis for implementing a CSP library, though many of the common features known in available CSP libraries have been excluded from the models. The SPIN model checker has been used to check for the presence of deadlocks, livelocks, starvation, race conditions and correct channel communication behaviour. The three models are separately verified for a variety of different process configurations. This verification is performed automatically by doing an exhaustive verification of all possible transitions using SPIN. The joint result of the models is a single dynamic channel type which supports both local and distributed any-to-any communication. This model has not been verified and the large state-space may make it unsuited for exhaustive verification using a model checker. An implementation of the dynamic channel will be able to change the internal synchronisation mechanisms on-the-fly, depending on the number of channel-ends connected or their location.",

author = "Friborg, {Rune M{\o}llegaard} and Brian Vinter",

year = "2011",

doi = "10.3233/978-1-60750-774-1-35",

language = "English",

isbn = "978-1-60750-773-4",

series = "Concurrent Systems Engineering Series",

publisher = "IOS Press",

pages = "35--54",

editor = "Welch, {Peter H.} and Sampson, {Adam T.} and Pedersen, {Jan Baekgaard} and Jon Kerridge and Broenink, {Jan F.} and Barnes, {Frederick R. M.}",

booktitle = "Communicating Process Architectures 2011",

address = "United States",

note = "33rd WoTUG Conference on Concurrent and Parallel Programming : communicating process architectures 2011, WoTUG-33 ; Conference date: 19-06-2011 Through 22-06-2011",

}

TY - GEN

T1 - Verification of a dynamic channel model using the SPIN model checker

AU - Friborg, Rune Møllegaard

AU - Vinter, Brian

N1 - Conference code: 33

PY - 2011

Y1 - 2011

N2 - This paper presents the central elements of a new dynamic channel leading towards a flexible CSP design suited for high-level languages. This channel is separated into three models: a shared-memory channel, a distributed channel and a dynamic synchronisation layer. The models are described such that they may function as a basis for implementing a CSP library, though many of the common features known in available CSP libraries have been excluded from the models. The SPIN model checker has been used to check for the presence of deadlocks, livelocks, starvation, race conditions and correct channel communication behaviour. The three models are separately verified for a variety of different process configurations. This verification is performed automatically by doing an exhaustive verification of all possible transitions using SPIN. The joint result of the models is a single dynamic channel type which supports both local and distributed any-to-any communication. This model has not been verified and the large state-space may make it unsuited for exhaustive verification using a model checker. An implementation of the dynamic channel will be able to change the internal synchronisation mechanisms on-the-fly, depending on the number of channel-ends connected or their location.

AB - This paper presents the central elements of a new dynamic channel leading towards a flexible CSP design suited for high-level languages. This channel is separated into three models: a shared-memory channel, a distributed channel and a dynamic synchronisation layer. The models are described such that they may function as a basis for implementing a CSP library, though many of the common features known in available CSP libraries have been excluded from the models. The SPIN model checker has been used to check for the presence of deadlocks, livelocks, starvation, race conditions and correct channel communication behaviour. The three models are separately verified for a variety of different process configurations. This verification is performed automatically by doing an exhaustive verification of all possible transitions using SPIN. The joint result of the models is a single dynamic channel type which supports both local and distributed any-to-any communication. This model has not been verified and the large state-space may make it unsuited for exhaustive verification using a model checker. An implementation of the dynamic channel will be able to change the internal synchronisation mechanisms on-the-fly, depending on the number of channel-ends connected or their location.

U2 - 10.3233/978-1-60750-774-1-35

DO - 10.3233/978-1-60750-774-1-35

M3 - Article in proceedings

SN - 978-1-60750-773-4

T3 - Concurrent Systems Engineering Series

SP - 35

EP - 54

BT - Communicating Process Architectures 2011

A2 - Welch, Peter H.

A2 - Sampson, Adam T.

A2 - Pedersen, Jan Baekgaard

A2 - Kerridge, Jon

A2 - Broenink, Jan F.

A2 - Barnes, Frederick R. M.

PB - IOS Press

T2 - 33rd WoTUG Conference on Concurrent and Parallel Programming

Y2 - 19 June 2011 through 22 June 2011

ER -

Verification of a dynamic channel model using the SPIN model checker

Abstract

Conference

Access to Document

Fingerprint

Cite this