Compositional Verification of Asynchonously Communicating Systems

Jan Martijn van der Werf

doi:10.1007/978-3-319-15317-9_4

Compositional Verification of Asynchonously Communicating Systems

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Abstract

Within a network of asynchronously communicating systems, the complete network is often not known, or even available at run-time. Consequently, verifying whether the network of communicating systems behaves correctly, i.e., the network does not contain any deadlock or livelock, is impracticable. As such systems are highly concurrent by nature, Petri nets form a natural choice to model these systems and their communication.
This paper presents a formal framework based on a generic communication condition to verify correctness of the system by pairwise checking whether these systems communicate correctly and fulfill some condition, then the whole network is guaranteed to behave correctly. As an example, this paper presents the elastic communication condition.

Original language	English
Title of host publication	Formal Aspects of Component Software
Subtitle of host publication	11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers
Editors	Ivan Lanese, Eric Madelaine
Place of Publication	Cham
Publisher	Springer
Pages	49-67
Edition	1
ISBN (Electronic)	978-3-319-15317-9
ISBN (Print)	978-3-319-15316-2
DOIs	https://doi.org/10.1007/978-3-319-15317-9_4
Publication status	Published - 18 Feb 2015

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	8997
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Access to Document

10.1007/978-3-319-15317-9_4

4Final published version, 516 KBLicence: Taverne

Cite this

van der Werf, J. M. (2015). Compositional Verification of Asynchonously Communicating Systems. In I. Lanese, & E. Madelaine (Eds.), Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers (1 ed., pp. 49-67). (Lecture Notes in Computer Science; Vol. 8997). Springer. https://doi.org/10.1007/978-3-319-15317-9_4

@inproceedings{03a50a0a89f44c0aad7f047b2d812950,

title = "Compositional Verification of Asynchonously Communicating Systems",

abstract = "Within a network of asynchronously communicating systems, the complete network is often not known, or even available at run-time. Consequently, verifying whether the network of communicating systems behaves correctly, i.e., the network does not contain any deadlock or livelock, is impracticable. As such systems are highly concurrent by nature, Petri nets form a natural choice to model these systems and their communication. This paper presents a formal framework based on a generic communication condition to verify correctness of the system by pairwise checking whether these systems communicate correctly and fulfill some condition, then the whole network is guaranteed to behave correctly. As an example, this paper presents the elastic communication condition.",

author = "{van der Werf}, {Jan Martijn}",

year = "2015",

month = feb,

day = "18",

doi = "10.1007/978-3-319-15317-9_4",

language = "English",

isbn = "978-3-319-15316-2",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "49--67",

editor = "Lanese, {Ivan } and Eric Madelaine",

booktitle = "Formal Aspects of Component Software",

edition = "1",

}

van der Werf, JM 2015, Compositional Verification of Asynchonously Communicating Systems. in I Lanese & E Madelaine (eds), Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers. 1 edn, Lecture Notes in Computer Science, vol. 8997, Springer, Cham, pp. 49-67. https://doi.org/10.1007/978-3-319-15317-9_4

Compositional Verification of Asynchonously Communicating Systems. / van der Werf, Jan Martijn.
Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers. ed. / Ivan Lanese; Eric Madelaine. 1. ed. Cham: Springer, 2015. p. 49-67 (Lecture Notes in Computer Science; Vol. 8997).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Compositional Verification of Asynchonously Communicating Systems

AU - van der Werf, Jan Martijn

PY - 2015/2/18

Y1 - 2015/2/18

N2 - Within a network of asynchronously communicating systems, the complete network is often not known, or even available at run-time. Consequently, verifying whether the network of communicating systems behaves correctly, i.e., the network does not contain any deadlock or livelock, is impracticable. As such systems are highly concurrent by nature, Petri nets form a natural choice to model these systems and their communication. This paper presents a formal framework based on a generic communication condition to verify correctness of the system by pairwise checking whether these systems communicate correctly and fulfill some condition, then the whole network is guaranteed to behave correctly. As an example, this paper presents the elastic communication condition.

AB - Within a network of asynchronously communicating systems, the complete network is often not known, or even available at run-time. Consequently, verifying whether the network of communicating systems behaves correctly, i.e., the network does not contain any deadlock or livelock, is impracticable. As such systems are highly concurrent by nature, Petri nets form a natural choice to model these systems and their communication. This paper presents a formal framework based on a generic communication condition to verify correctness of the system by pairwise checking whether these systems communicate correctly and fulfill some condition, then the whole network is guaranteed to behave correctly. As an example, this paper presents the elastic communication condition.

U2 - 10.1007/978-3-319-15317-9_4

DO - 10.1007/978-3-319-15317-9_4

M3 - Conference contribution

SN - 978-3-319-15316-2

T3 - Lecture Notes in Computer Science

SP - 49

EP - 67

BT - Formal Aspects of Component Software

A2 - Lanese, Ivan

A2 - Madelaine, Eric

PB - Springer

CY - Cham

ER -

van der Werf JM. Compositional Verification of Asynchonously Communicating Systems. In Lanese I, Madelaine E, editors, Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers. 1 ed. Cham: Springer. 2015. p. 49-67. (Lecture Notes in Computer Science). doi: 10.1007/978-3-319-15317-9_4

Compositional Verification of Asynchonously Communicating Systems

Abstract

Publication series

Access to Document

Fingerprint

Cite this