对ROS2的DDS的形式化分析

论文阅读
留言

一篇对ROS2的DDS的形式化分析

image-20211129142233026

模型组成

模型由下述五部分组成：

节点、发布缓存、订阅缓存、DDS缓存、传输信道

概念过程表示

概念和过程表示如下：

节点——N1，N2·····

发布缓存——Pn——bp[n]

订阅缓存——Sn——bs[n]

DDS缓存——bds

传输信道——bc

DDS收集信息——Publishing Interfacce ——数据从bp[n]到bds

DDS分发数据——Subscribing Interface——数据从

bc到bs[n]

信道中的数据丢失概率——pn

论文特点

优先级问题：论文使用的是非抢占式优先级

PTA（概率时间自动机）是一个对有限自动机在时间和概率上的一个扩展

各模块详细建模

A.节点模块

image-20211129142248474

状态集（PTA中是Location）：Init、Send_wait、Receive

不变式：true、无、t<=TRH（接受和处理消息的最大时间）

迁移：

变量：时钟变量t、临时存储的发送消息：tmp_pub、publisher的buffer : bp、subscriber的buffer bs

B. Publishing Interface 模块

image-20211129142300962

状态集： Init、Collect

不变式：true、t<=TCH

变量：时钟变量t、DDS的buffer bds

collect时优先级高的pb[n]先进行收集，如果bds满了就删除buffer中第一条消息

C. 数据分发模块

image-20211129142322826

状态集：Init、 根据数据类型不同，有5个其他状态、PUB（发布注册）、UNP（取消发布）、SUB（订阅注册）、UBS（取消订阅）、DAT（普通消息）

不变式：true、t<=TNH(*4),t<=TDH

变量：时钟变量t、publish表pub、subscribe表sub、传输信道的buffer bc

D. Subscribe Interface模块

image-20211129142336749状态集：Init、Match、Distribute

不变式：true、无、t<=TTH

变量：sub表中和bc[0]的topic对应的 sub[j]、sub[j]的nodeID tmp1、bs[tmp1]的当前大小（新消息存放位置） temp2，时钟变量t、概率p[i]

其中涉及的数据结构

消息：一个结构体，包含node_id、type、消息内容

bds：一维队列，存放的是消息

sub表和pub表：一维数组，存放的是消息

bc：一维队列，存放的是消息

bs和bp：二维数组，第一维表示某一个节点的publisher或subscriber（也就是消息的node_id），然后数组存放单元为消息

性质提取与统计分析

安全性 无死锁

活性 Nn可以到达Send_Wait位置

高优先级节点平均有更高的概率来先发送数据 低优先级的节点的pb满的概率比高优先级节点的pb满的概率大 低优先级节点的pb空的概率比高优先级的节点小

image-20211129142827662