基于TLA+的BRP协议规约及验证

• 作者: 王戟 陈火旺 陈立前
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: BRP TLA+ ABP 规约 验证 模型检验
• 年，卷（期）: 2006,（1）
• 所属期刊栏目: 计算机网络与安全
• 页码范围: 12-15
• 页数: 4页
• 分类号: TP393
• 字数: 3941字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2006.01.005

摘要

BRP协议是为不可靠信道上传送大数据包文件设计的工业协议.该协议的正确性依赖于各部件实时方面的假设.本文主要阐述了使用时序规约语言TLA+对BRP协议进行规约和验证的过程.首先通过自然语言非形式化地描述BRP协议的基本原理和需求,在此基础上建立了BRP的形式化模型,利用TLA+先对不考虑实时要求的BRP进行规约,然后添加实时约束获得BRP完整的规约,最后使用模型检验器TLC验证BRP协议的各种性质.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王戟	国防科技大学计算机学院	41	880	14.0	29.0
2	陈火旺	国防科技大学计算机学院	56	1155	18.0	33.0
3	陈立前	国防科技大学计算机学院	4	10	2.0	3.0