Core Hybrid Event-B I: Single Hybrid Event-B machines
Core Hybrid Event-B I: Single Hybrid Event-B machines
复制标题
DOI：
10.1016/j.scico.2015.02.003
复制
发表时间：
2015-07-01
影响因子：
1.3
通讯作者：
Zhu, Huibiao
中科院分区：
文献类型：
--
作者：
Banach, Richard;Butler, Michael;Zhu, Huibiao
当今，面对对正确设计的混合系统和信息物理系统日益增长的需求，在Event - B的背景下考虑了包含连续变化行为以及通常的离散状态变化的问题。提出了一种名为混合Event - B的Event - B扩展，它在常见的离散转换（在此背景下称为模式事件）之间容纳连续行为（称为柔顺事件）。连续状态变化可以通过常微分方程的间接规范组合，或者通过将变量赋值为依赖于时间的值的直接规范，或者通过要求行为遵循依赖于时间的谓词的间接规范来指定。讨论了扩展的语法元素，并根据变量的依赖于时间的赋值属性描述了语义。参照从离散Event - B继承的细化概念详细研究了细化。提出了一整套证明义务，涵盖了新框架的所有方面。给出了一些示例和案例研究。一个特别的挑战——考虑到符合关于离散Event - B的现有直觉的必要性以及对工具支持的影响（如在像Rodin这样的离散Event - B工具中所体现的）——是设计整个框架，以便尽可能少地干扰处理离散Event - B的现有结构。© 2015 Elsevier B.V.保留所有权利。
Faced with the increasing need for correctly designed hybrid and cyber-physical systems today, the problem of including provision for continuously varying behaviour as well as the usual discrete changes of state is considered in the context of Event-B. An extension of Event-B called Hybrid Event-B is presented, that accommodates continuous behaviours (called pliant events) in between familiar discrete transitions (called mode events in this context). The continuous state change can be specified by a combination of indirect specification via ordinary differential equations, or direct specification via assignment of variables to values that depend on time, or indirect specification by demanding that behaviour obeys a time dependent predicate. The syntactic elements of the extension are discussed, and the semantics is described in terms of the properties of time dependent valuations of variables. Refinement is examined in detail, with reference to the notion of refinement inherited from discrete Event-B. A full suite of proof obligations is presented, covering all aspects of the new framework. A selection of examples and case studies is presented. A particular challenge - bearing in mind the desirability of conforming to existing intuitions about discrete Event-B, and the impact on tool support (as embodied in tools for discrete Event-B like Rodin) - is to design the whole framework so as to disturb as little as possible the existing structures for handling discrete Event-B. (C) 2015 Elsevier B.V. All rights reserved.