ZEUS：分布式时间模型-并行计算基于KRONOS的理论研究

不《理论计算机科学电子札记》68卷第4期（2002年）URL：http://www.elsevier.nl/locate/entcs/volume 68. html20页sZEUS：一个分布式的时间模型--并行计算基于KRONOSV. Brabermana，1，4，A. Oliverob、2、5、F. Schapachnika，3a计算机科学系，FCEyN，布宜诺斯艾利斯大学，阿根廷b阿根廷布宜诺斯艾利斯阿根廷企业大学信息技术系摘要在这项工作中，我们提出了ZEUS，一个分布式模型-自组织，从工具KRONOS[8]发展而来，目前可以处理时间自动机上TCTL可达性属性[1]的向后计算[2]。ZEUS是遵循以软件架构为中心的方法开发的。它介绍了一些有趣的功能，如先验图分区，一个复杂的机器，以达到最佳性能（通信捎带和延迟消息）和死区时间利用率，其中每个处理器使用不活动的时间间隔来执行辅助，耗时的任务，稍后将加快其余的计算。虽然已经取得了一些良好的结果，早期的实验指出了困难，获得加速使用并行异步版本。我们还提出了一些克服这些障碍的途径。1介绍模型检查的研究集中在增加工具可以处理的问题的大小最终的浪潮是分布式计算的使用，其中一组计算机一起工作来解决问题[16，4，20]。分布式策略的有用性通常由“加速比”来衡量获得。n个处理器的加速比计算为t1n 其中ti是时间1 由UBACyT资助的研究资助X156和X094。2由UADE赠款PSI.2.2002资助的研究。3 电子邮件地址：fschapac@dc.uba.ar4 电子邮件地址：vbraber@dc.uba.ar5 电子邮件地址：aolivero@uade.edu.ar2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。BRABERMAN，OLIVERO和 SCHAPACHNIK2≤ ≤ ∧−用i个处理器完成验证目标通常是获得线性加速，尽管验证顺序版本耗尽其内存的情况也被认为是成功的。许多成功的工作已经做了分发untimed模型检查器[20，16，3，11，18 ， 5 ， 12 ， 14] 等 ， 然 而 ， 除 了 Behrmann ， Hune 和 Vaandrager 在UPPAAL [4]的分布式版本上的工作，没有做太多关于并行化或分发Timed模型检查器的工作。在这项工作中，我们提出了ZEUS，一个分布式模型-编译器，它从工具KRONOS[8]发展而来，目前可以处理时间自动机[2]上TCTL可达性属性[1]的向后计算。本文的其余部分组织如下：在第2节中，我们描述了我们的KRONOS工具的演变。第3节介绍了我们的分布式模型中最有趣的几第4节展示了一个版本的列车闸机控制器案例研究的几个配置上的性能，第5节介绍了经验教训，以及在研究中要采取的路径。2Kronos工具KRONOS[8]工具正式检查实时系统是否满足其要求。它建立在时间自动机理论[2]和时间时序逻辑的基础上，如TCTL [1]。虽然在现实世界的应用中得到了成功的应用[17，21，9]，但它无法处理与大多数其他工具相同的状态爆炸问题。主要问题是存储耗尽和无法使用多处理器设备时可用。尽管理解本文并不需要深入了解KRONOS形式和算法的技术知识，但我们将介绍主要概念，并将让感兴趣的读者参考大量领域[2，8]等）。时间自动机是一种将正实值时钟与自动机符号相结合的实时形式时钟记录事件之间经过的时间所有的时钟都是同步的，也就是说，它们都以同样的速度前进当发生转换时，允许将时钟重置为零。转换与作为时钟上的谓词的保护相关联。警卫决定何时可以进行转换。包含时钟会产生无限状态空间（控制位置加上时钟估值）。幸运的是，这并不意味着许多有趣问题的不可判定性，例如可达性。为了处理无限状态操纵，像KRONOS这样的工具将时钟估值的凸集表示为涉及一个时钟或两个时钟之间的差异的不等式的合取（例如，1X5 Xy > 8）。一种称为差异界限的矩阵（DBM）[10]通常用于处理此类信息。非凸集表示为凸集的并集。克罗诺斯表演BRABERMAN，OLIVERO和 SCHAPACHNIK3：定点引擎D：区域Fig. 1. 克罗诺斯建筑。可达性查询作为控制位置图上的非凸集的向后传播这种传播是从目标状态开始的适当优先运算符的定点计算。最终的答案是初始状态是否属于计算的固定点。完整的TCTL验证主要基于前面解释的算法[13]。在KRONOS术语中，每个凸集被称为一个区域，而凸集的并集被称为一个区域（不要与[2]的区域图混淆）。从概念的角度来看，它的架构可以被视为一个定点引擎，可以将其非凸集读取和写入区域3发行克洛诺斯：宙斯为了获得分布式时间模型，必须处理一些问题。作为必要条件，最终的架构必须是可证明正确的。正确性证明的草图见第3.1节。在业绩方面，应建立一种微妙的平衡。一方面，最大化的分配是需要的。另一方面，应要求处理器之间的最小通信要求最小通信的基本原理不应被认为是文献中通常提到的网络延迟，而是上下文切换。这是因为处理器必须暂时停止可盈利的定点计算，以处理不可避免的消息传递，通常涉及硬件中断和操作系统级别的上下文切换在扩展KRONOS时，我们保留了控制图的显式表示和时钟值的符号表示虽然该领域的大多数工作都使用了控制图的on-the-docky结构和其节点（位置）的哈希函数，该函数试图平衡处理之间的负载节点，我们引入了一个先验控制图划分，它的第一个版本是基于工具METIS[15]。如果m是边数，则METISBRABERMAN，OLIVERO和 SCHAPACHNIK4使用O（m）启发式方法来处理寻找最小割的NP完全虽然控制图的在线构造更吸引人，特别是当可达节点是控制位置的一个小子集时，或者当错误位置实际上是可达的时，我们相信，在可行的情况下，使用整个控制图可能比在线构造更有优势6：• 它建立了一个合适的测试床，以实验不同的图划分策略。当前版本大大减少了跨越处理器边界的边缘数量，从而最大限度地减少了通信需求，从而减少了上下文切换。• 它建立了一个合适的框架，动态节点重新分配时，由于处理器处理的符号区域的数量上的巨大差异，负载平衡受到损害虽然当前版本不具备在处理器之间迁移位置的能力，但它被视为一条非常有前途的研究路径（更多信息请参见第5节）。• 扩展到完整的TCTL很容易实现以下KRONOS算法。• 只要模型的时间约束发生变化，就可以进行分布分区和配置重用。另外两个策略也被用来帮助减少处理节点之间的消息交换。一个可以在很大程度上提高性能的重要决策是使用推送模式，其中节点向彼此发送它们将需要的区域，或者使用轮询模式，其中节点在需要时显式请求区域。我们的第一个决定是使用基于消息捎带的混合策略处理节点的行为基本上与轮询模式相同，但当处理器A需要位于另一个处理器B中的区域时，它将请求B的所有A这种机制应该减少通信开销，因为交换的为了进一步减少通信，状态机确定处理节点是否真的需要请求区域。它有三种可能的模式：“Low regions-demand, busy processing node”“High regions-demand, idle processing node”6即，当控制位置的图形与所涉及的DBM的数量相比并不巨大时。BRABERMAN，OLIVERO和 SCHAPACHNIK5：协调员C/DC/D胶囊胶囊：迭代器DCC：负载评估器D：固定点发动机：助手DK：连接器：连接器DD：储存D：偏远地区C/DDD：路由存储D**D*：地方区域存储：Delta蓄能器：Embassys图二. ZEUSarchitecture.“High regions-demand, busy processing node” 处理节点还没有空闲，但是启发式算法7预测它很快就会空闲，因此它的请求被无延迟地发送。为了处理所有这些设计考虑，构建了如图2所示的架构其明显的复杂性服从于一个关键的设计决策：关注点分离该架构应该作为一个试验台，用于试验有关同步、区域通信和负载平衡的一系列设计决策。因此，我们的目标是一个松散耦合的解决方案，其中固定点计算和轮询或推送模式的使用等问题尽可能独立。这一策略使我们识别出映射到不同组件的某些方面。从体系结构的角度来看，胶囊是与处理节点相关联的一组组件每个分区被分配给一个处理节点。胶囊的定点引擎负责为关联分区计算可以到达目标状态的状态集。该架构背后的一个关键思想是向定点引擎隐藏存在分布的事实。为了实现这一点，存储组件被细化为几个部分：路由器组件负责隐藏7试探法是确定每次迭代改变的区域数量减少到特定阈值以下。BRABERMAN，OLIVERO和 SCHAPACHNIK6每个位置都被分配到胶囊。在定点计算期间，如果定点引擎需要读取分配给同一胶囊的区域，则路由器将请求定向到本地区域如果位置位于另一个胶囊中，则将向相应的大使馆请求其相关区域。在每个胶囊内，每个相邻胶囊都有一个大使馆。 当请求提供一个区域时，如果他们有一些“新”区域要提供，他们会立即回答。当没有新的信息到达时，它们将请求转发到连接器，要求它向对应的胶囊。当新区域到达时，它们在下一次迭代中对定点引擎可见胶囊A具有连接器A、B，其中在A中的位置与B中的位置之间存在至少一个边缘。连接器处理网络通信，但也负责决定何时将请求实际发送到网络，从而实现延迟消息传递策略。为了做出该决定，他们查询负载评估器组件，并且如果胶囊处于“低区域需求”状态则事实上，请求转发仅在胶囊处于“高区域需求”并且没有应答挂起时在这种情况下，必须进行捎带，因此连接器将目标封装器感兴趣的每个未发送区域附加到请求（增量累加器在此起作用，稍后解释）。接收连接器立即响应请求，而不管它们自己的胶囊区域的需求。增量封装器充当由定点引擎生成的所有新区域的存储库，这些区域最终必须对其他封装器可见。同样，固定点引擎并不知道增量缓存的存在;路由器的工作是保证写入的本地区域也到达那里。显然，负载评估器组件负责确定胶囊是否空闲以及其区域需求是高还是低。助手执行数据表示压缩（即，如果可能的话，表示具有较少数量的DBM的区域）。 在本地存储库和增量累加器中应用压缩。 这导致了“语义上无害”的死时间利用率，有望使未来的计算和消息传递变得更轻。迭代器负责确定控制流是位于定点引擎组件还是位于帮助器组件。协调员负责启动验证，包括胶囊间的分离管理和工作分配。在模型检查阶段，协调器偶尔从capsules接收8由于技术原因，特别注意向属于同一固定点引擎迭代的每个请求展示相同的信息。BRABERMAN，OLIVERO和 SCHAPACHNIK7→我我我我X我我x1，.，xn我我 1nα关于本地定点存在的信息和用于估计通过网络传输的消息因此，协调器是检测已经到达定点或初始状态的组件对于感兴趣的读者，更详细的描述的架构被列为附录5。3.1正确性证明的草图为了避免一大步，我们没有直接证明ZEUS的正确性，而是逐步证明了更类似于KRONOS架构的中间版本的正确性（见图3）。其中两个是特别感兴趣的：第一个是我们所谓的“朴素分布”，它引入了对远程信息的非常简单的同步访问的分布，第二个包括引入复杂的为了证明它们是正确的，我们遵循分布式算法证明中的一个常见策略，将演示分为两部分：（a）描述的半算法收敛到最小定点，以及（b）协调器最终将在定点发生时检测到定点。为了解决第一个问题，我们求助于Cousot [7]提出的“异步迭代”概念定义3.1异步迭代设（P，±）是完备格，n是正整数，F：PnPn是单调算子.设δ∈ Ord是IN n={1，…，n}，使得：a）（<$δ∈Ord）（<$i∈INn）（（<$α≥δ）（i=cα））令τδ：δ∈Ordτ是Ordn的元素序列，使得：b）（i∈INn）（δ∈Ord）（τδ δ）c）（<$δ∈Ord）（<$i∈INn）（<$β≥δ）（（<$α≥β）（δ≤τ）d) （<$β，δ∈Ord）（（β为极限序数<$β δ）=<$（（<$i∈ INn）（β≤τδ）算子F与序列<$cδ的异步迭代：δ∈Ord和τδ：δ∈Ord，从D∈Pn开始，定义如下：x0=Dxδ=xδ−1后继序数δi/=cxδ=F（ττδ）后继序数δi=cδx δ=.δJδJ≤δi极限序数δ文[7]证明了异步迭代是平稳序列，其极限确实是从D出发的算子F的最小不动点。δδBRABERMAN，OLIVERO和 SCHAPACHNIK8：定点引擎D：区域：协调员C/DC/D：固定点发动机：固定点发动机DDDD：区域：区域C/DC/D：迭代CCCC：固定点发动机：助手：固定点发动机：助手DDDD：区域：迭代器：协调员：区域(a) 步骤0（KRONOS）.(b) 步骤1（(c) 步骤2.C/DC/DCC：固定点发动机DD DDD*D：Delta累积的：连接器：连接器：区域*：助手：迭代器：协调员：协调员C/DC/D：迭代器DCC：加载阿塞索河D：固定点发动机：助手D：连接器：连接器DD：偏远地区DD存储*：C/DD：路由*DD：地方区域斯托拉格河：Delta累积的*(d) 步骤3.（e）步骤4。图三. 架构进化。也就是说，异步迭代提供了一种迭代计算模型，它保证如果满足某些假设，那么即使计算不遵循定点迭代演算的标准顺序，也会达到最小定点。特别地，在由该模型描述的计算期间，可以使用来自不同的过去时刻的数据。这是分布式计算中出现的一种现象，在分布式计算中，给定演算中使用的远程数据当然，其他一些假设也应该成立，比如计算的公平性（3.1.a）。粗略地说，在非平凡的要求中，有一个要求，即在给定的处理节点上在给定的时间点产生的信息最终将可用于依赖于它的任何其他远程演算（3.1.c）。例如，为了证明这些要求适用于ZEUS，我们证明了（a）局部固定点必然会发生，（b）因此(d)更新的信息将作为答案返回正确性的充分证明可以在[19]中找到。BRABERMAN，OLIVERO和 SCHAPACHNIK9t1fx3.2实施说明ZEUS它使用TCP/IP套接字进行进程间通信，并包装在一个通信库中。它分别依赖于KRONOS和METIS库进行DBM计算和位置分布。它可以在大多数Unix平台上运行。4初步实验结果我们作为指导案例研究的例子是文献中常见的火车门控制器版本控制器记录列车的状态，并相应地在门上启动要评估的属性（表示为观察者的可达性问题）是列车是否可以在闸门打开或刚刚关闭时进入铁路道口表1：TGC案例研究的规模。#自动机#地点#转换#时钟每列车331栅极4101控制器（5列）182051控制器（6列）212801观察员5221组成（5列）4764278508组成（6列）14388902629我们将ttx定义为使用x个处理器运行验证的总挂钟时间，tcx为将自动机和相关信息复制到所有处理器所需的时间，tix为总空闲时间（在所有参与者胶囊上）。我们做了区分，因为复制过程是次优的，可以增强。加速函数Sx定义如下：fx=（ttx−tcx）Sx=1fx表示使用x个处理器完成运行所需的时间，与仅使用一个处理器相比。可以看出，我们认为线性加速是理想的。在我们的第一个实验中，在由10个BRABERMAN，OLIVERO和 SCHAPACHNIK10例如环境#procsttx（秒）tcx（秒）fx×100%SXTGC5，达尔文14050百分百1可达27724百分之十三点零九7.64目标状态313048百分之二十点二五4.94迅速12480百分百122519.68%10.333129151.61%1.944373百分之十三点七一7.295202380.24%1.256285百分之九点二七10.78TGC5，达尔文18890百分百1不可达2515525577.07%0.17目标状态3362549402.25%0.25TGC6，达尔文1∞N/AN/AN/A可达2∞N/AN/AN/A目标状态3320146N/AN/A迅速1∞N/AN/AN/A2∞N/AN/AN/A3∞N/AN/AN/A4919974百分百4516077716.63%6.0161659103百分之十六点九一5.91表2 TGC的结果。节点9，并在硅图形IP27与四个270兆赫处理器10和1千兆内存运行IRIX 646.5，我们确实能够处理更大的问题比单处理器版本。此外，在许多情况下，我们还获得了重要的加速（见表2）。但是，在某些情况下，当我们增加处理器数量时，性能会考虑到这些不令人满意的结果，我们决定重新聚焦实验分析快速编码不同通信策略的灵活性：宙斯允许我们• 原始的伪轮询模式，其中胶囊在具有“高区域需求”时• 一种推送模式，其中节点将它们生成的区域发送给其他节点，9个都有64 Mb内存，Linux 2.2.15- 4 mdk内核，5个有Pentium III733 Mhz处理器和其他5个与AMD速龙940 Mhz通过100 Mbps的以太网网络连接。其中只有六个可用。由于群集上的处理器速度不同，因此首先使用更快的处理器，以避免将加速分配给某些配置，因为引入了更快的处理器。10其中只有三个可用。BRABERMAN，OLIVERO和 SCHAPACHNIK11需要他们毫不拖延。该模型类似于分布式可达性图探索中使用的模型[20]。• 订阅架构。这是伪轮询模式的变体，它消除了许多不需要的消息。当来自一个capsule的两个连续请求都无法带回信息时，请求源和目标capsule之间就会发生订阅这意味着不会发出新的请求，以避免重新编写目标。当目标生成新的区域时，它将它们发送给订阅的请求者，就像在推送模式中一样我们还使用了几种分区策略来改善负载平衡：• 最小切割：使用METIS，如前所述• TL-加权最小切割：使用METIS特征将权重信息添加地点与属性要达到的重量十倍正常重量11.• OpL加权最小切割：使用METIS特征将权重信息添加到位置。该信息来自关于在单处理器上的先前验证期间在每个位置12中操作的凸部的我们的想法是看看一个所谓的好分布在验证时间内是如何实现的。• 随机分布：控制节点的均匀分布，没有局部保留。新一组实验的目标是获得关于一些识别出的关键问题是如何在总的时间内被解决的答案：帽之间的位置分布，通信策略和符号状态空间表示碎片化。我们记录了几个指标，最有意义的指标是：每个胶囊的空闲时间、每个胶囊的I/O时间、定点引擎时间（表中称为”表中）。作为衡量负载平衡的指标，我们采用了一个需要时间的操作，例如符号状态之间的差异（参见算法1的第10然后，我们为每个节点累加表示要操作的符号状态的凸数的乘积（这是有意义的，因为对于给定的时钟集，这个乘积近似地决定了操作的计算复杂度）。我们将此指标称为“#ops”。在桌子上。看看实验数据，有一个特别糟糕的情况，它出现在两个处理器上，其中90%的工作似乎落在一个胶囊中。毫无疑问，在平衡方面存在问题，但人们会期望时间与单处理器版本相似，但它们几乎差了七倍早期的实验表明，主要问题并不是11TL是Target Locations的缩写。12OpL是Operations per Location的缩写。BRABERMAN，OLIVERO和 SCHAPACHNIK12I/O，见表4。我们决定在Silicon Graphics机器上运行实验，以便轻松推理并精确定位每个胶囊上发生的事情。这些实验并不意味着是结论性的，因为我们只使用一个例子和少量的处理器。然而，一些现象可能会警告我们，向后计算的并行化是一项重要的任务。以下结果是在具有不可达的“ER-ROR”状态的TGC 5上获得的我们观察到订阅模式的性能总是比原始的伪轮询模式好一点，因此我们选择只报告该模式和推送策略。另一方面，我们没有报告新的结果的基础上纯粹的最小割，因为加权版本似乎表现得更好。此外，正如预期的那样，位置的随机分布表现非常糟糕，并且示例没有在4小时的挂钟时间内完成不幸的是，该工具的当前版本仅在完成后才记录指标，因此我们无法显示数据。让我们补充一下，胶囊0的I/O时间还包括协调器的I/O，因为在当前版本中，协调器驻留在该胶囊中。我们按照分区策略来构造数据。随着每个表，我们提供了不同版本如何执行的部分结论。表3：TGC5的结果，不可达目标状态，单处理器版本。1处理器章0tt（s）tc（s）ti（s）88800空闲时间（s）fpe时的时间（s）I/O#请求rcvd#ops.0868003273740TL-加权最小割就工作量分配而言，分区显然不能令人满意。虽然订阅的性能优于推送，但性能的下降是不可忽视的。单处理器版本由于（可能的）碎片问题而引人注目正如[6]和[4]所报告的那样，在定点计算期间改变评估顺序可能会加剧区域表示中的碎片化（即，代表一个区域所需的凸的数量请注意，操作数量增加，而I/O时间几乎没有影响。见表4。所有的运行似乎都表明，推送策略存在一些问题，除了总挂钟时间之外，我们目前的指标还没有捕捉到这些问题。BRABERMAN，OLIVERO和 SCHAPACHNIK13表4：TGC5、不可达目标状态、TL加权最小切割划分的结果。Comm.strategie2处理器3个处理器次tt（s）tc（s）ti（s）tt（s）tc（s）ti临时票据tion29622429142041493944空闲时间I/O#请求#ops.空闲时间I/O#请求#ops.时间在FPE（个）rcvd时间在FPE（个）rcvd（个）（个）（个）（个）章029143751257341971355667793章102916028596123019941177905481章219730533942推tt（s）tc（s）ti（s）tt（s）tc（s）ti52712452222194494244空闲时间I/O#请求#ops.空闲时间I/O#请求#ops.时间在FPE（个）13岁时间在FPE（个）rcvd（个）（个）（个）（个）章0522231465525734211837413269306章105225074885675740214903848303893章221260742942OpL加权最小割在这种情况下，我们在工作负载分配方面获得了更好的结果，正如我们预期的那样。因此，信息交流增加了。碎片化仍然存在，并解释了为什么时间没有减少。monoprocessor版本一个令人不快的事实是，订阅模式和推送模式都没有用3个处理器完成。一个可能的解释是分裂问题的加剧。见表5。表5：TGC5、不可达目标状态、OpL加权最小切割分割的结果。Comm.strategie2处理器3个处理器订阅tt（s）tc（s）ti（s）tt（s）tc（s）ti1650241111∞N/AN/A空闲时间（s）fpe时的时间I/O#请求rcvd#ops.空闲时间（s）FPE时间（个）I/O#请求rcvd#ops.章0111049410232293082章11155855122949683章2推tt（s）tc（s）ti（s）tt（s）tc（s）ti4252244077∞N/AN/A空闲时间（s）fpe时的时间I/O#请求rcvd#ops.空闲时间（s）FPE时间（个）I/O#请求rcvd#ops.章0407711691748704244章10420706663962755章2BRABERMAN，OLIVERO和 SCHAPACHNIK1413请注意，当使用推策略“#req.“randomBRABERMAN，OLIVERO和 SCHAPACHNIK15从表4和表5中可以看出，通信策略并不影响实验的结果，这可能是因为示例很小，并且在单个机器上通信时不涉及硬件中断。必须指出的是，前面提到的指标（每个位置的操作数）和时间结果之间似乎有直接的关系为了减轻碎片化问题，我们决定应用保守的抽象，包括当一个区域将被传输到另一个胶囊时应用凸包。在下面的文章中，我们将报告几个使用这个想法的实验。OpL加权最小割，使用凸包每个区域只传输一个凸函数可以减少订阅模式的挂钟时间，但仍然有太多的空闲时间。推模式的性能是远远不能令人满意的，我们没有解释的现象，使用提出的指标。见表6。表6：使用凸包的TGC5、不可达目标状态、OpL加权最小切割分割的结果。Comm.strategie2处理器3个处理器次tt（s）tc（s）ti（s）tt（s）tc（s）ti临时票据tion93224893992491673空闲时间I/O#请求#ops.空闲时间I/O#请求#ops.时间在FPE（个）rcvd时间在FPE（个）rcvd（个）（个）（个）（个）章04943941710563027631621226313815章13994883481593391038146147286章209230451204280推tt（s）tc（s）ti（s）tt（s）tc（s）ti3602243288730491152空闲时间I/O#请求#ops.空闲时间I/O#请求#ops.时间在FPE（个）rcvd时间在FPE（个）rcvd（个）（个）（个）（个）章032882716773075388047418911485246701章10355706732743298678813709151443章2066104801021703TL-加权最小割，使用凸包在这种情况下，我们有三个处理器的情况下非常好的结果，并令人惊讶的是，有两个性能差。这表明，在胶囊之间发送更简单的区域或改善工作负载分布的策略无法解决碎片化问题。 这种现象似乎更复杂，可能取决于区域的到达时间或我们尚未确定的划分策略的特征。见表7。1313也没有完成在4挂钟小时。BRABERMAN，OLIVERO和 SCHAPACHNIK16表7：使用凸包的TGC5、不可达目标状态、TL加权最小割分割的结果。Comm.策略2处理器3个处理器次tt（s）tc（s）ti（s）tt（s）tc（s）ti临时票据tion486124481545249766空闲时间I/O#请求#ops.空闲时间I/O#请求#ops.时间在FPE（个）rcvd时间在FPE（个）rcvd（个）（个）（个）（个）章048153120125734382210421662章104816021110551804070152310121章23840103942推tt（s）tc（s）ti（s）tt（s）tc（s）ti483324478952749913空闲时间I/O#请求#ops.空闲时间I/O#请求#ops.时间在FPE（个）rcvd时间在FPE（个）rcvd（个）（个）（个）（个）章04798313612573445621412122121章10479903311105518048003632510605章245701729425结论和未来工作ZEUS是一个基于KRONOS工具的分布式时间模型，它使用软件架构进行了描述和证明。据作者所知，它是第一个用于时间系统的分布式模型基于向后可达性计算。它被认为是一个广泛的设计决策，如通信模式或同步类型的测试平台。我们对异步版本的初步结果，虽然在某些情况下显示出有希望的加速，但令人惊讶的是违反直觉，但证明了需要一个开放的架构来测试替代概念。在某些情况下看到的不规则行为可能与数据结构对操作顺序的敏感性有关一方面，最好在一个胶囊里尽可能多地做本地工作，而不与其他人交流直觉告诉我们，这种异步策略的优点是：（a）很好地利用了并行处理资源，（b）避免了区域的早期传播，这些区域最终将被包含到另一个区域中，从而减少了传播的次数。另一方面，当通信发生时，这可能导致在具有大量凸部的“成熟”区域之间的操作此外，广度优先遍历不受欢迎（据报道，这是避免碎片化的好策略[4]）。应该做更多的研究来深入了解这些现象，并提出解决方案的并行设置。这可能需要开发专门的可视化技术，这是我们目前正在研究的。今后要探讨的一个方向是，从代表某一区域所需的凸点数目的意义上提高区域的代表性我们目前正在探索的另一个研究方向是开发ZEUS的同步版本，试图模仿KRONOS在顺序版本中应用操作符更准确地说，这个版本BRABERMAN，OLIVERO和 SCHAPACHNIK17将在每个胶囊上同步应用每个定点迭代。虽然它失去了潜在的并行性，但它可能会使区域操作的数量接近KRONOS在单处理器上执行的操作。因此，如果实现了良好的负载平衡，这种策略可能会带来重要的加速。我们还相信，动态平衡最终可以应用于更好地利用分布式资源。幸运的是，ZEUS架构似乎是一个有吸引力的起点，在相邻的胶囊之间进行位置迁移，以寻求更好的负载平衡。 这可以作为架构重新配置来完成，其中在处理胶囊之间建立新的链接。自然的下一步是扩展泽乌斯为了处理完整的TCTL，主要是通过调整KRONOS策略来适应分布式环境。此外，我们认为，如果需要的话，向前计算可以很容易地结合到这种情况中。获得反例迹线也是相关的领域或研究（例如，[4]）。致谢我们要感谢Sergio Yovine为我们提供了KRONOS库引用[1] 巴尔河，C. Courcoubetis和D. L. Dill，Model Checking in Dense Real-Time，Information and Computation104（1993），pp. 2-34网址http://citeseer.nj.nec.com/alur93modelchecking.html[2] 巴尔河和D. L. Dill，A theory of timed automata，Theoretical ComputerScience126（1994），pp. 183-235网址http://citeseer.nj.nec.com/alur94theory.html[3] 巴拉特，J。，L. 我和J。 Str′brna′，SPIN中的Distribut edLTLmodel-checking，in：SPIN，2001，pp. 200-216网址http：//citeseer.nj.nec.com/article/barnat00distributed.html[4] Behrmann，G.，T. Hune和F. W. Vaandrager，Distributing timed modelchecking-how the search order matters，in：Computer Aided Verification，LNCS1855（2000）。216-231URLhttp://citeseer.nj.nec.com/behrmann00distributing.html[5] 本-大卫，S.，T. Heyman，O. Grumberg和A. Schuster，Scalable distributedon-the-chromatic symbolic model checking，in：Formal Methods in Computer-Aided Design，2000，pp. 390-404网址http://citeseer.nj.nec.com/326863.html[6] Braberman，V.、C.Lo'pezPombondA.Olivero，Onimprvingbackwardsverification for timed automata ， in ： TPTS 2002 ，BRABERMAN，OLIVERO和 SCHAPACHNIK18satellite event for the JointBRABERMAN，OLIVERO和 SCHAPACHNIK19欧洲软件理论与实践会议，ETAPS 2002，ENTCS65（2002）。网址http://www.elsevier.com/locate/entcs/volume65.html[7] Cousot ， P. ， “Methodes Iteratives de Construction et D'Approximation dePoints Fixes D'Operateurs Monotones sur un Treillis，Analyse Semantique desProgrammes，”Phd.thehesis，UniveresitéeSciéntifiquetMéedicaledeGrenoble，InstitutNationalPolytechnique de Grenoble（1978）.[8] 道斯角，A. Olivero，S.Tripakis和S.Yovine，工具KRONOS，在：Proceedings of Hybrid Systems III，LNCS1066（1996），pp. 208-219[9] 道斯角和S. Yovine，使用KRONOS验证多速率时间自动机的两个例子，在：第16届IEEE实时系统研讨会论文集（RTSS六十六比七十五网址http://citeseer.nj.nec.com/daws95two.html[10] Dill，D. L.，有限状态并发系统的时间假设和验证。有限状态系统自动验证方法国际研讨会，LNCS407（1990），pp. 197-212[11] Garavel，H.，R.马提斯库和我M. Smarandache，用于模型检测的并行状态空间构造，在：M。B. 第八届国际SPIN研讨会论文集，多伦多，加拿大，2001年，页. 217-234网址http://citeseer.nj.nec.com/474094.html[12] Grumberg ， O. ， T. Heyman 和 A.Schuster ， Distributed symbolic modelcheckingfor µ-calculus ， in ： Computer Aided Verification ， 2001 ， pp.350-362.网址http://citeseer.nj.nec.com/473825.html[13] Henzinger，T.一、X. Nicollin，J. Sifakis和S. Yovine，Symbolic ModelCheckingfor Real-Time Systems，Information and Computation 111（1994），pp. 193-244。[14] Heyman，T.，D.盖斯特岛Grumberg和A.李文，大规模并行电路可达性分析中的可扩展性问题。Grumberg，editor，Computer Aided Verification，12thInternational Conference，LNCS1855（2000），pp. 20-35网址http://citeseer.nj.nec.com/heyman00achieving.html[15] Karypis，G.和V. Kumar，不规则图的并行多级k路划分方案，技术报告，明尼苏达大学计算机科学系/美国陆军HPC研究中心。关闭USA.（1998年）。[16] Lerda，F.和R.陈志华，应用于分散式记忆体模型检测之研究，国立成功大学机械工程研究所硕士论文，（1999）.网址http://citeseer.nj.nec.com/lerda99distributedmemory。HTML[17] M.博兹加岛Maler，A. Pnueli和S. Yovine，时间自动机的符号验证的一些进展，在：O。 Grumberg，编辑，第9届计算机辅助验证国际会议论文集（CAV179比190。网址http://citeseer.nj.nec.com/bozga97some.htmlBRABERMAN，OLIVERO和 SCHAPACHNIK20[18] Ranjan河，桑哈维河Brayton和A. Sangiovanni-Vincentelli，工作站网络上的二进制决策图，在：计算机设计国际会议，1996年，pp.358-364.网址http://citeseer.nj.nec.com/ranjan96binary.html[19] Schapachnik ， F. ， “DistributedandParallelVerificationofReal-Time Systems ， ”Degr e the es is ， De p a r