Autonomous System Safety Properties with Multi-Machine Hybrid Event-B

TL;DR

The multi-machine formalism is 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.

Abstract

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.

Figures (4)

• Figure 1: A simple Event-B machine, together with its context.
• Figure 2: A schematic Hybrid Event-B machine.
• Figure 3: Illustrating Hybrid Event-B refinement.
• Figure 4: Multiple machines and their interfaces.