Time-sensitive protocol design and implementation

在过去的十年中，web基础设施已经发展到支持不同供应商提供的服务的动态访问。潜在地，这使得跨界协作成为可能，并且遵循精确的非琐碎的对话模式。然而，今天的服务仍然是单独使用的，几乎没有集成，也没有安全与服务质量的保证。为了使数字经济能够从服务集成和多方开放合作中具体受益，确保包含整个系统而不仅仅是单个服务的安全保障（例如，死锁自由）至关重要。此外，由于服务是单独开发和动态组合的，因此验证应该是模块化的。基于多方会话类型（MPST）的现有框架支持模块化，它允许针对涉及多方的全局协议规范对程序进行有效的静态（行为）本地类型检查。不幸的是，会话类型的最新技术并没有充分解决程序正确性的非功能方面的问题。过程工程的质量意识方法尤其重要，因为质量属性可能影响整个系统的功能行为。例如，远程数据库的响应时间可能会影响与多个客户机的复杂交互的死锁自由。这个项目将专注于时间，这是许多关键安全和质量属性的基础，因为许多重要的协作依赖于一些截止日期或超时的概念(例如，Twitter流媒体API要求客户端“……每四分钟重新连接不超过两次”)。该项目的目的是为工程时间敏感的分布式协议提供一个框架。这里的协议是作为实际分布式实现应该遵循的交互模式的特别的、应用程序级别的抽象规范。协议的一些例子是邮局协议（POP2）或Map-Reduce。我们提出的框架将是实用的，正式的基础，并支持：时间敏感协议的规范，它们作为可执行程序的模块化实现，以及通过类型检查对协议进行程序的模块化自动验证。我们将提供两种语言，一种用于规范，另一种用于实现时间敏感协议，并根据基于MPST的验证（即行为类型检查）框架建立它们之间的关系。模块化和形式化将来自于使用MPST。将解决三个开放的挑战，这对于MPST在定时会话编程中的实际应用至关重要：表达性、可追溯性和嵌入到具体的语言和工具中。通过表达性，我们指的是编程原语为操作的时间设置灵活的计划和支持运行时调整的能力（例如，取决于操作执行的实际时间，或运行时系统负载）。这将使程序能够适应不可预测的运行时延迟，从而产生整体方法的健壮性。当用这种灵活的时间安排验证程序时，将通过结合静态和动态验证（即，通过混合类型）来确保可追溯性。时间相互作用的混合类型仍然是一个未开发的方向，但在验证效率和鲁棒性方面是一个有希望的方向。最后，定时会话编程的编程原语将被嵌入到一种主流编程语言中，供从业者直接使用。具体来说，我们将为时间感知会话编程提供一个Java API，并为使用该API编写的程序提供一个混合类型检查工具。这将有助于及时评估理论，从学术界和实践者那里广泛获取项目成果，并支持影响。

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.