\input zb-basic
\input zb-ioport
\iteman{io-port 06096953}
\itemau{Lozes, \'Etienne; Villard, Jules}
\itemti{Reliable contracts for unreliable half-duplex communications.}
\itemso{Carbone, Marco (ed.) et al., Web services and formal methods. 8th international workshop, WS-FM 2011, Clermont-Ferrand, France, September 1--2, 2011. Revised selected papers. Berlin: Springer (ISBN 978-3-642-29833-2/pbk). Lecture Notes in Computer Science 7176, 2-16 (2012).}
\itemab
Summary: Recent trends in formal models of web services description languages and session types focus on the asynchronicity of communications. In this paper, we study a core of these models that arose from our modelling of the Sing\# programming language, and demonstrate correspondences between Sing\# contracts, asynchronous session behaviors, and the subclass of communicating automata with two participants that satisfy the half-duplex property. This correspondence better explains the criteria proposed by Stengel and Bultan for Sing\# contracts to be reliable, and possibly indicate useful criteria for the design of WSDL. We moreover establish a polynomial-time complexity for the analysis of communication contracts under arbitrary models of asynchronicity, and we investigate the model-checking problems against LTL formulas.
\itemrv{~}
\itemcc{}
\itemut{}
\itemli{doi:10.1007/978-3-642-29834-9\_2}
\end