In the last decade, the web infrastructure has evolved to support on-the-fly access of services provided by different vendors. Potentially, this enables collaborations that are cross-boundary and obey precise non-trivial patterns of conversation. However, today services are still used separately, with little integration and guarantees of safety and quality of service.
To enable the digital economy to concretely benefit from service integration and open collaborations among several parties, it is critical to ensure safety guarantees (e.g., deadlock freedom) that encompass whole systems, and not just single services. Moreover, as services are developed separately and composed on-the-fly, verification should be modular. Modularity is supported by existing frameworks based on multiparty session types (MPST), which allow effective static (behavioural) local type-checking of programs against global protocol specifications involving several parties.
Unfortunately, the state of the art on session types does not sufficiently address non-functional aspects of program correctness. A quality-aware approach to process engineering is particularly critical, as quality properties may affect the functional behaviour of the overall system. For example, the response time of a remote database may affect the deadlock freedom of complex interactions with several clients. This project will focus on time, which is at the basis of many critical safety and quality properties, as many non-trivial collaborations rely on some notion of deadline or timeout (e.g., the Twitter Streaming API requires clients to "...reconnect no more than twice every four minutes").
The aim of the project is to provide a framework for engineering time-sensitive distributed protocols. Protocols are intended here as ad-hoc, application level, abstract specifications of the interaction patterns that actual distributed implementations should follow. Some examples of protocol are the Post Office Protocol (POP2) or Map-Reduce.
The framework we propose will be practical, formally grounded, and support: specification of time-sensitive protocols, their modular implementation as executable programs, and modular automated verification of programs against protocols via type-checking. We will provide two languages, one for the specification and one for the implementation of time-sensitive protocols, and establish their relationship in terms of a verification (i.e., behavioural type-checking) framework based on MPST.
Modularity and formality will derive from using MPST. Three open challenges will be addressed, which are critical for the practical applicability of MPST to timed session programming: expressiveness, tractability, and embedding into concrete languages and tools.
By expressiveness we mean the ability of the programming primitives to set flexible schedules for the timing of actions and support run-time adjustments (e.g., depending on the actual timing in which actions are executed, or on the run-time system load). This will yield robustness of the overall approach by enabling programs to adapt to unpredicted run-time delays.
When verifying programs with such flexible time schedules, tractability will be ensured by combining static and dynamic verification (i.e., via hybrid typing). Hybrid typing of timed interactions is still an unexplored direction, but a promising one in terms of efficiency of verification and robustness.
Finally, the programming primitives for timed session programming will be embedded into a mainstream programming language that can be directly used by practitioners. Concretely, we will provide a Java API for time-aware session programming and a hybrid type-checking tool for programs written with this API. This will enable timely assessment of the theory, wide access to the project's results from academics and practitioners, and support impact.
|