摘要: 1、研究背景（context）
实时发布订阅协议RTPS是在工业上被广泛使用的分布式通信协议，它是OMG标准化的数据分发服务（DDS）实施的互操作性协议。该协议定义了参与通信的各方实体、所传递消息的格式、以及消息如何在通信实体之间进行可靠传输，等等。RTPS协议旨在提供可信赖的通信功能。它对实时和概率特征建模，用于描述协议中对响应时间的限制，以及可能的数据丢失。然而，目前还缺少对RTPS协议的执行规范的形式化描述和验证方法，因此通信的可靠性不能严格保证，并且，协议的性能也缺乏形式化分析。
2、目的（Objective）
该论文将使用形式化方法，对RTPS协议的执行规范进行形式化建模和验证，严格验证RTPS协议的正确性，并形式化地分析关于实时和概率特征的参数对协议性能的影响。
3、方法（Method）
该论文首先使用Simulink/Stateflow对RTPS协议进行图形化建模，并针对协议的需求进行仿真分析。然而，仿真并不能严格保证模型行为的正确性。因此，我们提供了一套转换规则，将Simulink/Stateflow模型转换为Uppaal模型，并严格证明了转换前的Simulink/Stateflow模型是转换后Uppaal模型的精化。然后，我们对转换后的Uppaal模型进行形式化验证，其中验证的性质定义为TCTL逻辑公式。同时，我们还对Uppaal模型进行统计模型检测，形式化分析模型的性能。精化关系保证了文中所验证的TCTL性质在原来的Simulink/Stateflow模型上仍旧保持成立。
4、结果（Result&Findings）
本文的工作为RTPS协议的建模、仿真和验证建立了一个完整的框架。使用Simulink/Stateflow对RTPS协议进行形式化建模和仿真。使用Uppaal模型检测，形式化验证了RTPS协议的如下重要性质：Writer和Reader对于数据的写入和读取满足一致性和顺序性；协议所提供的heartbeat和acknowledgement机制能够保证通信的可靠性。这些性质都可以由精化关系所保证，因此在原来的Simulink/Stateflow模型上仍旧保持成立。通过形式化验证，为RTPS协议的正确性提供了更强的保证。另一方面，经过验证的Simulink/Stateflow模型可以直接生成可信赖的可执行代码。
我们还用统计模型检测分析了RTPS协议的定量性质，例如，在某一个给定时间期限内完成输入数据的传输的概率，可以定义为通信错误率以及传输延迟时间的函数。这能够为协议具体实现在选择参数时提供有效的指导。
5、结论（Conclusions）
本文为RTPS协议的建模、仿真和验证建立了一个完整的框架。建立了RTPS的形式化模型，并针对关键的实时、概率等特征进行仿真和验证，这为协议的正确性和效率提供了比测试更有力的保证。
本文只处理RTPS协议的有限方面，未来可能的扩展包括考虑协议的消息片段和发现模块。