Symbolic model checking for channel-based component connectors
Research output: Contribution to journal › Research article › Contributed › peer-review
Contributors
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
Original language | English |
---|---|
Pages (from-to) | 688-701 |
Number of pages | 14 |
Journal | Science of Computer Programming |
Volume | 74 |
Issue number | 9 |
Publication status | Published - 1 Jul 2009 |
Peer-reviewed | Yes |
External IDs
ORCID | /0000-0002-5321-9343/work/173985297 |
---|---|
ORCID | /0000-0003-1724-2586/work/173988428 |
Keywords
ASJC Scopus subject areas
Keywords
- Binary decision diagrams, Branching time logic, Constraint automata, Data streams, Model checking, Reo