Verifying asynchronous interactions via communicating session automata
File(s)2019_Chapter_.pdf (814.56 KB)
Published version
Author(s)
Lange, Julien
Yoshida, Nobuko
Type
Conference Paper
Abstract
This paper proposes a sound procedure to verify properties of communicating session automata (csa), i.e., communicating automata that include multiparty session types. We introduce a new asynchronous compatibility property for csa, called k-multiparty compatibility (k-mc), which is a strict superset of the synchronous multiparty compatibility used in theories and tools based on session types. It is decomposed into two bounded properties: (i) a condition called k-safety which guarantees that, within the bound, all sent messages can be received and each automaton can make a move; and (ii) a condition called k-exhaustivity which guarantees that all k-reachable send actions can be fired within the bound. We show that k-exhaustivity implies existential boundedness, and soundly and completely characterises systems where each automaton behaves equivalently under bounds greater than or equal to k. We show that checking k-mc is pspace-complete, and demonstrate its scalability empirically over large systems (using partial order reduction).
Editor(s)
Dillig, I
Tasiran, S
Date Issued
2019-07-12
Date Acceptance
2019-07-01
Citation
Computer Aided Verification Proceedings, Part I, 2019, 11561, pp.97-117
ISBN
978-3-030-25539-8
ISSN
0302-9743
Publisher
SPRINGER INTERNATIONAL PUBLISHING AG
Start Page
97
End Page
117
Journal / Book Title
Computer Aided Verification Proceedings, Part I
Volume
11561
Copyright Statement
© The Author(s) 2019. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Identifier
http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000491468000006&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=1ba7043ffcc86c417c072aa74d649202
Source
31st International Conference on Computer-Aided Verification (CAV)
Subjects
Science & Technology
Technology
Computer Science, Software Engineering
Computer Science, Theory & Methods
Computer Science
VERIFICATION
Publication Status
Published
Start Date
2019-07-15
Finish Date
2019-07-18
Coverage Spatial
New York, NY
Date Publish Online
2019-07-12