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
Proc. of the 5th International Workshop on the Foundations of Coordination Languages and Software Architectures (FOCLASA), volume 175(2) of Electronic Notes in Theoretical Computer Science, 19--37, 2007

Details
Bibtex

KurzfassungAbstract
The paper reports on the foundations and experimental results with a model checker for component connectors modelled by networks of channels in the calculus Reo. The specification formalisms is a branching time logic that allows to reason about the coordination principles of and the data flow in the network. The underlying model checking algorithm relies on variants of standard automata-based approaches and model checking for CTL-like logics. The implementation uses a symbolic representation of the network and the enabled I/O-operations by means of binary decision diagrams. It has been applied to a couple examples that illustrate the efficiency of our model checker.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{KB2007,
  author    = {Sascha Kl{\"{u}}ppelholz and Christel Baier},
  title     = {Symbolic model checking for channel-based component connectors},
  booktitle = {Proc. of the 5th International Workshop on the Foundations of
               Coordination Languages and Software Architectures (FOCLASA)},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {175(2)},
  year      = {2007},
  pages     = {19--37},
  doi       = {10.1016/J.ENTCS.2007.03.003}
}