Checking Equivalence for Reo Networks

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung

Beitragende

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

OriginalspracheEnglisch
Seiten (von - bis)209-226
Seitenumfang18
FachzeitschriftElectronic Notes in Theoretical Computer Science
Jahrgang215
PublikationsstatusVeröffentlicht - 29 Juni 2008
Peer-Review-StatusJa

Konferenz

Titel4th International Workshop on Formal Aspects of Component Software
KurztitelFACS 2007
Veranstaltungsnummer
Dauer19 - 21 September 2007
BekanntheitsgradInternationale Veranstaltung
Ort
StadtSophia-Antipolis
LandFrankreich

Externe IDs

Scopus 46049102575
ORCID /0000-0002-5321-9343/work/205988104

Schlagworte

Schlagwörter

  • Reo, bisimulation, coordination, partitioning splitter, symbolic model checking