We propose a typing theory, based on multiparty session types, for modular verification of real-time choreographic interactions. To model real-time implementations, we introduce a simple calculus with delays and a decidable static proof system. The proof system ensures type safety and time-error freedom, namely processes respect the prescribed timing and causalities between interactions. A decidable condition on timed global types guarantees time-progress for validated processes with delays, and gives a sound and complete characterisation of a new class of CTAs with general topologies that enjoys progress and liveness. © 2014 Springer-Verlag.
CITATION STYLE
Bocchi, L., Yang, W., & Yoshida, N. (2014). Timed multiparty session types. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8704 LNCS, pp. 419–434). Springer Verlag. https://doi.org/10.1007/978-3-662-44584-6_29
Mendeley helps you to discover research relevant for your work.