Time-sensitive protocol design and implementation

在过去的十年中，Web基础设施已经发展为支持对不同供应商提供的服务的即时访问。潜在地，这使得跨国界的合作成为可能，并遵循精确的、非琐碎的对话模式。然而，今天的服务仍然是分开使用的，几乎没有整合，也没有对安全和服务质量的保证。为了使数字经济能够从服务集成和多方开放协作中具体受益，关键是确保涵盖整个系统的安全保障(例如，死锁自由)，而不仅仅是单一的服务。此外，由于服务是单独开发的，并且是动态组合的，因此验证应该是模块化的。模块化得到了基于多方会话类型(MPST)的现有框架的支持，该框架允许根据涉及多方的全局协议规范对程序进行有效的静态(行为)本地类型检查。不幸的是，有关会话类型的最新技术不足以解决程序正确性的非功能方面。过程工程的质量意识方法尤其关键，因为质量属性可能会影响整个系统的功能行为。例如，远程数据库的响应时间可能会影响与多个客户端进行复杂交互的死锁自由度。这个项目将重点关注时间，这是基于许多关键的安全和质量属性，因为许多重要的协作依赖于某些截止日期或超时的概念(例如，Twitter流媒体API要求客户端“...每四分钟重新连接不超过两次”)。该项目的目的是为设计时间敏感的分布式协议提供一个框架。协议在这里旨在作为实际分布式实现应该遵循的交互模式的临时、应用程序级别的抽象规范。协议的一些例子是邮局协议(POP2)或映射简化。我们提出的框架将是实用的、正式的基础和支持：时间敏感协议的规范，它们作为可执行程序的模块化实现，以及通过类型检查针对协议的模块化自动程序验证。我们将提供两种语言，一种用于规范，另一种用于时间敏感协议的实现，并根据基于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.