Formal verification of a TDMA protocol start-up mechanism
Formal verification of a TDMA protocol start-up mechanism
复制标题
TDMA协议启动机制的形式化验证
DOI：
10.1109/prfts.1997.640153
复制
发表时间：
1997
期刊：
影响因子：
--
通讯作者：
Henrik Lönn
中科院分区：
文献类型：
--
作者：
Henrik Lönn
本文介绍了DACAPO协议的启动算法的正式验证。该协议使用TDMA（时部多访问）总线仲裁。经过证实，从任意初始状态开始，四个通信站的集合在有限的时间内同步并运行。系统模型包括与/SPL PlusMn/10/SUP -3/相对应的时钟漂移。使用定时自动机网络对该协议进行建模，并使用符号模型检查器Uppaal进行验证。
This paper presents a formal verification of the start-up algorithm of the DACAPO protocol. The protocol uses TDMA (Time Division Multiple Access) bus arbitration. It was verified that an ensemble of four communicating stations becomes synchronized and operational within a bounded time from an arbitrary initial state. The system model included a clock drift corresponding to /spl plusmn/10/sup -3/. The protocol was modeled using a network of timed automata, and verification was performed using the symbolic model checker UPPAAL.