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

摘要

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.%通过形式化建模分析了系统特点,确认系统行为,从而尽可能避免系统的冲突等情况.文中提出了一种使用进程代数描述网络服务组件的行为建模方法,包括强模拟、强互模拟、时效性、触发器、服务环境等网络服务交互行为描述方法,然后给出了P2P节点的节点发现、防火墙穿越等行为的描述,提出了适用于托管的RCMMS网络自管理协议,并使用代数的方法描述协议行为,确认其合理性,从而验证文中所提出的方法.