A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866914717334765568 |
|---|---|
| author | Ishii, Daisuke |
| author_facet | Ishii, Daisuke |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_10919 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method Ishii, Daisuke Software Engineering 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. |
| title | A Hypergraph-based Formalization of Hierarchical Reactive Modules and a Compositional Verification Method |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2403.10919 |