• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Software engineering and formal methods >CoCoSpec: A Mode-Aware Contract Language for Reactive Systems
【24h】

CoCoSpec: A Mode-Aware Contract Language for Reactive Systems

机译：CoCoSpec：一种用于反应式系统的模式感知合同语言

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

摘要

Contract-based software development has long been a leading methodology for the construction of component-based reactive systems, embedded systems in particular. Contracts are an effective way to establish boundaries between components and can be used efficiently to verify global properties by using compositional reasoning techniques. A contract specifies the assumptions a component makes on its context and the guarantees it provides. Requirements in the specification of a component are often case-based, with each case describing what the component should do depending on a specific situation (or mode) the component is in. We introduce CoCoSpec, a mode-aware assume-guarantee-based contract language for embedded systems built as an extension of the Lustre language. CoCoSpec lets users specify mode behavior directly, instead of encoding it as conditional guarantees, thus preventing a loss of mode-specific information. Mode-aware model checkers supporting CoCoSpec can increase the effectiveness of the compositional analysis techniques found in assume-guarantee frameworks and improve scalability. Such tools can also produce much better feedback during the verification process, as well as valuable qualitative information on the contract itself. We presents the CoCoSpec language and illustrate the benefits of mode-aware model-checking on a case study involving a flight-critical avionics system. The evaluation uses Kind 2, a collaborative, parallel, SMT-based model checker extended to fully support CoCoSpec.
机译：长期以来，基于合同的软件开发一直是构建基于组件的反应性系统（尤其是嵌入式系统）的领先方法。合同是在组件之间建立边界的有效方法，可以通过使用组成推理技术有效地用于验证全局属性。合同规定了组件根据其上下文进行的假设及其提供的保证。组件规范中的要求通常是基于案例的，每种情况都描述了组件应根据组件所处的特定情况（或模式）执行的操作。我们引入CoCoSpec，这是一种基于模式的，基于假设担保的合同作为Luster语言的扩展而构建的嵌入式系统的Java语言。 CoCoSpec允许用户直接指定模式行为，而不是将其编码为条件保证，从而防止丢失特定于模式的信息。支持CoCoSpec的模式感知模型检查器可以提高在假定保证框架中发现的成分分析技术的有效性，并提高可伸缩性。这样的工具还可以在验证过程中产生更好的反馈，以及合同本身上有价值的定性信息。我们介绍了CoCoSpec语言，并在涉及飞行关键型航空电子系统的案例研究中说明了模式识别模型检查的好处。评估使用Kind 2，这是一种基于SMT的协作，并行，模型检查器，已扩展为完全支持CoCoSpec。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号