本周主要阅读了两篇论文，其一是今年2-3月份发表在CCF B类会议DATE上的一篇short paper，题目是《Modeling, implementation, and analysis of XRCE-DDS applications in distributed multi-processor real-time embedded system》。其二是前年11月份发表在CCF C类会议ISPA上的一篇论文《Model checking for the Goal-Feedback-Result Pattern in ROS》。
Modeling, implementation, and analysis of XRCE-DDS applications in distributed multi-processor real-time embedded system
摘要
发布订阅机制是一种最近许多分布式应用中透明通信的设计模式。DDS是一个基于发布订阅机制的机器对机器的通信标准，旨在保证可靠、高效、互操作且实时数据交换。然而，对资源的高需求限制了DDS在低开销嵌入式系统中的使用。XRCE-DDS是一个基于客户-代理的标准，来使资源受限的小型嵌入式系统连接到DDS全局数据空间中。当前XRCE-DDS实现受限于主机操作系统，目标仅限于单处理器模块，并且缺乏性能分析方法。在这篇论文中，作者在CompSOC平台上实现了XRCE-DDS标准的裸机实现，来作为一个片上多处理器系统（MPSoC）上的一个实例。提出的框架包括一个硬实时XRCE-DDS的Client端和一个软实时XRCE-DDS的Agent端。一个场景感知数据流（SADF）模型被提出来，来捕捉在不同执行场景中系统的动态行为。作者通过使用经过实验验证的马尔可夫模型捕获概率场景切换来分析吞吐量的长期预期值。
主要贡献
- 在ZYNQ板上的CompSOC平台中实现了XRCE-DDS的裸机实现。客户端在硬实时的RISC-V处理器上实现，Agent跑在软实时的Arm处理器上。多个RISC-V处理器并行运行，每个处理器运行了多个客户端。
- 使用SADF表示了XRCE-DDS应用的概率模型。提出一个马尔可夫模型来分析长期预期吞吐量
Publisher端的SADF模型
Program这个actor代表的是一个实时程序，使用到了XRCE-DDS的两个接口，也就是Pub_Req和Pub_Res这两个用来publish消息的接口，这里抽象为两个actor。Agent位于Arm处理器上，通过非实时的网络和Client进行通讯，所以消息传输会发生丢失、延迟等概率行为。因此也就设计了多个不同的执行场景。
途中a和b代表的分别是信道上message的生产和消费速率，此处可以理解a为agent向DDS域成功发送的message。
- 场景p1代表时限内Agent成功publish了消息到DDS中
- 场景p2代表虽然经过很长时间（但未超时），但是Agent还是成功publish了消息到DDS中。
- 场景p3代表超时了，仍然未收到Agent发来的成功response，此时相当于未成功生产，所以a值为0。此时Pub_Res会让实时程序继续工作。
Subscriber端的SADF模型
这个模型和Publisher其实非常类似。但是可能的场景有4个，同时需要关注的信道有3个，DDS和Agent之间的非实时网络，Sub_Res和实时程序之间的可忍受的失败消息传递信道，以及多次可忍受失败导致的Sub_Res向实施程序下达重启的信道。
- 场景S1代表正常情况下快速的收到了DDS的消息
- 场景S2代表经过很长时间（但未超时），Client收到DDS消息
- 场景S3代表可忍受的消息传递失败，会先让程序继续工作，等待XRCE-DDS的历史变量和流运行完成，将已经收到的消息传递完（因为此时ef都还有消息在传递）。
- 场景S4代表n次可忍受的消息失败后，就不可忍受了，且此时历史消息已经都结束，那么就下达重启命令
应用的SADF模型
将上述两个模型进行结合，再加上实验中的具体数据，得到DDS域进行的时间场景D1,D2和D3，并得到他们的概率。同事在DDS域中的信息丢失与否也被两个场景进行建模为L1,L2。这样单个发布订阅者就存在了24个场景。
马尔可夫模型的SADF模型
通过两千万次迭代实验，得到上图的两个马尔可夫模型，然后结合上面对场景D和场景L的值，就可以得到24个大场景中两两转移的概率。从而可以计算预期吞吐量。
- 在CompSOC平台上的一个网络，进行实验分析了XRCE-DDS的应用
思考
- 首先这篇论文是对XRCE-DDS的建模分析，但是其本质却是立足于完整的DDS发布订阅机制来进行考量的，而不是针对XRCE-DDS的协议最核心的C-S机制进行建模分析。我觉得这一点是可以考虑学习的。但是还没想好跟ROS1相联系，毕竟ROS1没使用DDS
- 论文的贡献既然实现了对XRCE-DDS协议的一种实现，且是基于多处理器、嵌入式系统的一个实现，我觉得是一个比较大、比较新的工作量。不过说实话如果不是网络问题一直下载不下来，我觉得我们可能也已经走在这一步的路上了。
- 这个文章的概率其实解释的都挺笼统，大部分都说是从实验得来，那可能实验就是这样的吧，如果想要进行概率模型检测，无论是模拟还是实际的实验都需要进行统计。
Model checking for the Goal-Feedback-Result Pattern in ROS
摘要
目标-回馈-结果模式广泛运用于基于机器人操作系统的多任务进程和分布式控制系统的通讯中。随着越来越多的传感器设备和应用在服务机器人中被部署，保证ROS中的GFR通信结构的正确性和可靠性越来越重要。ROS中的GFR通信和任务调度的形式化分析和验证在本文中通过模型检测实现。为了对通信进程和调度策略进行建模，本文设计了客户端进程、服务端进程和调度器的时间自动机。无死锁、可调度和可响应性质使用CTL语言进行了形式化描述，并使用自动模型检测工具进行了自动验证。GFR模式的形式化模型分析和验证提供了一种精化设计模型，并且对避免基于机器人系统应用GFR早期设计阶段的细微错误或者bug很有帮助。
主要贡献
模型检测被用于带调度的GFR通信机制的形式化分析和验证。建立了时间自动机来描述通信进程和调度策略。并使用CTL语言描述了无死锁、可调度和可响应等性质，然后使用了UPPAAL进行了自动检测。
关于调度这方面，主要是实现了EDF（最早截止时间）的调度算法。
建立的模型主要构成为三个模块——client、scheduler和server
- client可以发布目标（goal），也可以取消正在进行的任务
- scheduler用来维护一个任务队列，同时负责抢占相关
- server用来执行client所布置的、由scheduler交给的goal，并根据时间触发向client汇报执行情况（feedback），当最后任务完成\终止\取消后，目标（goal）有结果之后，向client发送result消息。
三者自动机分别如下所示
- idle状态就是起始状态，信号goal[id]表示触发的要scheduler调度的任务，数组result[id]=0,ggoal[id]=1,getback[id]=0表示了目标id的结果、feedback等的初始化。
- router状态是一个路由状态，此处在等待其他信号的到来，如果scheduler发送了dealit[id]表明要处理任务了，则进入connect这个中间状态再转入active状态，如果scheduler发送了wait[id]信号，则说明任务队列前面还有任务，就需要进入waitit状态进行等待。如果说收到了server发来的finish[id]信号，说明任务已经完成了， 可以回到idle状态了。或者如果收到server发来的canceled[id]信号，说明此时任务已经取消了，同样回到idle状态。
- waitit状态需要等待任务队列前面的任务顺利完成或取消后，自己就会有dealit[it]信号通知转入connect中间状态，不停留，直接转到active状态。
- active状态存在三种可能的路径
- 收到了server的信号，任务已经finish了，那就回到idle状态
- 向server发出信号cancel[id]，通知server任务取消。回到router状态。
- 来了一个优先级更高的任务由scheduler调度到前面，把自己抢占了，也就是收到了bepreemptedp[id]信号，进入preempted状态等待重新被启用。
- preempted状态会等待dealit[id]信号的到来，然后回到active状态。
- 同时，为了模拟feedback，在goal发出后，未被抢占的三个状态——router、waitit和active状态都会定时发送feedback[id]信号，来得到server执行过程中的信息。getback[id]赋值为1表示等待得到回馈。
- idle状态就是起始状态，最开始时Sstatus[front()]为0，当收到scheduler发来的dealit[front()]信号时，将时间t进行初始化，进入deal状态。或者当Sstatus[front()]为2时，说明是在deal状态中被抢占的任务，当收到scheduler发来的dealit[front()]信号时，则不需要对时间初始化，而是需要将Sstatus[front()]初始化，进入deal状态。
- deal状态负责处理任务，在这个阶段设计三个概念，最快执行时间、截止时间（DL）和执行时间（ET）。当任务完成后，t超过了DL，则将结果result[front()]赋值为2，表示超市完成，并进入名为outtime的临时状态，然后进入router状态；或者当任务完成时，t大于了执行时间，但是没超过截止时间DL，那么就将result[front()]赋值为3，表示时限内完成任务，进入router状态。同时在此状态还有一种转移情况是当收到scheduler发来的抢占信号bepreempted[e]，就需要将Sstatus[e]赋值为2，表示被强占，进入preempted的临时状态，candeal赋值为1表示下次可以进行下个任务的处理，最后回到idle状态。最后还有一种情况，就是在执行过程中，client不想要再继续执行，向scheduler发送了cancel信号，scheduler就会发来getfinish[front()]信号，此时deal状态就会将result[front()]赋值为1，表示取消任务，然后进入一个临时状态，紧接着进入finised状态
- router状态可以理解是一个中间状态，但是很奇怪论文没有给出它的转移guard（可能是抽象掉了），总之它也可以响应scheduler的getfinish[front()]信号，取消放弃任务，将result[front()]赋值为1,进入临界状态然后直接进入finished状态。同时他也会被优先级更高的任务进行抢占，响应抢占信号bepreempted[e]，将Sstatus[e]赋值为1，然后当下一次dealit信号来临时直接转移回router状态。而除此之外的正常情况，他会在这一状态和客户端建立联系，然后进入connect的临时状态，然后顺利进入finished状态。
- finished状态是任务已经不再执行的一个状态，一般包含三种任务，一种是被取消掉的，一种是超时完成的，一种是正常完成的，该状态会等待finish[front()]信号，然后回到idle状态。
- 同client状态对应，在deal状态、router状态以及finished状态，都会对client中的feedback信号进行接受，但是具体处理细节不太相同 ，ideal状态会将feedback[e]被赋值为1表示此时任务还在处理中，然后getback[e]赋值为0表示已进行回馈；router状态会将feedback[e]被赋值为2表示此时任务已处理完成，等待路由的建立，然后getback[e]赋值为0表示已进行回馈；finish状态则会将feedback[e]被赋值为3表示此时任务已结束，然后getback[e]赋值为0表示已进行回馈。
- idle状态就是起始状态。如果此时任务队列长度len为0，当client的goal[e]信号到达时，就会将任务e放入任务队列，并将任务e的截止日期赋值给x,并进入一个瞬时状态，然后发出dealit[front()]信号通知server对任务队列队首进行处理；如果队列长度不为0，那么该状态会马上向server发送dealit[front()]信号通知它来处理队首任务。
- select状态是最关键的状态。
- 收到client发来的goal[e]信号，如果该事件的截止日期比x要小，那就要把x更新为该事件的截止日期上限，并进入preempted的瞬时状态，因为该事件显然应该具有更高优先级；然后将此时的队首进行抢占，即向server发送bepreempted[front()]!消息，且将队首任务出队，进入下个瞬时状态，发送dealit[front()]!让server进行下一个队首任务的处理，如果此时candeal为1则赋值为0表示不可以处理下个任务（这里应该是和server做的一个同步操作），然后回到select状态。
- 如果收到goal[e]信号，新入队的任务的DL比x要大，说明它的优先级不强，放入队尾，向client发出wait[tail()]信号。回到select状态。
- 如果收到cancel[e]信号，则进入getcancel状态，如果此时dealcancel为0，发送canceled[e]给client，表示已经取消了任务，并出队任务，且将任务e的result改为1表示取消任务，回到select状态。如果dealcancel为1，则需要向server发送getfinish[front()]信号，将dealcancel改为0。进入新状态后，如果收到server的finish[front()]，说明该任务已经取消，则出队队首元素，回到idle状态。
- 如果收到server的finish[e]，说明该任务已经结束，如果该任务就是队首元素，那么出队队首元素，并进入idle状态。
思考
这篇论文跟之前我和师兄做的工作有所关联，都是对ROS进行的建模、验证，区别在于我们将建模的对象放在了发布-订阅机制上，而本文则是将研究重心放在了所谓的GFR机制上，这个GFR机制其实就是ROS1中的action通信。是基于pub/sub和client/service机制的ROS独有机制。根据论文的网址，我们看到确实在相关的库的介绍中，甚至是存在有specification的。
那这确实感觉是一个非常不错的切入点。
这篇论文的建模感觉确实抽象层次挺高，忽略了大部分细节，集中注意力在client、server和scheduler这三个地方，我觉得对scheduler部分的抽象是本文的一个亮点，尤其是将调度器如何执行了EFD调度算法这一部分建立的蛮有新意。但是有一些没有特别看懂，就是被强占的任务的后续处理没看的很明白，因为有一些执行的函数在论文中没有讲。
总结思考
如何对前后工作进行联系
关于之前的，能不能接着我们之前对ROS1验证的思路往下走，看能不能走到我们的MicroROS上，我缕了一下两者的关系，大概是这样的：
ROS1和ROS2作为一二代，互成竞品
ROS1中最常用的和嵌入式部分进行通信的是rosserial包（官方实现有arduino等）。
而到了ROS2中和ROS2进行通信的就是MicroROS了。
要么参考第一篇论文，考虑像它那样，放弃对client-server的模式的底层建模，转而考虑对整体的的建模。然后再想办法加别的工作量。
要么就是围绕ROS2再做一些工作，从而可以过渡到MicroROS上来。问题就是其他人已经做过了对ROS2中DDS的建模了，那可能就还要调研一下到底做什么东西。
建模思路和工作量努力方向的拓展
之前的建模思路主要集中在最直接最底层最简单的机制进行建模，然后根据specification和代码细节丰富模型。但实际上太过追求往底层靠进行抽象的话，感觉会忽略掉更具有代表性的独特的机制，就比如ROS1中我们一直在深挖pub/sub机制，但好像往上面一层的action相较而言更具有创新点以及更具有对ROS应用的代表性。
感觉自己可以考虑再跳出来，不考虑实现细节，实现底层，而是协议或者系统最具代表性的层次来抽象建模。
然后就是感觉仅仅靠阅读源码、建立模型，工作量无法支撑好的文章，还是得想办法做模拟、做实现；甚至考虑多环境、多处理器、多平台的实现。同时考虑到第二篇论文对scheduler的建模是一个亮点，再加上XRCE-DDS的Agent端中的Agent类同样继承了一个Scheduler类（不过是FCFS的比较简单的调度），这方面能不能提炼出什么值得深挖实现，然后进行建模的东西呢？
原文链接: https://zijian.wang/2021/09/23/2021-9-22周记/
版权声明: 转载请注明出处.