Symbolic model checking for channel-based component connectors

Publikation: Beitrag in FachzeitschriftForschungsartikelBeigetragenBegutachtung

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

OriginalspracheEnglisch
Seiten (von - bis)688-701
Seitenumfang14
FachzeitschriftScience of Computer Programming
Jahrgang74
Ausgabenummer9
PublikationsstatusVeröffentlicht - 1 Juli 2009
Peer-Review-StatusJa

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