Lange, Julien, Yoshida, Nobuko (2019) Verifying Asynchronous Interactions via Communicating Session Automata. In: 31st International Conference on Computer-Aided Verification (CAV 2019). Lecture Notes in Computer Science (11561). pp. 97-117. Springer ISBN 978-3-030-25539-8. E-ISBN 978-3-030-25540-4. (doi:10.1007/978-3-030-25540-4_6) (KAR id:74012)
PDF
Supplemental Material
Language: English Restricted to Repository staff only |
|
Contact us about this Publication
|
![]() |
PDF
Author's Accepted Manuscript
Language: English
This work is licensed under a Creative Commons Attribution 4.0 International License.
|
|
Download this file (PDF/797kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
Official URL: https://link.springer.com/chapter/10.1007/978-3-03... |
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 performance empirically over large systems using partial order reduction.
Item Type: | Conference or workshop item (Paper) |
---|---|
DOI/Identification number: | 10.1007/978-3-030-25540-4_6 |
Uncontrolled keywords: | verification, message passing concurrency, asynchrony, communicating automata, session types |
Subjects: | Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming, |
Divisions: | Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing |
Depositing User: | Julien Lange |
Date Deposited: | 21 May 2019 11:01 UTC |
Last Modified: | 04 Mar 2024 15:16 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/74012 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):