Formal Techniques for Distributed Systems
Formal Techniques for Distributed Systems
复制标题
分布式系统的形式化技术
DOI：
10.1007/978-3-642-38592-6_5
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Bocchi L
中科院分区：
文献类型：
--
作者：
Bocchi L
在大规模分布式基础设施中，应用程序是通过分布式组件之间的通信来实现的。人们认识到需要确保此类环境中安全交互的方法，但依赖于集中验证或限制规范方法的现有框架的适用性有限。本文提出了一种新的动态使用多方会话类型的监控π演算理论（MPST），为通过多方会话异步通信的分布式组件的安全保证提供了严格的基础。我们的理论建立了一个框架，语义精确的分散运行时执法，并提供了推理原则，监控分布式应用程序，补充现有的静态分析技术。我们通过显式路由器和全局队列的方式引入了网络等价，并提出了网络之间的新等价，它捕获了接口等价的概念，即等同于为用户提供相同服务的网络。我们说明了我们的静态-动态分析系统与ATM协议作为一个运行的例子，证明我们的理论与结果：满意度等价，本地/全球的安全性和透明度，和会话保真度。
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 recognized, however the existing frameworks, relying on centralised verification or restricted specification methods, have limited applicability. This paper proposes a new theory ofmonitoredπ-calculus with dynamic usage ofmultiparty 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.