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

摘要

随机进程代数是从经典进程代数发展起来,用于并发系统的定性和定量分析的形式化方法,特别适合在计算机网络和通信协议的建模和性能评价.系统模型中的每个活动赋予一个服从指数分布的时间变量,由此可将进程代数的语义模型转换为连续时间的马尔科夫链,易于进行性能测量的计算.本文首先介绍了SPA的语法和操作语义.作为一个应用,分析了令牌环局域网模型.进一步讨论了SPA的三种等价关系,并给出了相应的等价公式,以期解决模型状态空间爆炸问题.利用这些等价公式可对模型进行语义重写来简化模型.