Web Services and Formal Methods - 10th International Workshop, WS-FM 2013, Beijing, China, August 2013, Revised Selected Papers
Web Services and Formal Methods - 10th International Workshop, WS-FM 2013, Beijing, China, August 2013, Revised Selected Papers
复制标题
Web 服务和形式化方法 - 第 10 届国际研讨会，WS-FM 2013，中国北京，2013 年 8 月，修订后的精选论文
DOI：
10.1007/978-3-319-08260-8_3
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Bocchi L
中科院分区：
文献类型：
--
作者：
Bocchi L
在云基础设施上管理数据对现有的和经过充分研究的方法（如ACID和长时间运行的事务）提出了新的挑战。主要需求之一是在具有副本和分布式控制的场景中提供可用性和分区容错。这是以较弱的一致性为代价的，通常称为最终一致性。这些弱内存模型已被证明适用于许多场景，例如使用map reduce分析大型数据。然而，由于云基础设施的广泛可用性，弱存储不仅被专用应用程序使用，而且被通用应用程序使用。我们提供了一个正式的方法，基于进程演算，原因依赖于云存储的程序的行为。例如，它允许检查具有云存储的流程的组合通过明智地使用异步消息传递来确保“强”属性;在这种情况下，我们说该流程支持云存储提供的一致性级别。所提出的方法是组合的：支持的一致性水平被保存的并行组合时，用于比较进程存储合奏的前序是弱模拟。
Managing data over cloud infrastructures raises novel challenges with respect to existing and well-studied approaches such as ACID and long-running transactions. One of the main requirements is to provide availability and partition tolerance in a scenario with replicas and distributed control. This comes at the price of a weaker consistency, usually called eventual consistency. These weak memory models have proved to be suitable in a number of scenarios, such as the analysis of large data with map reduce. However, due to the widespread availability of cloud infrastructures, weak storages are used not only by specialised applications but also by general purpose applications. We provide a formal approach, based on process calculi, to reason about the behaviour of programs that rely on cloud stores. For instance, it allows to check that the composition of a process with a cloud store ensures ‘strong’ properties through a wise usage of asynchronous message-passing; in this case, we say that the process supports the consistency level provided by the cloud store. The proposed approach is compositional: the support of a consistency level is preserved by parallel composition when the preorder used to compare process-store ensembles is the weak simulation.