Verifying asynchronous interactions via communicating session automata

DOI10.1007/978-3-030-25540-4_6MaRDI QIDQ6154577zbMATH OpenOpenAlexFDO

Authors Julien Lange, Nobuko Yoshida

Publication date 16 February 2024

Published in Computer Aided Verification (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/1901.09606

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Multiparty session types meet communicating automata
• Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
• Taming concurrency for verification using multiparty session types
• Automated verification of automata communicating via FIFO and bag buffers
• Multiparty asynchronous session types

Cited in

(5)

• Communicating finite state machines and an extensible toolchain for multiparty session types
• Session types without sophistry. System description
• Fair asynchronous session subtyping
• Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types
• Complete multiparty session type projection with automata

This page was built for publication: Verifying asynchronous interactions via communicating session automata

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6154577)