×

Timed multiparty session types. (English) Zbl 1417.68117

Baldan, Paolo (ed.) et al., CONCUR 2014 – concurrency theory. 25th international conference, CONCUR 2014, Rome, Italy, September 2–5, 2014. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 8704, 419-434 (2014).
Summary: 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.
For the entire collection see [Zbl 1295.68016].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDFBibTeX XMLCite
Full Text: DOI Link