...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>International journal of parallel programming >Bringing Coq into the World of GCM Distributed Applications
【24h】

Bringing Coq into the World of GCM Distributed Applications

机译：将Coq带入GCM分布式应用程序世界

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

摘要

Among all programming paradigms, component-based engineering stands as one of the most followed approaches for real world software development. Its emphasis on clean separation of concerns and reusability makes it appealing for both industrial and research purposes. The Grid Component Model (GCM) endorses this approach in the context of distributed systems by providing all the means to define, compose and dynamically reconfigure component-based applications. While structural reconfiguration is one of the key features of GCM applications, this ability to evolve at runtime poses several challenges w.r.t reliability. In this paper we present Mefresa, a framework for reasoning on the structure of GCM applications. This contribution comes in the form of a formal specification mechanized in the Coq Proof Assistant. Our aim is to demonstrate the benefits of interactive theorem proving for the reasoning on software architectures. We provide a configuration and reconfiguration language for the safe instantiation of distributed systems.
机译：在所有编程范例中，基于组件的工程是现实世界中软件开发最受关注的方法之一。它强调关注点和可重用性的清晰分离，使其在工业和研究方面都具有吸引力。网格组件模型（GCM）通过提供定义，组成和动态重新配置基于组件的应用程序的所有方法，在分布式系统的上下文中认可了此方法。虽然结构重配置是GCM应用程序的关键功能之一，但这种在运行时不断发展的能力给可靠性带来了许多挑战。在本文中，我们介绍了Mefresa，这是对GCM应用程序结构进行推理的框架。该贡献以Coq证明助手中机械化的正式规范的形式出现。我们的目的是证明交互式定理证明对软件体系结构推理的好处。我们提供一种用于安全实例化分布式系统的配置和重新配置语言。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号