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.

Originalsprog	Engelsk
Titel	Communicating Process Architectures 2011 : Proceedings of the 33rd WoTUG Technical Meeting, 19–22 June 2011, University of Limerick, Ireland
Redaktører	Peter H. Welch, Adam T. Sampson, Jan Baekgaard Pedersen, Jon Kerridge, Jan F. Broenink, Frederick R. M. Barnes
Antal sider	20
Forlag	IOS Press
Publikationsdato	2011
Sider	35-54
ISBN (Trykt)	978-1-60750-773-4
ISBN (Elektronisk)	978-1-60750-774-1
DOI	https://doi.org/10.3233/978-1-60750-774-1-35
Status	Udgivet - 2011
Begivenhed	33rd WoTUG Conference on Concurrent and Parallel Programming: communicating process architectures 2011 - University of Limerick, Limerick, Irland Varighed: 19 jun. 2011 → 22 jun. 2011 Konferencens nummer: 33

Konference

Konference	33rd WoTUG Conference on Concurrent and Parallel Programming
Nummer	33
Lokation	University of Limerick
Land/Område	Irland
By	Limerick
Periode	19/06/2011 → 22/06/2011

Navn	Concurrent Systems Engineering Series
Vol/bind	68
ISSN	1383-7575

Adgang til dokumentet

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

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

Citationsformater

Friborg, R. M., & Vinter, B. (2011). Verification of a dynamic channel model using the SPIN model checker. I P. H. Welch, A. T. Sampson, J. B. Pedersen, J. Kerridge, J. F. Broenink, & F. R. M. Barnes (red.), Communicating Process Architectures 2011: Proceedings of the 33rd WoTUG Technical Meeting, 19–22 June 2011, University of Limerick, Ireland (s. 35-54). IOS Press. Concurrent Systems Engineering Series Bind 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. red. / Peter H. Welch; Adam T. Sampson; Jan Baekgaard Pedersen; Jon Kerridge; Jan F. Broenink; Frederick R. M. Barnes. IOS Press, 2011. s. 35-54 (Concurrent Systems Engineering Series, Bind 68).

Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › peer review

Friborg, RM & Vinter, B 2011, Verification of a dynamic channel model using the SPIN model checker. i PH Welch, AT Sampson, JB Pedersen, J Kerridge, JF Broenink & FRM Barnes (red), 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, bind 68, s. 35-54, 33rd WoTUG Conference on Concurrent and Parallel Programming, Limerick, Irland, 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. I Welch PH, Sampson AT, Pedersen JB, Kerridge J, Broenink JF, Barnes FRM, red., Communicating Process Architectures 2011: Proceedings of the 33rd WoTUG Technical Meeting, 19–22 June 2011, University of Limerick, Ireland. IOS Press. 2011. s. 35-54. (Concurrent Systems Engineering Series, Bind 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. red. / Peter H. Welch ; Adam T. Sampson ; Jan Baekgaard Pedersen ; Jon Kerridge ; Jan F. Broenink ; Frederick R. M. Barnes. IOS Press, 2011. s. 35-54 (Concurrent Systems Engineering Series, Bind 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

Konference

Adgang til dokumentet

Fingeraftryk

Citationsformater