| 基于TLA＋的BRP协议规约及验证 |
| |
| 引用本文： | 陈立前,王戟,陈火旺.基于TLA＋的BRP协议规约及验证[J].计算机工程与科学,2006,28(1):12-15. |
| |
| 作者姓名： | 陈立前 王戟 陈火旺 |
| |
| 作者单位： | 国防科技大学计算机学院,湖南,长沙,410073 |
| |
| 基金项目： | 中国科学院资助项目;国家科技攻关项目 |
| |
| 摘 要： | BRP协议是为不可靠信道上传送大数据包文件设计的工业协议。该协议的正确性依赖于各部件实时方面的假设。本文主要阐述了使用时序规约语言TLA＋对BRP协议进行规约和验证的过程。首先通过自然语言非形式化地描述BRP协议的基本原理和需求，在此基础上建立了BRP的形式化模型，利用TLA＋先对不考虑实时要求的BRP进行规约，然后添加实时约束获得BRP完整的规约，最后使用模型检验器TLC验证BRP协议的各种性质。
|
| 关 键 词： | BRP TLA＋ ABP规约 验证 模型检验 |
| 文章编号： | 1007-130X(2006)01-0012-04 |
| 修稿时间： | 2004年10月29 |
TLA+Based BRP Specification and Verification |
| |
| CHEN Li-qian,WANG Ji,CHEN Huo-wang.TLA+Based BRP Specification and Verification[J].Computer Engineering & Science,2006,28(1):12-15. |
| |
| Authors: | CHEN Li-qian WANG Ji CHEN Huo-wang |
| |
| Abstract: | |
| |
| Keywords: | BRP TLA ABP |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程与科学》浏览原始摘要信息 |
|
点击此处可从《计算机工程与科学》下载全文 |
|
