BCL: A compositional contract language for embedded systems
BCL: A compositional contract language for embedded systems
复制标题
BCL：嵌入式系统的组合合约语言
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Christos Sofronis
中科院分区：
文献类型：
--
作者：
Orlando Ferrante;R. Passerone;A. Ferrari;L. Mangeruca;Christos Sofronis
大型复杂系统的设计要求能够在设计周期中尽早正确地指定和验证不同组件的交互，以确保满足全局水平的要求。我们使用基于契约概念的方法来解决这个问题。特别是，我们提出了一个图形和文本为基础的语言的需求定义，允许设计人员逐步和分层构建合同规范的系统组件组成一组简单而直观的模式。这些模式具有形式化的语义，并在Simulink框架中实现为监视器组件，用于运行时验证。合同与组件一起进行模拟，以验证满意度和兼容性。巡航控制的案例研究证明了该方法的有效性。
The design of large scale complex systems demands the ability to correctly specify and verify as early as possible in the design cycle the interaction of the different components that ensure that the global level requirements are satisfied. We address this issue using an approach based on the notion of contract. In particular, we propose a graphical and text-based language for requirement definition that allows designers to incrementally and hierarchically construct contract specifications for system components by composing a set of simple and intuitive patterns. The patterns have a formal semantics, and are implemented as monitor components in the Simulink framework for runtime verification. The contracts are simulated together with the components to verify both satisfaction and compatibility. A cruise control case study demonstrates the effectiveness of the approach.