Symbolic Model Checking for Channel-based Component Connectors

11 years 11 months ago
Symbolic Model Checking for Channel-based Component Connectors
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.
Sascha Klüppelholz, Christel Baier
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors Sascha Klüppelholz, Christel Baier
Comments (0)