Checking Equivalence for Reo Networks
Research output: Contribution to journal › Research article › Contributed › peer-review
Contributors
Abstract
Constraint automata have been used as an operational model for component connectors described in the coordination language Reo which specifies the cooperation and communication of the components by means of a network of channels. This paper addresses the problem of checking equivalence of two Reo networks. We present a compositional approach for the generation of a symbolic representation of constraint automata for Reo networks and report on an implementation that realizes a partitioning splitter technique for checking bisimulation equivalence for Reo networks. Using a special operator on our symbolic data structure enables efficient treatment of the rich labeled transitions in constraint automata. In order to show the power of this approach we then present some benchmarks.
Details
| Original language | English |
|---|---|
| Pages (from-to) | 209-226 |
| Number of pages | 18 |
| Journal | Electronic Notes in Theoretical Computer Science |
| Volume | 215 |
| Publication status | Published - 29 Jun 2008 |
| Peer-reviewed | Yes |
Conference
| Title | 4th International Workshop on Formal Aspects of Component Software |
|---|---|
| Abbreviated title | FACS 2007 |
| Conference number | |
| Duration | 19 - 21 September 2007 |
| Degree of recognition | International event |
| Location | |
| City | Sophia-Antipolis |
| Country | France |
External IDs
| Scopus | 46049102575 |
|---|---|
| ORCID | /0000-0002-5321-9343/work/205988104 |
Keywords
Keywords
- Reo, bisimulation, coordination, partitioning splitter, symbolic model checking