Towards the Coordination and Verification of Heterogeneous Systems with Data and Time
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908492723388416 |
|---|---|
| author | Kräuter, Tim Rutle, Adrian Lamo, Yngve König, Harald Durán, Francisco |
| author_facet | Kräuter, Tim Rutle, Adrian Lamo, Yngve König, Harald Durán, Francisco |
| contents | Modern software systems are often realized by coordinating multiple heterogeneous parts, each responsible for specific tasks. These parts must work together seamlessly to satisfy the overall system requirements. To verify such complex systems, we have developed a non-intrusive coordination framework capable of performing formal analysis of heterogeneous parts that exchange data and include real-time capabilities. The framework utilizes a linguistic extension, which is implemented as a central broker and a domain-specific language for the integration of heterogeneous languages and coordination of parts. Moreover, abstract rule templates are reified as language adapters for non-intrusive communications with the broker. The framework is implemented using rewriting logic (Maude), and its applicability is demonstrated by verifying certain correctness properties of a heterogeneous road-rail crossing system. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_12325 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Towards the Coordination and Verification of Heterogeneous Systems with Data and Time Kräuter, Tim Rutle, Adrian Lamo, Yngve König, Harald Durán, Francisco Software Engineering Modern software systems are often realized by coordinating multiple heterogeneous parts, each responsible for specific tasks. These parts must work together seamlessly to satisfy the overall system requirements. To verify such complex systems, we have developed a non-intrusive coordination framework capable of performing formal analysis of heterogeneous parts that exchange data and include real-time capabilities. The framework utilizes a linguistic extension, which is implemented as a central broker and a domain-specific language for the integration of heterogeneous languages and coordination of parts. Moreover, abstract rule templates are reified as language adapters for non-intrusive communications with the broker. The framework is implemented using rewriting logic (Maude), and its applicability is demonstrated by verifying certain correctness properties of a heterogeneous road-rail crossing system. |
| title | Towards the Coordination and Verification of Heterogeneous Systems with Data and Time |
| topic | Software Engineering |
| url | https://arxiv.org/abs/2508.12325 |