基于Uppaal的通信协议消息传输的流水线技术的建模与分析

王长青

同济大学软件学院，上海 201804

0 引言

在嵌入式系统中，有很多是基于通信协议的消息传递，那么一个消息从发送到接受需要多少时间呢？多个消息传输又需要多少时间呢？有没有减少通信时间的可能性？因此，为了研究这几个问题，我们做了一个实验，即我们模拟一个通信协议，我们把这个通信协议通过UPPAAL[1]、[2]、[3]建成一个时间自动机的模型，然后模拟利用流水线技术进行消息传输，最后我们得到一组数据，然后我们对这组数据进行分析，以此研究采用流水线技术减少时间通信的可能性。

在第1节中，我们简要的描述了这个通信协议，在第2节中，我们分析了这个通信协议，并对流水线传输机制进行了建模，在第3节中，我们对这个系统的属性进行了验证，在第4节中，我们进行了总结并提出了以后可以改进的可能性。

1 通信协议的模拟

1.1 通信协议的简单描述

这个通信协议是非常容易理解的，即有一个通信媒介，一个发送者，一个接受者，消息的长度是固定的并且我们假定这个通信媒介传送消息是有延迟的。比如传送消息延迟为delay，那么当我们在时刻t的时候发送一个消息，接受者接受消息应该是在t +delay。

1.2 一些通信协议的假设

为了便于模拟，我们提出了一些假设：1）消息传递过程中是没有丢失的；2）接受者接收到消息时，对消息的处理时间为零。基于以上假设，当消息达到接受者时，接受者会立即发送一个成功信号。

2 基于UPPAAL工具的流水线建模

我们采用流水线技术来模拟发送，即我们把介质发送的延迟时间分段，其中每段为固定的消息长度，这样我们就可以得到一些段，这些段就可以组成一个流水线，我们就可以模拟这个流水线进行消息传输。

在这个模型设计中，为了便于研究，我们假设消息长度为5，消息传递延迟为消息长度的整数倍，假设为15，下面是模型中用到的一些公共变量：

1）int[0,1] buffer[3]={0,0,0} 这是一个消息队列，用来存放要发送的消息，此队列大小为3，其中0代表没有消息，1代表有消息；

2）int[0,1] medium[3] = {0,0,0} 这是流水线的状态标志，0代表此段空闲，1代表此段正在处理消息；

3）urgent chan msg_ok 当消息达到接受者时，接受者发送此信号；

4）urgent chan medium_ok 当一个消息传输完时，流水线时间自动机会发送此信号；

5）urgent chan b_medium1 流水线第一段处理完消息时发送的信号；

6）urgent chan b_medium2 流水线第二段处理完消息时发送的信号；

7）urgent chan go消息时间自动机准备好要发送的消息时发送的信号；

8）int totleTime = 0 发送所有消息总的时间消耗。

9）int lock = 0防止系统出现死循环的锁。

下面是两个函数：

2.1 消息模型

消息模型主要实现了以下几个步骤：1）准备消息，消息的长度为5；2）消息准备好时，检查消息队列是否满；3）如果消息队列满了，则等待；否则，发送信号给发送者。如图1.4描述了消息模型。

2.2 发送者模型

发送者模型主要实现了以下功能：接受消息模型准备好消息的信号，把消息放到消息队列中。图1.5描述了发送者模型。

2.3 流水线模型

主要实现了以下几个步骤：1）检查消息队列，看有没有要发送的消息；2）从消息队列中拿第一条消息，模拟延迟；3）发送信号给流水线第二段；4）处理下一条消息；5）流水线第二段接受流水线第一段的消息；6）模拟延迟；7）发送信号给流水线第三段；8）处理下一个消息；9）流水线第三段接受来自流水线第二段的消息；10）模拟延迟；11）发送消息给接受者，令其接受消息；12）消息队列消息数量减一。如图1.1，图1.2，图1.3所示。

2.4 接受者模型

接受消息，并检查所有消息是否传输完成。图1.6描述了接受者模型。

2.5 获取消息传输总时间的模型

当消息队列中的消息传输完后，我们会得到所有消息传输的总时间，这个功能有两个模型组成，分别为observer和loop，其中loop负责监控消息是否全部完成，observer负责计算时间。如图1.7，1.8所示。

3 系统属性的分析和验证

A[] not deadlock 这个系统不会死循环。

4 结论

在整个试验中，我们依次模拟了5条，20条，50条，100条消息传输所需的时间，实验结果如下图所示：

消息数 采用流水线技术花费时间不采用流水线技术花费时间 时间减少百分比5 47 75 24.00%20 135 300 55.00%50 314 750 58.13%100 615 1500 59.00%

从以上结果可以看出，随着消息数的增多，减少的时间逐渐增多，最终可以达到一半以上，这说明在基于通信协议的消息传输过程中，流水线技术可以大大减少传输所需要的时间。后面的实验我们会考虑两点：1）传输延迟不是固定的；2）传输延迟长度可能小于消息长度。

[1]Systems and Software Verification: Model-Checking Techniques and Tools, B.Berard (Author),M.Bidoit (Author),A.Finkel (Author),F.Laroussinie (Author),A.Petit (Author),L.Petrucci (Author),P.Schnoebelen (Author),P.McKenzie.

[2]Temporal Verification of Recactive Systems:Safety,Zohar Manna (Author),Amir Pnueli (Author).

[3]UPPAAL Manual, www.uppaal.com.