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

TL;DR

This paper extends Hybrid Event-B to multi-machine systems, enabling formal specification and verification of autonomous systems with multiple control points, demonstrated through a multi-agent incident response example.

Contribution

It introduces a multi-machine formalism for Hybrid Event-B, addressing semantic challenges and enabling modeling of complex autonomous systems with multiple control loci.

Findings

Successfully specified a multi-agent incident response system

Highlighted semantic issues in multi-machine Hybrid Event-B

Demonstrated the approach with a coordinated drone 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.