PC-手机下载系统的协议分析与优化

理论计算机科学电子笔记164（2006）205-224www.elsevier.com/locate/entcs面向系统升级的张苗苗，1岁同济大学软件工程学院中国上海邓文雄2联合国大学中国澳门摘要对于嵌入流式下载协议的PC-手机下载系统，存在数据不能正确地从PC传输到手机，或者传输速度慢得令人无法接受的问题。为了解决这些问题，我们进行了形式化分析的协议与一些定时参数和给定的概率的消息丢失和无序数据使用概率模型检测工具PRISM。我们介绍了一种技术，以减少状态空间的系统建模的协议，这是一个网络概率时间自动机在PRISM上的实验结果给出了一个清晰的解释，并有助于确定最佳的参数设置，以满足工业要求。保留字：流式下载协议，概率模型检验，Prism。1介绍流式下载协议用于将软件下载到手机中，以便进行工厂测试、安装和系统升级。该协议由一家通信公司实现，后来用于一个PC-移动系统中，出现了一些正确性问题，如软件不能下载或下载软件所需的时间过长。这些鼓励我们使用某种形式的机械支持（如模型检查器或定理证明器）对协议进行形式化分析。我们的正式分析是基于该公司使用的真正的PC移动下载系统，1电子邮件地址：miaomiao@mail.tongji.edu.cn2电子邮件地址：dvh@iist.unu.edu1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.07.020206M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205该协议是嵌入式的。该协议传输的下载程序被组织成包含在帧中的数据包，PC机和手机之间的数据链路是两线USB（通用串行总线）连接。该协议的机制有点类似于滑动窗口协议[10]，除了这里我们对窗口移动和重新发送采取了不同的处理。由于数据链路参数包括USB总线的大小和传输时延是影响系统性能的主要因素，我们将在我们的论文中仔细考虑这些因素。与在发送器和接收器上都具有滑动窗口的文献[5，6 另外，本文主要对下载性能进行了分析，而对移动端数据帧的处理该系统的一个重要预期属性是与时间相关的：软件下载可以尽可能快地完成。为了测量下载时间，我们引入了这个系统模型的定时信息参数。 典型的是PC端的帧发送间隔和超时值、USB的传输时间延迟以及移动端的处理时间。 该协议表现出定时和不确定性行为。此外，本文中的系统与其他滑动窗口论文[5，6，10]中的系统之间的一个关键点区别在于，在该系统中存在一些过渡的可能性，例如关于帧丢失的过渡，并且考虑了无序帧概率。一个自然的模型，体现了不确定性，概率和实时方面，称为概率时间自动机，这是时间自动机[1]的概率扩展，已在[2]中提出，并在这里采用建模系统。我们所分析的系统属于部分同步系统的子类，其中（i）帧通过链路的传输延迟和移动端的处理延迟可以不确定地取值，但受某个常数的限制，（ii）每个发送但未被接收的帧都需要一个计时器来记录自发送以来所经过的时间，作为决定是否重发帧的基础，（iii）系统中使用的所有时钟同时演进，（iv）对于下载软件包，帧的数量通常很高，因此系统状态的数量很大。通过模型检查来验证这些系统通常是非常困难的，因为时间自动机的状态空间在计时器的数量上呈指数增长。 许多现实的算法和协议都属于难处理的部分同步系统。例子包括用于在不可靠信道上可靠传输数据的滑动窗口协议[5]，以及ZeroConf协议[15，7，17]，其目的是动态配置IPv4链路本地地址。在实际的下载系统中，下载软件的每一帧都有一个唯一的地址来区分自己和其他的，而对于建模来说，这可能会导致状态爆炸。为了避免一个大的状态空间，没有必要给下载软件的每个帧不同的我们只标记那些当前M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205207在滑动窗口内。这表面上保证了该窗口中每个帧的唯一标识。当窗口移动时，窗口左侧的一些帧会在窗口外部结束，而相同数量的新帧会从窗口右侧进入。从左边离开窗口的帧的标签然后被重新用于进入窗口的新帧。窗口移动累积变量move指示已经成功下载的帧的数目。因此，结合移动，标签在尚未从窗口中移除的已发送帧中总是唯一的，因此不会对协议机制造成问题，尽管它可能已用于已成功下载的帧。由于每个发送的帧都与一个定时器相关联，因此还需要根据此标签设置仔细考虑定时器分配和释放。在本文中，我们专注于定性行为的系统类似的性能分析的滑动窗口协议的仿真工具POOSL在[3]。然而，我们的论文中的分析更为正式。此外，我们的系统中所提出的算法、行为和机制更加完善，更接近于现实。本文的主要贡献是给出了上述下载系统的形式化模型，并通过引入一些定时参数来修改协议规范以满足系统要求。利用概率模型检验器PRISM（PRISM的详细信息见[8]和[9]）对不同参数值变化的实验结果表明了定性性质，这可以清楚地解释工业中遇到的问题，有助于确定最佳参数设置和以确定多个关键参数来提高系统性能，例如超时周期、传输时间延迟和处理时间。本文的其余部分组织如下。下一节将对下载协议进行概述，并介绍该协议在实践中遇到的问题。 在第三节中，回顾了概率时间自动机的概念，然后分析和构建了作为概率时间自动机网络的下载协议的抽象系统模型。 在第4节中，我们使用PRISM来分析系统的性能相对于系统参数的不同值第五部分是本文的结论2PC-Mobile系统及下载协议在本节中，我们将概述下载协议，并列出行业内出现的一些问题。2.1整个系统通过该协议传输的信息被组织成包含在帧内的分组。帧包含一个已被编码用于在特定链路上传输的分组。链接具有明确的最小和最大长度以及必须出现在其中的一组所需信息。PC和移动设备之间的链接是双线USB，这是一种插入式连接，208M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205用于连接PC和移动设备（参见图1，其中通道1和通道2代表两条线）。因此，系统中有四个主要组件：PC，移动，通道1和通道2。同时，有四个USB总线，b1，b2，b3和b4，其中b1是PC USB发送总线，b2是移动USB接收总线，b3b 4是移动USB发送总线，b4是PC USB接收总线。 缓冲器b1和b2存储帧，b3和b4存储帧。 每次，一个帧首先发送到b1，然后信道1将其从b1发送到b2。在移动端处理完该帧后，移动端可以生成一个相应的确认给b3，然后通道2将该确认发送给b4，PC可以根据移动端的响应发出其他动作。USB比旧的端口（如串行和并行端口）更快。USB 1.1规格支持高达12 Mb/sec的数据传输速率，USB 2.0的最大传输速率为480 Mbps。 连接通常是无错误的，但偶尔会有导致帧丢失和无序帧的不良连接。 我们用p1表示消息丢失的概率 以及P2表示在移动侧发现的帧重新排序的概率。通道1PCB1B2移动通道2B4B3Fig. 1.下载系统为了从PC下载软件，首先PC通过有线信道1向移动设备发送hello帧，以通知移动设备它将开始传输软件，并且同时PC启动定时器z。如果移动设备准备好接受数据，它将通过有线信道2向PC发回AckH。否则，移动设备不发送任何内容。如果移动设备没有准备好接收数据，或者消息hello或AckH丢失，则定时器z将产生超时，这意味着PC在发送帧而没有接收到它之后已经等待了一定长度的确认时间。PC然后需要再次发送hello一旦接收到AckH，PC就开始发送软件的实际帧i并启动新的定时器t[i]。每一帧包含移动设备中该帧将被写入的闪存的相对地址，这样，不同的帧可以通过移动设备中闪存的不同目标地址来区分。在我们后面的模型中，我们将使用不同的整数来表示不同的帧。在接收到帧i时，移动设备检测帧中的错误（如果有的话），并丢弃任何无效（包括坏的或重复的）帧。通过检查帧的有效内容和检查帧校验序列（FCS）来检测帧i的成功接收以确认ack [ i ]响应，确认ack[i]被发送回PC，包括帧i的相对地址（标签）。如果定时器t[i]超时并且没有接收到ack[i]，则PC需要重新发送帧i。M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205209为了提高下载效率，在任何时候，发送方都保持与其正在发送或将要发送的帧相对应的连续标签（相对地址）的发送滑动窗口。该技术允许数据在一个方向上发送，在一对协议实体之间，受到未确认消息的最大数量的限制。窗口大小WS可以是未确认帧的最大数量。如果光标没有到达窗口的右端，PC在发送窗口中的另一帧之前不会等待确认帧。请注意，如果窗口中的所有帧都已发送，PC将等待，直到收到最左侧帧的确认。如果PC接收到确认，它可能会认为在被确认的帧之前发送的任何未确认的帧丢失或失败，需要再次发送它们。 这意味着，如果确认不对应于最左边的一个，窗口将不会移动。如果确认对应于最左边的确认，则窗口将向右移动一帧。这个过程一直持续到整个程序被传输。对于移动端，在它从b2得到一个帧后，它将通过检查它是否是好的来处理该帧，然后生成一个确认，如果该帧是正确的，它将被发送回PC。 从PC端成功接收到的帧被暂时存储在手机的RAM中，然后在每隔固定的时间间隔后，根据内部的地址，镜框2.2发现的问题该协议的目的是成功地下载软件到手机系统升级。然而，在一家通信公司的实施过程中，遇到了几个问题：• 下载过程不继续，软件根本没有下载。• 下载软件，但速度很慢。问题是如何更改协议参数以加快下载速度。经过仔细检查，该公司的人发现，由于b2中的缓冲器大小非常有限，PC发送帧的速度很快，实际上大部分帧都丢失了，因为移动端的数据处理速度慢，导致b2缓冲器的流量过大。为了解决这个问题，在协议实现中，他们添加了另一个参数TD，即发送两个连续帧之间的时间延迟，从而解决了第一个问题。 但是，他们设置的TD很大，下载一个小程序花了好几分钟。 虽然，他们还没有以正式的方式证明解决方案，仍然不清楚他们设定的TD是否合理。 此外，在协议中存在许多参数，并且关于参数如何影响性能以及如何使下载尽可能快地提出的问题需要进一步研究。这里应该注意的是，对于公司中实现的PC-Mobile系统，与USB总线相比，移动端有足够的RAM存储器，只有在检查总线b3中有空间之后，210M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205s∈S因此，在B3中，不存在缓冲器超过缓冲器为了分析协议，我们引入了一些与时间相关的参数，这些参数将出现在我们后面的模型中，除了出现在协议规范中的TO。这些参数如下所示。• 如前所述，TD是发送两个连续帧之间的时间延迟。• TO是超时值，从PC发送帧的时刻开始，直到重新发送帧的时刻（如果没有收到该帧的确认）。• TR是通过信道1或信道2的帧或确认的最大传输时间。• TP是移动设备对帧的最大处理时间。引入这一参数的目的也是为了分析上述两个问题。 如果在移动端处理帧比在PC端发送帧到信道1快得多，显然bu2 over bu 2就不会发生。缓冲器的大小BS也是影响协议性能的一个关键参数。这里我们假设缓冲器b1、b2和b3（不是b4）具有相同的大小BS。还存在其它参数，诸如要发送的帧的数量N（即，大小要下载的软件的大小）和滑动窗口的大小WS完整的下载系统不仅包括时间约束，而且还包括随机信息。对于这种系统的建模，我们使用概率时间自动机，我们认为这是最适合我们的目的。3抽象概率时间模型3.1概率时间自动机在本节中，我们回顾了[2]中的概率时间自动机模型和概率时间结构的概念及其语义。概率分布与马尔可夫决策过程集合S上的概率分布是映射p：S→ [0，1]，使得设置{s|s ∈ S且p（s）> 0}是有限的，且p（s）= 1。所有概率的集合S上的分布由μ（S）表示。马尔可夫决策过程是一个元组（Q，Steps），其中Q是一组状态，Steps：Q→ 2μ（Q）是为每个状态分配一组概率分布的函数。 直觉上，马尔可夫决策过程遍历状态在状态s中，该过程在步骤（s）中非确定性地选择概率分布p，然后根据p来概率性地选择要移动到哪个状态。 如[2]中所述，我们用一个来自于[1]的字母来标记选择概率分布的动作，并假设步骤：Q → 2×μ（Q）。 因此，过渡的形式a、pq−→q J，其中（a，p）∈ φ ×μ（Q）是这个转变的标志。我们还假设一个拉贝林函数L：Q →2AP，其中AP是一组原子命题，它将状态q与M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）2052110120LLL在状态q成立的原子命题。 然后，标记的马尔可夫决策过程是元组（Q，Steps，L）。La belled路径（或执行序列）是形式ω=l0l1l2q0−→ q1−→ q2− →. 、其中，qi是状态，而li是转换的标签对于路径ω，设first（ω）表示ω的第一个状态，如果ω是有限的，则设last（ω）表示ω的最后一个状态。 |ω|是ω的长度，定义为ω中跃迁出现的次数，如果ω无限，则为∞。 对于k ≤ |ω|，设ω（k）表示ω的第k个状态，并且step（ω，k）表示ω中第k次跃迁的标号。对于两条路径ω=l0l1l2LJandωJ=qJ−→0LJqJ−→1LJqJ−→2... 使得Qnq0−→ q1−→ q2− →. Q n=qJ，ω和ωJ的级联定义为J=l0l1l2J J J0J1J2。ωωq0−→ q1−→ q2− →. q n−→ q1 −→ q2 − →.时钟、时钟估值、时钟约束：设R表示非负实数集。时钟是一个以与实时相同的速率增加的实值变量。 令C ={x1.，xn}是一组时钟。时钟估值是一个函数ν：C →R，它为每个时钟分配一个实值。令RC表示所有时钟赋值的集合，0表示将0分配给C中的每个时钟的时钟赋值。 对于一组时钟X<$C，我们用ν[X：= 0]表示将0分配给X中的所有时钟并且与ν一致的时钟赋值所有其他钟表 对于t∈R，我们写ν+t为时钟赋值，v（x）+t到每个时钟x∈ C。C上的约束是形式为xi<$c或xi−xj<$c的表达式，其中i j，i，j≤n且n ∈ {<，≤，>， ≥}，c∈N.一个时钟估值ν满足一个时钟约束xi<$c（xi−xj<$c）i <$v（xi）<$c（v（xi）−v（xj）<$c）。C的区域是由约束的合取描述的赋值空间RC的凸子集对于一个区域和一组时钟X <$C，集合{v[X：= 0]|v ∈ n}也是一个区域，记为n [X：= 0]。令ZC表示C的所有区的集合概率时间自动机时间自动机作为实时系统的一种模型在文献[1]中被引入。 它们扩展了离散概率分布模型的概率实时系统。定义3.1概率时间自动机是一个元组G=（S，L，s<$，C，inv，prob，nτs∈S）consistinggof• 一个节点的有限集合S，• - 函数L：S → 2AP，将在该节点中为真的原子命题集合分配给自动机的每个节点，• astartnodes<$eS，• 一组有限的时钟C，212M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205• 函数inv：S →ZC，为每个节点分配不变条件，• 函数prob：S → 2μ（S×2C），为每个节点分配一组S × 2C上的离散概率分布，• 一族函数<$τs<$s∈S，其中对任意s∈ S，τs：prob（s）→ZC赋予每个p∈prob（s）一个使能条件。定义中的最后一项说，根据概率分布（在节点处选择）的所有概率选择都具有相同的启用条件。概率时间自动机的行为几乎与时间自动机相同，除了它必须在每个离散点p上选择一个概率分布。该系统将所有的日志初始化为0。时钟的值以相同的速率增加。在任何时间点，如果系统处于节点s中，则满足不变量inv（s）。 然后系统可以（a）保持在节点s，如果仍然满足inv（s），则让时间前进;或者（b）如果存在概率分布p∈prob（s），使得τs（p）满足时钟的当前值，则进行离散转移。因此，如果让时间前进违反了inv（s），那么如果不能进行离散转换，系统就会死锁。我们用ZC（G）表示G中出现的所有时钟区的集合，ZC（G） {inv（s）∈ ZC|s ∈ S}<${τ s（p）∈ ZC|s ∈ S且p ∈ prob（s）}。3.2建模思想在这一部分中，我们提出了我们的思想和方法来建模系统，主要涉及大的状态空间减少和相关的窗口移动的处理。首先，我们提出了一些假设，我们以后的分析与PRISM工具的系统。(i) 从一端发送到另一端的消息（帧或确认）到达的顺序与发送它们的顺序相同(ii) 消息传输有一个非零的时间延迟，即从一端发送的消息至少要经过一段时间才能到达另一端(iii) 由于移动设备需要检查帧是否是坏的，因此我们假设消息处理的时间不为零。(iv) 一旦确认到达b4总线，它将被立即处理，与移动中的处理时间相比，处理时间在PC中是如此之小，可以假设为零。因此，缓冲器b4从不存储超过1条消息。状态空间缩减和窗口移动在该协议中，软件下载的帧的数量可以超过一万个，这些帧通过不同的地址来区分，并且可以用整数来标记。此外，对于每个帧，我们需要几个不同的辅助变量来存储该帧的相关信息，包括（1）该帧是否被发送，(2)如果发送，哪个时钟记录其确认的时间流逝，（3）如果M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205213是否已经接收到该帧的确认，以及（4）该帧位于滑动窗口中的因此，即使对于一个小尺寸的软件包，状态空间可能会非常大，因为各种框架和它们的相关变量。为了避免模型检测中的状态空间暴露，我们使用变量来区分滑动发送窗口内的帧，而不是软件的每一帧。假设滑动窗口可以容纳WS帧，并且窗口中的位置由0到WS-1范围内的变量i表示。我们使用变量real[i]来表示当前窗口位置i的帧的标签。变量sent[i]用于指示窗口位置i处的帧，即具有标签real[i]的帧是否已被发送。类似地，变量ack[i]指示具有标签real[i]的帧的确认是否已被PC接收。一旦PC收到来自移动设备的响应，它将检查在哪个位置在窗口中，帧标签等于确认标签。更具体地说，假设位置是j，即标签与real[j]相同• 如果j=0，则将ack[j]设置为1。窗口不会移动，因此有关窗口移动的变量不会改变。• 如果j=0并且从位置1开始连续地存在已经接收到其相应确认的换句话说，存在m，0 ≤m< W S− 1，使得ack [0]= 1，且ack [1]= 1.。Rack[m] = 1。在这种情况下，窗口向右移动m+1步，窗口中剩余帧的位置减少m+1，而向量real中从位置0开始直到位置m的帧标签被移动到起始位置为WS-（m+1）和结束位置为WS-1的位置，以便重新用于刚刚进入窗口的帧新输入的帧ack [i]和sent[i]的相关变量，i ∈ {WS-（m+1），...，W S-1}被设置为0，意味着需要发送这些新帧。图（2）给出了WS= 6和m=2的情况的描述，这意味着窗口移动3步。位置i012345位置i012345real[i]ack[i]111010real[i]ack[i]010000框架体积需要移动新帧发送[i]111110发送[i]110000移动前后移动3步图二. 窗口移动3步窗口移动的步数由变量move累加，即move是当前滑动窗口的光标位置如果move等于帧的数量N，则所有的帧成功地到达移动设备，并且下载过程结束。让当前窗口的大小为WSD，它被初始化为WS。当move等于N-WSD时，即，未被传输的剩余帧的数量等于当前窗口的大小，当移动当前窗口时，012345345012214M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205我们将窗口大小相应地减小到WSD-1计时器评估当帧被发送时，定时器启动以记录经过的时间，以判断从发送帧起经过的时间是否随着超时TO而期满。当接收到确认或定时器超时时，定时器被释放，以便分配给即将发送的其他帧。由于在滑动窗口中存在最大WS帧，所以我们需要WS定时器。在这里，我们给出一些关于处理这些计时器的解释。我们将窗口中与帧real[i]相关的计时器t[real[i]]解释为模型中的时钟，其中i是窗口位置。在任何时候，t[real[i]]指示第实数[i]个时钟的当前时间。在TO时间单位内接收到帧real[i]的确认之后，或者当在TO时间单位之后t[real[i]]到期导致帧real[i]被重新发送时，我们需要将t[real[i]]重置为0。图（3）示出了在移动窗口3步之后t[real[i]]如何改变，在这种情况下，应该是刚刚接收到位置0中的帧的确认位置i012345位置i012345real[i]ack[i]111000real[i]ack[i]000000框架体积需要移动新帧发送[i]111110发送[i]110000t[real[i]]t[3] t[4] t[5][0条评论][1][2][3]t[real [i]]t[0] [1][2][3]t[3] t[4] t[5]移动前后移动3步图3.第三章。定时器前后窗口移动3步如果PC接收到一个帧的确认，它会假设在此之前发送的任何未确认的帧丢失或失败，需要再次发送，并且其相关时钟重置为0。重新发送帧从上述机制，我们得出结论，有两种情况下，一个帧将被重新发送。• 发送帧时，设置一个计时器来记录所经过的时间。 当定时器在TO时间单元之后到期而没有接收到针对该帧的确认时，则需要再次发送该帧。• 当帧i被发送时，定时器被设置以记录时间流逝。当接收到在帧i之后发送的帧j的确认，而没有接收到帧i的确认时，根据假设1，帧i或其确认丢失，这需要重新发送帧帧的唯一表达式我们假设任何帧及其对应的确认具有相同的标签。对于窗口位置j的帧，我们可以使用对（move，real[j]）作为帧的唯一标签。345012012345M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205215我们描述的程序PC的协议正式在Pseduo-Algol如下。数据数组帧[0..N-1];integer i，j，k，move，array real[0.WS-1];/*move是窗口移动累积 */ timer z，td，array t[0.. WS-1];/* timer td在从它开始的TD时间单位之后/* timer t[i]在TO时间单位后变为超时，从它的开始 */boolean array ack[0. WS-1]，发送[0..WS-1];/*使用 hello消息初始化 */move：= 0; sent：=false;ack：=false; /* 窗口位于开始处，窗口中没有发送或接收任何内容 */WSD：=min（WS，N）; /* 数据可以小于窗口 */，对于j=0到 WSDdoreal[j]：=j;int i =0;初始化：向信道1发送“hello”帧;启动定时器z;等待（z=超时）或接收到AckH;如果没有（接收到AckH），则转到init;/* 建立的通信 */开始计时器td;whilemove =N- 1 do begin/* 以下三个部分可以并行执行 *//*循环中的第1部分：不是原子的，并且需要时间*/ for i=0toWSDdo/*在 窗口中发送帧 */if（sent[i]=false）then /*send frame i*/开始wait（td = timemout）;send frames[move+i];/*frames[move+i]的标签为real[i]*/starttimert[real[i]];start timer td; sent[i]=trueend;/* 循环中的第2部分，应作为原子命令执行 *//* 检查已确认的帧 *//*max是窗口 中最右边的帧的索引已确认 */int max：=0;/*recevied_ack返回窗口中已确认的帧的标签 */for i=0 toWSD doif let（v= received_ack）in（v=real[i]）thenstart ack[i]：=true; max：=i end;/* 重新发送那些没有ACK且超时的帧 */for i=0 toWSD doif（t[real[i]]=timeout and not ack[i] and sent[i]）然后发送[i]：= false;/* 重新发送窗口中索引低于max的帧尚未确认 */对于i=0到max-1，如果（sent[i]=1而不是ack[i]），则sent[i]：=false;/* 循环中的第3部分：应作为原子命令执行 *//*如果 需要，检查并移动窗口*/ while（ack[0]and sent[0] andmove N-WSD）do/*将窗口向右移动一帧 */ begin k：=real[0];对于i=0到WSD-2，return [i]; return [i+1];ack[i]：= ack[i+1]; sent[i]：= sent[i+1]end;real[WSD-1]：= k; sent[WSD-1]：=false; ack[WSD-1]：=false; move：=move+1;端while（ack[0] and sent[0] andmove> N-WSD）do/*将窗口向右移动一帧*/对于i=0到WSD-2doreturn [i]; return [i+1];ack[i]：= ack[i+1]; sent[i]：= sent[i+1]end;move：= move+1; WSD：= WSD-1;端端216M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205可变意义范围使用[i]当使用时钟i时等于1（否则等于0）其中索引i对应于帧标签i0... 1发送[i]当发送帧的位置i窗口已发送（否则为0）0... 1ack[i]等于1时，接收窗口的位置i（否则为0）0... 1实数[j]窗口位置j0个......WS − 1t[i]自发送帧以来的当前时间i0... 到水务署当前窗口大小最初等于WS0... WS移动步骤窗口已移动0... Nb1[i]、b2[i]、b3[i]第i位分别位于缓冲器b1，b2和b3中，b1、b2和b3的数组大小为BS0... WS+ 1B4PC端0... WS+ 1nb1，nb2，nb3在bu中使用的位置数b1，b2，b3。0... BS充分但b2在b2上是否溢出。0个...... 1电话临时变量0个......WS − 1表1模型中使用的变量3.3协议模型在下文中，我们将PC-移动下载系统描述为由四个概率时间自动机组成的网络：PC，移动，通道1和通道2。除了上面提到的积分常数外，我们还引入了丢失消息率的概率p1，帧被重新排序的概率p2。由于窗口大小可能会在下载过程接近完成时发生变化，因此我们使用变量WSD来表征其变化。表1显示了我们模型中使用的变量。我们使用sent[i]来表示发送窗口位置i的帧是否 发送或不发送。这包括第一次发送帧和重新发送帧的情况，无论它已经发送了多少次。 缓冲器数组b1、b2、b3和变量b4的任何元素的值都在0和WS+1之间。从0到WS-1的值表示帧或分段标签。值WS表示没有帧或确认存储在这个位置，因此它是空的，而值WS+1表示存储的帧或确认与问候帧有关。这些缓冲器数组和b4的所有元素最初都设置为WS，所有其他变量都为设置为0。PC的模型如图4所示。自动机从位置0开始。位置0处的自循环转换表示程序被成功下载。如果软件还没有开始传输，则PC通过向服务器b1发送hello帧并同时设置定时器z来移动到位置1。一旦PC接收到hello确认，它就移动到位置2以下载软件。当定时器z超时并且没有确认到达时，需要重新发送hello从位置2经过位置3、4、5并在位置2结束的转换序列实现了发送帧的过程，该帧的位置i在M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）2052175b1[nb1]：=tel，nb1：=nb1[tel]：+86-10-20160700t[tel]：= 0移动>0移动=Nz=TD移动Nb1 =BSb 4 =WSz：= 00move= 0b1[0]：=WS+ 1nb1：=nb 1 + 1z：= 0z=TD移动N N−WSD tel：=real [0]对于i=0，i WSD −1，i ++，{real[i]：=real[i+1]，sent[i]：=sent[i+1]，ack[i]=ack[i+1]}real[WSD−1]：=tel，sent[WSD−1]：= 0，67对于n= 0，n j，n ++{ifack[n] = 0发送[n]：= 0}ack[0]= 0移动=Nack[0]= 1移动=N−WSD对于i=0，i WSD −1，i ++，{real[i]：=real[i+1]，sent[i]：=sent[i+1]，ack[i]=ack[i+1]}move：=move+1，W SD：=WSD −1滑动窗口是最小的并且被指示为还没有被发送，以启动计时器来记录自从帧被发送以来经过的时间，并且在B1中找到正确的位置来存储该帧。当PC在b4中找到确认i时，它将立即处理它。分别使用从位置2到位置6和位置7的转换，我们区分确认i的相关帧是否位于滑动窗口的第一个位置。 除此之外，PC还需要重新发送所有这些在被确认帧之前发送的未确认帧，如从位置6开始的转换所示。以位置7为中心的两个自循环转换模拟窗口移动场景。其中一个具有保护移动=N-WSD意味着移动后窗口大小减少1如果move等于帧的数目N或没有接收到对位置0中的帧的确认，则PC从位置7转移到位置2。在模型中，我们还考虑了发送两个连续帧之间的时间延迟设置为零的情况。可能会发生多个计时器同时超时的情况，因此每个计时器都应进行相应的处理。而对于延迟不为零的情况，根据模型假设，这种情况不会出现。见图4。 PC概率时间自动机通道1的模型如图5-a所示。自动机从位置1开始，它一直驻留在那里，直到b1中有一个帧，然后移动到位置1。根据该模型，信道1中的传输时间延迟的上限是TR218M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205p1对于i=1，i nb 1 −1，i ++，b 1[i −1]：=b1[i]b1[i]：=WS，nb 1：=nb 1− 1p2z2> 0对于i=1，i nb 2 −1，i ++，b 2[i −1]：=b2[i]b 2[i]：=WS，nb2：=nb2 −1移动=N移动=N紧急b1[0]/=WSz1：=0001z1≤TRz1> 0nb 2 =BS对于i=1，i nb 1 −1，i ++，b 1[i −1]：=b1[i]b 1[i]：=WS，nb1：=nb1 −1紧急2[0]=/W Sz2：=01z2≤TP1−p 2+TRTP > z2> 0dB 3 0± 2 0对于i=1，i nb 3 −1，i ++，b 3[i −1]：=b3[i]b 3[i]：=WS，nb3：=nb3 −1移动=N0紧急b3[0]/=WSz3：=01z3≤TR1−p 1z3> 0b 4 =WS b4：=b 3[0]对于i=1，i nb 3 −1，i ++，b 3[i −1]：=b3[i]b 3[i]：=WS，nb3：=nb3 −1假设只有当用于记录帧传输所经过的时间的时钟Z1大于0时，才能发生从位置1的输出转换。 当b2满时，来自b1的帧由于b2缓冲器过延而丢失，否则帧成功到达b2或仍然由于物理消息丢失而丢失。移动和通道2的模型分别如图5-b和图6所示。注意，移动自动机中的不变量是z2≤TP+TR。这是因为即使最大帧处理时间是TP，在b3已满的情况下，确认仍然会停留在移动设备的RAM中，并且直到移动设备发现有空的位置可以容纳它并立即将其无时间延迟地放入b 3才能到达b3。我们使用紧急过渡来表达这种情况。由于最大传输时间是TR，因此空闲空间的最大等待时间也是TR。图五. 信道1和移动概率时间自动机见图6。 通道2概率时间自动机4棱镜模型及其验证4.1Prism中的模型在本节中，我们简要介绍了我们在PRISM中的模型以及该工具的模型检查结果。PRISM是一个概率模型检查器，是一个对表现出概率行为的系统进行建模和分析的工具。 它是基于一个精确的数学模型的建设，具体如反应模块M. Zhang，L.Van Hung/Electronic Notes in Theoretical Computer Science 164（2006）205219[16]这是一个很好的例子。该模型由一组可以相互交互的模块组成，其中每个模块通常包括一组状态，表示系统的所有可能配置以及这些状态之间可能发生的转换。系统的特性随后以PCTL或CSL表示。由于在这个系统中存在概率性（消息丢失、帧重排）和非确定性行为（传输时延和处理时延），我们在PRISM中使用的建模形式是马尔可夫决策过程（MDP），它允许表达这些行为。 如前所述，该模型由PC、通道1、移动设备和通道2这四个模块，它们通过全局共享变量进行通信，并通过标记有相同操作的命令进行同步，以强制两个或多个模块同时进行转换。每个模块具有与我们之前介绍的相应自动机相同的功能。由于PRISM不支持数组，在PRISM模型中，我们以前在概率时间自动机中使用的任何变量数组都将根据数组的大小变为一组变量。例如，在我们以前的模型中