A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method

TL;DR

This paper introduces a hypergraph-based formalization of hierarchical reactive modules and presents an automatic, compositional verification method for complex synchronous systems, enabling modular analysis even with circular dependencies.

Contribution

It reformulates reactive modules using hypergraphs for better hierarchical and parallel reasoning and develops an SMT-based verification approach for modular systems with assume-guarantee contracts.

Findings

Effective verification of hierarchical systems with circular dependencies.

Implementation demonstrated using SMT-based model checker.

Supports modular verification of complex cyber-physical systems.

Abstract

The compositional approach is important for reasoning about large and complex systems. In this work, we address synchronous systems with hierarchical structures, which are often used to model cyber-physical systems. We revisit the theory of reactive modules and reformulate it based on hypergraphs to clarify the parallel composition and the hierarchical description of modules. Then, we propose an automatic verification method for hierarchical systems. Given a system description annotated with assume-guarantee contracts, the proposed method divides the system into modules and verifies them separately to show that the top-level system satisfies its contract. Our method allows an input to be a circular system in which submodules mutually depend on each other. Experimental result shows our method can be effectively implemented using an SMT-based model checker.