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.

翻译：组合方法对于推理大型复杂系统至关重要。本文针对常用于建模信息物理系统的同步层次结构系统，重新审视了反应模块理论，并基于超图对其进行重构，以阐明模块的并行组合与层次化描述。进而提出一种层次化系统的自动验证方法：给定带有假设-保证契约标注的系统描述，该方法将系统分解为多个模块并分别验证，从而证明顶层系统满足其契约。该方法允许输入为子模块相互依赖的循环系统。实验结果表明，该方法可通过基于SMT的模型检查器有效实现。