Symbolic model checking for channel-based component connectors

Sascha KlüppelholzSascha Klüppelholz, Christel BaierChristel Baier

DOI Link

Sascha Klüppelholz, Christel Baier
Symbolic model checking for channel-based component connectors
Science of Computer Programming, 74(9):688--701, 2009

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@article{KB2009,
  author  = {Sascha Kl{\"{u}}ppelholz and Christel Baier},
  title   = {Symbolic model checking for channel-based component connectors},
  journal = {Science of Computer Programming},
  volume  = {74},
  number  = {9},
  year    = {2009},
  pages   = {688--701},
  doi     = {10.1016/J.SCICO.2008.09.020}
}