@article {RN54,
	title = {Practical interruptible conversations: distributed dynamic verification with multiparty session types and Python},
	journal = {Formal Methods in System Design},
	volume = {46},
	number = {3},
	year = {2015},
	pages = {197-225},
	type = {Journal Article},
	abstract = {The rigorous and comprehensive verification of communication-based software is an important engineering challenge in distributed systems. Drawn from our industrial collaborations (Ocean Observatories Initative, http://www.oceanobservatories.org/, JBoss Savara Project, http://www.jboss.org/savara) on Scribble, a choreography description language based on multiparty session types, and its theoretical foundations (Honda et al., in POPL, pp 273{\textendash}284, 2008), this article proposes a dynamic verification framework for structured interruptible conversation programming. We first present our extension of Scribble to support the specification of asynchronously interruptible conversations. We then implement a concise API for conversation programming with interrupts in Python that enables session types properties to be dynamically verified for distributed processes. Finally, we expose the underlying theory of our interrupt mechanism, studying its syntax and semantics, its integration in MPST theory and proving the correctness of our design. Our framework ensures the global safety of a system in the presence of asynchronous interrupts through independent runtime monitoring of each endpoint, checking the conformance of the local execution trace to the specified protocol. The usability of our framework for describing and verifying choreographic communications has been tested by integration into the large scientific cyberinfrastructure developed by the Ocean Observatories Initiative. Asynchronous interrupts have proven expressive enough to represent and verify their main classes of communication patterns, including asynchronous streaming and various timeout-based protocols, without introducing any implicit synchronisations. Benchmarks show conversation programming and monitoring can be realised with little overhead.},
	keywords = {Distributed systems, Python, Runtime monitoring, Session types},
	issn = {0925-9856},
	doi = {10.1007/s10703-014-0218-8},
	url = {<Go to ISI>://WOS:000360940700001},
	author = {Demangeon, R. and Honda, K. and Hu, R. and Neykova, R. and Yoshida, N.}
}
@article {RN58,
	title = {Parameterised Multiparty Session Types},
	journal = {Logical Methods in Computer Science},
	volume = {8},
	number = {4},
	year = {2012},
	type = {Journal Article},
	abstract = {For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from G{\"o}del{\textquoteright}s System T to express a wide range of communication patterns while keeping type checking decidable. To type individual distributed processes, a parameterised global type is projected onto a generic generator which represents a class of all possible end-point types. We prove the termination of the type-checking algorithm in the full system with both multiparty session types and recursive types. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.

},
	keywords = {Computer Science, D.1.3, F.1.1, F.1.2, F.3.3, Logic in Computer Science},
	issn = {1860-5974},
	doi = {10.2168/Lmcs-8(4:6)2012},
	url = {<Go to ISI>://WOS:000315381600008},
	author = {Denielou, P. M. and Yoshida, N. and Bejleri, A. and Hu, R.}
}
