  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.
