对MQTT的形式化分析和建模

论文阅读
留言

一篇对MQTT发布订阅协议的形式化工作

MQTT简述

一个消息发布订阅协议

MQTT3.1.1控制包类型

  1. CONNECT 客户端在建立和服务端的链接后发送的第一个数据包。服务端收到两个时说明违反协议断开连接
  2. CONNACK 服务端对CONNECT的一个确认链接请求的回复。是服务端发到客户端的第一个包。如果客户端等待这个包超时，则客户端关闭连接。
  3. PUBLISH 发送消息
  4. PUBACK 当存在QoS时，会对PUBLISH进行确认
  5. PUBREC QoS 2 对PUBLISH包的确认
  6. PUBREL 对PUBREC的回复
  7. PUBCOMP 对PUBREL的回复
  8. SUBSCRIBE 客户端发出 创建一个subscriptions，注册一个或多个客户端感兴趣的话题。同时该消息会注明对于该subscriptions，服务端可以向客户端发送消息的最大QoS。
  9. SUBACK 对SUBSCRIBE的确认，并处理该包
  10. UNSUBSCRIBE 取消订阅。
  11. UNSUBACK 对UNSUBSCRIBE的确认
  12. PINGREQ 表明client依旧活跃，或测试网络连接依旧存活
  13. PINGRESP 对PINGREQ的回应，表明服务端依然存活
  14. DISCONNECT 客户端最后发送来断开连接的。

QoS的等级

  • QoS 0（最多一次传输）—— 发送者发送PUBLISH，接收者接受消息

  • QoS 1 （最少一次传输）—— 发送者发送PUBLISH和一个未使用的包标识符，必须收到接收者回复的PUBACK才视作PUBLISH发送成功。

另一方面，接收者必须回复一个PUBACK包，且对所有传入的含有相同包标识符的PUBLISH数据包进行这样的对待

  • QoS 2 发送者和QoS2的发送类似。但是除此之外，他必须在收到PUBREC时回复PUBREL。接收者对PUBLISH的回复是PUBREC，接收 PUBREL 时，它不能导致重复的消息被传递，它必须通过发送包含与 PUBREL 相同的包标识符的 PUBCOMP 包来响应 PUBREL 包。

非形式化表述

两部分，其一是链接与断开连接，其二是发布与订阅

形式化建模

半形式化建模

就是UML建立类图和序列图

基于PTA的形式化建模

没有概率的模型

对代理的建模

  1. subscriber端的建模

    image-20211201090349858

  2. publisher端的建模

    image-20211201090404460

​ B12的环是检测链接是否还在

​ 当收到client的PUBLISH的时候，进入结束接收l，发送pub_broc信号进入B8`````

对Subscription、Unsubscription和Connection的建模

image-20211201090428329

有概率和时间的模型

对Subscriber建立的概率模型

image-20211201090448062

对Publisher建立的概率模型

image-20211201090500008

SMC和概率时间自动机解决了可达性和安全性因空间爆炸不可判定的问题

验证的性质

image-20211201090540298