网络服务行为的进程代数验证方法研究及其应用  

A Study on Network Service Behavior Verification with Process Algebra and Its Application

作　　者：陈福[1,2] 杨家海[2] 杨扬[3] 王元卓[4] 贾美英[3] 

机构地区：[1]北京外国语大学计算机科学与技术系,北京100089 [2]清华大学信息科学与技术国家实验室,北京100084 [3]北京科技大学计算机科学与技术系,北京100083 [4]中国科学院计算技术研究所网络重点实验室,北京100083

出　　处：《计算机学报》2011年第9期1660-1668,共9页Chinese Journal of Computers

基　　金：国家"八六三"高技术研究发展计划项目基金(2009AA01Z251;2008AA01A303);国家"九七三"重点基础研究发展规划项目基金(2009CB320505);国家科技支撑项目(2008BAH37B05);国家自然科学基金(60873192;61070182;60873193;60803123);中央高校基本科研业务费专项资金(2010XJ025)资助~~

摘　　要：通过形式化建模分析了系统特点,确认系统行为,从而尽可能避免系统的冲突等情况.文中提出了一种使用进程代数描述网络服务组件的行为建模方法,包括强模拟、强互模拟、时效性、触发器、服务环境等网络服务交互行为描述方法,然后给出了P2P节点的节点发现、防火墙穿越等行为的描述,提出了适用于托管的RCMMS网络自管理协议,并使用代数的方法描述协议行为,确认其合理性,从而验证文中所提出的方法.With formalization and modeling system, we can analyze system characteristics, verify system behavior and try to avoid conflicts through. This paper presents a behavior modeling method for network services components using process algebra, including strong simulation, strong bisimulation, timeliness, service triggers, and service content. Then the P2P discovery of nodes and firewall traversal behavior description are presented. And a network self management protocol named RCMMS is proposed with process algebra description to verify the proposed method.

关 键 词：进程代数 Π演算 服务行为 交互系统演算 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]