节点之间的通信规则是分布式系统所承载的计算机网络的基础,随着网络服务要求的提高,网络系统的复杂性在协议方面体现出空间分布性、并发性、异步性、不稳定性和多样性,越来越要求采用系统工程的方法来设计和维护系统,在系统的整个生命周期内,用图形化的数学工具来完成系统的形式描述、正确性验证、性能评价、目标实现和测试。消息传递作为分布式系统之间的一种重要的通信方式,其实现机制的研究显得尤其重要。但是,目前的许多分布式消息通信开发方法并没有专门针对分布式系统的特点而制订,导致开发成本与风险增大。随着实际问题的复杂度提高,通过形式化的方法来解决问题的需求变得越来越强烈。论文文首先提出一种基于广播请求和点到点应答相结合通信方式的分布式消息传递机制(MPCBP 消息通信),利用分层有色Petri 网对消息的发送和接收处理、节点间通信进行一定程度的形式化描述。对整个系统模型各分模块进行可达图分析,通过系统整体模型的状态空间分析来进行属性验证。借助于时间相关CPNs模型以及一定的计算方法,对整个MPCBP 系统进行性能分析。论文研究工作的主要内容与创新表现在以下几个方面: (1)从理论角度研究了MPCBP 消息通信的基本架构。结合有色Petri 网形式化方法能极好的模拟分布性和动态性的特点,分析其形式化描述与分析的可行性; (2)用基于CPNs 理论的形式化方法实现了MPCBP 消息通信机制。所描述的通信系统通过广播通信方式发送请求包,以点到点方式发送响应消息。并且实现了消息包有损失时的检测和请求重发; (3)形式化实现虫孔寻径的流控策略。包括消息片的顺序传输、消息片丢失时对消息的抛弃处理和相应的请求重传以及消息片无中断的连续流动; (4)对构建的系统模型进行状态空间分析。借助CPN Tools 形式化分析工具,通过状态空间分析结果进行可达性动态属性验证。(5)进行系统的性能分析和评价。利用时间关联的CPNs 模型,通过多次模拟来研究系统的时间延迟、带宽使用等性能指标,最终得到系统的最适中的重传时间间隔。