网络体系结构建模和性能评价形式化方法——随机进程代数.pdfVIP

第 34 卷第 11 期 数学的实践与认识 V o l34　N o 11　 2004 年 11 月 M A TH EM A T ICS IN PRA CT ICE AND TH EO R Y N ove. , 2004　 网络体系结构建模和性能评价的 形式化方法——随机进程代数 1, 2 1 1 1 冯烟利 , 　余镇危 , 　潘　耘 , 　刘克俭 ( ( ) ) 1. 中国矿业大学机电与信息工程学院 北京校区 , 北京　100083 (2. 山东工商学院信息工程学院, 山东 烟台　 264005) 摘要: 　随机进程代数是从经典进程代数发展起来, 用于并发系统的定性和定量分析的形式化方法, 特别适 合在计算机网络和通信协议的建模和性能评价. 首先介绍了 SPA 的语法和操作语义. 并以令牌环局域网模 型为例来说明其应用. 进一步讨论了 SPA 的三种等价关系, 以期解决模型状态空间爆炸问题. 关键词: 　形式化方法; 随机进程代数; 性能评价 1　引　　言 　　计算机网络体系结构是指导计算机通信协议设计和实现的逻辑框架, 它包含了模型化 的通信功能, 网络资源的分配及各模块或构件的交互等. 网络系统是具有分布和并发特性 的复杂系统, 需要用形式化方法进行精确的描述和验证. 所谓形式化方法就是具有坚实的 [ 1 ] 数学理论基础并由此给出一个形式化规范语言来描述系统行为的方法 . 形式化方法为计 算机网络的性能评价提供了一种有效的、抽象的、低廉的模型工具. 计算机网络的性能可分 为定性指标和定量指标. 定性指标包括可靠性、有无死锁和活锁、活性及公平性等等. 定量 指标包括系统的吞吐量、用户的响应时间和资源的利用率等. 相应地可以把形式化方法分 为两类: 一类只描述并发系统的功能特性, 对系统进行定性分析. 有代表性的方法是有限状 [ 2 ] [ 3 ] ( ) [ 4, 5 ] ( ) 态机 、 网 和进程代数 等. 一类是增加了定量分析的参数 如时间和概率 , Petri PA [ 6 ] [ 7 ] [ 8 ] ( ) 例如排队网络 、随机Petri 网 和随机进程代数 SPA 等. 由于系统的性能建模与系统 设计紧密相连, 只考虑系统的定性指标已满足不了需求, 具有定量性能分析的形式化方法成 为更加有力的工具. 2　从 PA 到 SPA 进程代数是基于代数形式建立并发系统的模型并提供对模型结构和行为进行推理的工 [ 4 ] [ 5 ] 具, 包括 CCS 和 CSP . 在进程