Symbolic model checking for channel-based component connectors

Research output: Contribution to journalResearch articleContributedpeer-review

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 languageEnglish
Pages (from-to)688-701
Number of pages14
JournalScience of Computer Programming
Volume74
Issue number9
Publication statusPublished - 1 Jul 2009
Peer-reviewedYes

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