Symbolic Model Checking for Channel-based Component Connectors
Symbolic Model Checking for Channel-based Component Connectors
复制标题
DOI：
10.1016/j.entcs.2007.03.003
复制
发表时间：
2007-06
期刊：
影响因子：
--
通讯作者：
Sascha Klüppelholz;C. Baier
中科院分区：
文献类型：
--
作者：
Sascha Klüppelholz;C. Baier
本文报道了用微积分RIO中的通道网络模拟元件连接器的模型检查器的基础和实验结果。规范形式主义是一种分支时间逻辑，允许对网络中的协调原则和数据流进行推理。底层的模型检测算法依赖于基于标准自动机的方法和CTL类逻辑的模型检测的变体。该实现使用了网络的符号表示和通过二叉决策图实现的I/O操作。它已经被应用于两个例子，说明了我们的模型检查器的效率。
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.