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

TL;DR

The paper addresses scalable formal verification for synchronous CPS with hierarchical structure, noting that existing implementations of reactive-module theory struggle with large models and circular dependencies. It introduces a hypergraph-based formalization of reactive modules and a decomposition method that maps a hierarchical module $M[M_1,\ldots,M_n]$ to a parallel composition $M_1 || \cdots || M_n || M^\dagger$ and verifies $M[M_1,\ldots,M_n] || M_a \preceq M_g$ using assume-guarantee contracts and an SMT-based model checker. A prototype implementation demonstrates automatic verification for subcontracts and top-level contracts across examples. The approach enables automated, scalable compositional verification for hierarchical CPS designs.

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.

Figures (2)

• Figure 1: Example system.
• Figure 2: Compositional verification.

Theorems & Definitions (2)

• definition thmcounterdefinition
• definition thmcounterdefinition