AlgebraicSystems: Compositional Verification for Autonomous System Design

TL;DR

AlgebraicSystems introduces a compositional verification framework using algebraic and categorical methods to analyze emergent behaviors in autonomous system design, enhancing model interoperability and safety assurance.

Contribution

It presents a novel algebraic and categorical approach for compositional verification, enabling better management of emergent behaviors in autonomous systems.

Findings

Framework supports interoperability of models through algebraic and categorical primitives

Enhances safety and security property verification in autonomous systems

Facilitates analysis of emergent behaviors via structure-preserving model transformations

Abstract

Autonomous systems require the management of several model views to assure properties such as safety and security among others. A crucial issue in autonomous systems design assurance is the notion of emergent behavior; we cannot use their parts in isolation to examine their overall behavior or performance. Compositional verification attempts to combat emergence by implementing model transformation as structure-preserving maps between model views. AlgebraicDynamics relies on categorical semantics to draw relationships between algebras and model views. We propose AlgebraicSystems, a conglomeration of algebraic methods to assign semantics and categorical primitives to give computational meaning to relationships between models so that the formalisms and resulting tools are interoperable through vertical and horizontal composition.