Event-B is a well known methodology for the verified design and development of systems that can be characterised as discrete transition systems. Hybrid Event-B is a conservative extension that interleaves the discrete transitions of Event-B (assumed to be temporally isolated) with episodes of continuously varying state change. While a single Hybrid Event-B machine is sufficient for applications with a single locus of control, it will not do for autonomous systems, which have several loci of control by default. Multi-machine Hybrid Event-B is designed to allow the specification of systems with several loci of control. The formalism is succinctly surveyed, pointing out the subtle semantic issues involved. The multi-machine formalism is then used to specify a relatively simple incident response system, involving a controller, two drones and three responders, working in a partly coordinated and partly independent fashion to manage a putative hazardous scenario.

翻译：Event-B是一种广为人知的方法论，用于可表征为离散转移系统的验证设计与开发。混合Event-B是其保守扩展，它将Event-B的离散转移（假定在时间上相互隔离）与连续变化的状态演化阶段交错组合。虽然单个混合Event-B机足以应对具有单一控制焦点的应用场景，但对于默认具有多个控制焦点的自主系统则不再适用。多机混合Event-B旨在支持具有多个控制焦点的系统规约。本文简要梳理了该形式化体系，并指出其中涉及的微妙语义问题。随后运用多机形式化方法对相对简单的事件响应系统进行规约，该系统包含一个控制器、两架无人机和三个响应单元，通过部分协同、部分独立的方式运作，以应对预设的危险场景。