• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Software engineering and formal methods >Towards a Proof Framework for Information Systems with Weak Consistency
【24h】

Towards a Proof Framework for Information Systems with Weak Consistency

机译：建立具有弱一致性的信息系统的证明框架

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Weakly consistent data stores are more scalable and can provide a higher availability than classical, strongly consistent data stores. However, it is much harder to reason about and to implement applications, when the underlying infrastructure provides only few guarantees. In this paper, we report on work in progress on a proof framework, which can be used to formally reason about the correctness of such applications. The framework supports the verification of functional properties, which go beyond the guarantees given by the data store and can cover relations between multiple interactions with clients and invariants between several objects. Additionally, we modeled and support modern database features, like causal consistency, snapshot-transactions, and conflict-free replicated data types (CRDTs). The framework and the proofs are developed within the interactive theorem prover Isabelle/HOL.
机译：弱一致性数据存储区比传统的强一致性数据存储区更具伸缩性，并且可以提供更高的可用性。但是，当基础结构仅提供很少的保证时，就很难推理和实施应用程序。在本文中，我们报告了在证明框架上正在进行的工作，该框架可用于正式推理此类应用程序的正确性。该框架支持功能属性的验证，这超出了数据存储所提供的保证，并且可以涵盖与客户端的多次交互之间以及多个对象之间的不变量之间的关系。此外，我们建模并支持现代数据库功能，例如因果一致性，快照事务和无冲突的复制数据类型（CRDT）。该框架和证明是在交互式定理证明者Isabelle / HOL中开发的。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号