Type-Based Verification of Delegated Control in Hybrid~Systems (Full Version)

TL;DR

This paper introduces a type-based verification system for hybrid systems that enables modular, global analysis of object interactions and supports delegated control, demonstrated on a cloud-based model.

Contribution

It presents a novel type-and-effect system that computes post-regions globally while verifying locally, handling delegated control in hybrid systems.

Findings

Successfully verified a cloud-based hybrid system model.

Handled systems with changing control objects over time.

Enhanced modularity in hybrid system verification.

Abstract

We present a post-region-based verification system for distributed hybrid systems modeled with Hybrid Active Objects. The post-region of a class method is the region of the state space where a physical process must be proven safe to ensure some object invariant. Prior systems computed the post-region locally to a single object and could only verify systems where each object ensures its own safety, or relied on specific, non-modular communication patterns. The system presented here uses a type-and-effect system to structure the interactions between objects and computes post-regions globally, but verifies them locally. Furthermore, we are able to handle systems with delegated control: the object and method that shape the post-region change over time. We exemplify our approach with a model of a cloud-based hybrid system.