ON GLOBAL TYPES AND MULTI-PARTY SESSIONS

被引:55
作者
Castagna, Giuseppe [1 ]
Dezani-Ciancaglini, Mariangiola [2 ]
Padovani, Luca [2 ]
机构
[1] Univ Paris Diderot, CNRS, PPS, Paris, France
[2] Univ Turin, Dipartimento Informat, I-10149 Turin, Italy
关键词
Web services; concurrency theory; type theory; subtyping; global types; session types; VERIFICATION; PROGRESS;
D O I
10.2168/LMCS-8(1:24)2012
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
Global types are formal specifications that describe communication protocols in terms of their global interactions. We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and restrictions are semantically justified. The multi-party sessions obtained projecting our global types enjoy a liveness property in addition to the traditional progress and are shown to be sound and complete with respect to the set of traces of the originating global type. Our notion of completeness is less demanding than the classical ones, allowing a multi-party session to leave out redundant traces from an underspecified global type. In addition to the technical content, we discuss some limitations of our language of global types and provide an extensive comparison with related specification languages adopted in different communities.
引用
收藏
页数:45
相关论文
共 44 条
[1]   A calculus for cryptographic protocols: The spi calculus [J].
Abadi, M ;
Gordon, AD .
INFORMATION AND COMPUTATION, 1999, 148 (01) :1-70
[2]  
Alur R., 2000, Proceedings of the 2000 International Conference on Software Engineering. ICSE 2000 the New Millennium, P304, DOI 10.1109/ICSE.2000.870421
[3]  
Alur R, 2001, LECT NOTES COMPUT SC, V2076, P797
[4]  
Alur R, 1999, LECT NOTES COMPUT SC, V1664, P114
[5]  
[Anonymous], 2008, Lecture Notes in Computer Science, DOI DOI 10.1007/978-3-642-00945-7
[6]  
[Anonymous], 2011, P WWW 2011, DOI DOI 10.1145/1963405.1963516
[7]  
[Anonymous], 2005, Web Services Choreography Description Language (WS-CDL)
[8]  
Baldoni Matteo., 2009, Proceedings of the 8th International Conference on Autonomous Agents and MultiAgent Systems (AAMAS), P843, DOI [DOI 10.5555/1558109.1558129, DOI 10.1145/1558109.1558129]
[9]  
Bergstra Jan A., 1993, CSR9314 U AMST PROGR
[10]  
Bettini L, 2008, LECT NOTES COMPUT SC, V5201, P418, DOI 10.1007/978-3-540-85361-9_33