Symbolic model checking for channel-based component connectors
Publikation: Beitrag in Fachzeitschrift › Forschungsartikel › Beigetragen › Begutachtung
Beitragende
Abstract
This paper introduces a temporal logic framework to reason about the coordination mechanisms and data flow of exogenous coordination models. We take a CTL-like branching time logic, augmented with regular expressions that specify the observable I/O-operations, as a starting point. The paper provides the syntax and semantics of our logic and introduces the corresponding model checking algorithm. The second part of the paper reports an implementation that relies on a symbolic representation of the coordination network and the connected components by means of binary decision diagrams. A couple of examples are given to illustrate the efficiency of the model checking techniques and their implementation.
Details
Originalsprache | Englisch |
---|---|
Seiten (von - bis) | 688-701 |
Seitenumfang | 14 |
Fachzeitschrift | Science of Computer Programming |
Jahrgang | 74 |
Ausgabenummer | 9 |
Publikationsstatus | Veröffentlicht - 1 Juli 2009 |
Peer-Review-Status | Ja |
Externe IDs
ORCID | /0000-0002-5321-9343/work/173985297 |
---|---|
ORCID | /0000-0003-1724-2586/work/173988428 |
Schlagworte
ASJC Scopus Sachgebiete
Schlagwörter
- Binary decision diagrams, Branching time logic, Constraint automata, Data streams, Model checking, Reo