Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX
Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX
复制标题
使用 TReX 对 IEEE 1394 根争用协议进行参数化可达性分析
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
M. Sighireanu
中科院分区：
文献类型：
--
作者：
Aurore Collomb;M. Sighireanu
我们报告了 IEEE 1394 根争用协议的完全参数化模型的可达性分析。该协议使用时间限制来选举领导者。有趣的一点是，时序约束涉及一些参数（传输延迟、等待间隔的界限），并且协议的行为强烈依赖于这些参数之间的关系。为了综合确保协议正确行为的关系，我们应用了 TReX 工具中实现的符号可达性技术。我们采用[24]中提出的根争用协议的非参数化模型，并研究该模型的不同参数化版本。我们能够自动综合通过对非参数化版本的证明或实验已经发现的所有关系。我们将我们的结果与使用其他参数化系统工具报告或获得的结果进行比较。
We report about the reachability analysis of fully parametrized models of the IEEE 1394 root contention protocol. This protocol uses timing constraints in order to elect a leader. The interesting point is that the timing constraints involve some parameters (transmission delay, bounds of waiting intervals), and the behavior of the protocol strongly depends on the relation between these parameters. In order to synthesize the relation ensuring the correct behavior of the protocol, we apply the symbolic reachability techniques implemented in the TReX tool. We take the unparameterized model of Root Contention protocol proposed in [24] and study different parametrized versions of this model. We are able to synthesize automatically all the relations already found by proof or experiments on the unparameterized versions. We compare our results with those reported or obtained using other tools for parametrized systems.