Monitoring networks through multiparty session types
Monitoring networks through multiparty session types
复制标题
DOI：
10.1016/j.tcs.2017.02.009
复制
发表时间：
2017-03-22
影响因子：
1.1
通讯作者：
Yoshida, Nobuko
中科院分区：
文献类型：
--
作者：
Bocchi, Laura;Chen, Tzu-Chun;Yoshida, Nobuko
在大规模的分布式基础架构中，应用程序是通过分布式组件之间的通信实现的。认识到在这种环境中确保安全互动的方法的需求已被认识到，但是依靠集中验证或限制规范方法的现有框架的适用性有限。本文提出了一种新的对PI-CALCULUS的监测理论，该理论具有多律会类型（MPST）的动态使用，为分布式组件的安全保证提供了严格的基础，通过多方会话对分布式组件进行安全性。我们的理论为语义上精确的分散运行时间执行建立了一个框架，并提供了对被监视的分布式应用程序的推理原则，这些应用程序补充了现有的静态分析技术。我们通过明确的路由器和全局队列的方式介绍异步，并提出了网络之间的新颖等价，以捕获接口等价的概念，即等同于向用户提供相同服务的网络等同。我们以ATM协议作为运行的示例来说明我们的静态动力分析系统，并以结果证明我们的理论是合理的：满意度等效性，本地/全球安全性和透明度以及会话保真度。 （c）2017年作者。 Elsevier B.V.发表的这是CC根据许可证的开放访问文章
In large-scale distributed infrastructures, applications are realised through communications among distributed components. The need for methods for assuring safe interactions in such environments is recognised, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory of monitored pi-calculus with dynamic usage of multiparty session types (MPST), offering a rigorous foundation for safety assurance of distributed components which asynchronously communicate through multiparty sessions. Our theory establishes a framework for semantically precise decentralised run-time enforcement and provides reasoning principles over monitored distributed applications, which complement existing static analysis techniques. We introduce asynchrony through the means of explicit routers and global queues, and propose novel equivalences between networks, that capture the notion of interface equivalence, i.e. equating networks offering the same services to a user. We illustrate our static-dynamic analysis system with an ATM protocol as a running example and justify our theory with results: satisfaction equivalence, local/global safety and transparency, and session fidelity. (C) 2017 The Author(s). Published by Elsevier B.V. This is an open access article under the CC BY license