Imperial College London
Professor Nobuko Yoshida

ProfessorNobukoYoshida

Faculty of Engineering, Department of Computing

Academic Visitor
 
 
 
//

Contact

 

+44 (0)20 7594 8240n.yoshida Website

 
 
//

Location

 

556Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Lange:2019:10.1007/978-3-030-25540-4_6,
author = {Lange, J and Yoshida, N},
doi = {10.1007/978-3-030-25540-4_6},
pages = {97--117},
publisher = {SPRINGER INTERNATIONAL PUBLISHING AG},
title = {Verifying asynchronous interactions via communicating session automata},
url = {http://dx.doi.org/10.1007/978-3-030-25540-4_6},
year = {2019}
}
Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - 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).
AU  - Lange,J
AU  - Yoshida,N
DO  - 10.1007/978-3-030-25540-4_6
EP  - 117
PB  - SPRINGER INTERNATIONAL PUBLISHING AG
PY  - 2019///
SN  - 0302-9743
SP  - 97
TI  - Verifying asynchronous interactions via communicating session automata
UR  - http://dx.doi.org/10.1007/978-3-030-25540-4_6
UR  - http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000491468000006&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=1ba7043ffcc86c417c072aa74d649202
UR  - https://link.springer.com/chapter/10.1007%2F978-3-030-25540-4_6
UR  - http://hdl.handle.net/10044/1/75071
ER  -
Download