时间自动机验证技术的改进方法

60简体中文《理论计算机科学电子札记》65卷第6期（2002）网址：http://www.elsevier.nl/locate/entcs/volume65.html8页时间自动机向后验证的改进（扩展摘要）诉 Bra bermana，1，4，C. L'o pez Po m bo a，2，5，A. Oliv erob，3，6a计算机科学系，FCEyN，布宜诺斯艾利斯大学，阿根廷b阿根廷布宜诺斯艾利斯阿根廷企业大学信息技术系摘要时间自动机[2]的验证技术内置于KRONOS[7]等工具中，基于适当算子的定点演算。在这项工作中，我们提出了不同的替代方案来计算固定点，这对收敛所需的迭代1介绍时间自动机[2]的验证技术内置于KRONOS[7]等工具中，基于适当算子的定点演算。 比如说，为了在时间自动机上验证TCTL [1]这样的逻辑，通常需要获得状态集，系统可以从该状态集演化并达到满足公式φ的状态集（真的特征集φ）。 该组可以被描述为一个定点。众所周知，Cousot [6]的混沌迭代结果表明存在许多算法替代来进行这样的演算。在这项工作中，我们探讨了不同的迭代方法来解决问题φ1UIφ2？"，式中φ1和φ2是mulas的TCTL，I表示达到φ2所用的时间。一方面，我们提出了一种方法，试图减少收敛所需的迭代次数这是通过利用在同一次迭代中获得的中间结果，而不是中间结果1UBACyT资助X156和TW72的研究。2由FOMEC 376奖学金资助的研究3由UADE资助的研究ING 6 -01。4电子邮件地址：vbraber@dc.uba.ar5 电子邮件地址：clpombo@dc.uba.ar6电子邮件地址：aolivero@uade.edu.ar2002年2月出版，电子科学和B。 V. 操作访问根据C CB Y-NC-N D许可证进行。BRABERMAN，LO'PEZPOMBO和OLIVER O61联系我们∼ ∼∈ {≤ ≥}∈像KRONOS中的传统迭代算法一样，以前迭代的结果。另一方面，我们提出了一种局部收敛方法，该方法与[11]类似-在图组件上计算定点，从而避免结果的传播，直到它们局部稳定。我们已经实现了一个原型，这两种策略都是基于KRONOS工具的，我们得到了一些初步的结论。nary实验数据最后，我们比较了这两种替代方案，并提出了可能优于以前实现的组合。2时间自动机时间自动机（TA）[2]已经成为建模和分析时间系统的最广泛使用的形式主义之一，它得到了几个工具的支持（例如，KRONOS[7]，UPPAAL[3]，HY TECH[10]，RED[17]，TREAT[12]，etc.）。 它们已成功地应用于通信协议、实时系统和电路的自动检测。TA是有限自动机，其中时间通过时钟合并作为有限自动机，TA G= S = s1，.，s n，X，E，I由一组有限的节点S（在TA文献中称为位置）和一组边E组成。没有最终地点的概念，因为处决是有限的。当集合X中声明的时钟测量经过的时间时，边缘模型每个边沿都关联有一个定时条件保护是对时钟值的约束，形式为 x其中<，=，>，和n N. 只要一条边的相关保护为真，就可以遍历该边。时间在位置处流逝，并且边遍历是瞬时的，并且相关联的时钟被重置。此外，定时条件通过I与每个位置相关联。这些条件称为不变量，并确定位置的有效时钟值因此，可以使用不变量来表示控件不能在该位置停留超过一定量的时间（即，截止日期）。语义是通过标记的转换系统给出的，其中状态由控制位置和时钟值（正实数）组成，有关更多细节，请参见例如[19]。状态之间有两种转换：时间（与时间的进展有关）和离散（与自动机中的边缘交叉有关）。状态集通常通过某些称为区域的时间谓词来描述（在KRONOS文献中），我们一般表示为φ。在状态上给定一个谓词，我们将满足它的状态集表示为[[]]（的特征集）。将具有到处于a中的状态的时间转变的状态的集合表示为predt（a），并且将通过遍历与边e相关联的离散转变而达到处于a中的状态的状态的集合表示为prede（a）。这两个算子都是区域封闭的。BRABERMAN，LO'PEZPOMBO和OLIVER O62XXX XXXXXX3经典向后验证我们的兴趣在于计算mφ1| U|φ2的计算公式的TCTL，其中φ1，φ2是计算公式的TCT L。 一个状态e长到[[φ1<$UIφ2]]，此时自动机可以通过I中的时间长度的φ 1 -状态的路径演化并到达φ2-状态。在下文中，为了简单起见，我们将自己限制为def公式：在[18]中，它表明，该区域相当于最小固定点：µX。（φtruedX）其中真d是pred t（pred e（）），即是作为在和它的离散前驱的联合中的状态的时间前驱（即，通过离散转变的前驱）的状态的集合。在下面的命题中，我们证明在KRONOS中，定点计算的抽象函数描述。命题3.1（K）给定G=S ={s1，...，s n}，X，E，I是一个定时的 au-tomata和φ =i∈{1，.，n}@= s iφ i一个描述simboli的谓词-cally是一组状态，然后是μ。（φtrued）可以迭代地计算为如下所示：{Xij}（1≤i≤n），（0≤j）Xi0=predt（φi）Xij=Xij−1e∈Eik pred t（pred e（Xkj−1））;对于1 ≤ j。其中Xij是X在迭代次数j处的分量i的值，并且Eik是从si到sk的边的集合。✷4一种减少迭代次数（K†）的方法第一个想法是基于一个简单的观察：为了计算i，j并不总是需要利用在最后一次迭代期间为位置kk，j−1）。 如果该方法采用以下方法，如果位置k已经被处理则在当前迭代中计算的位置k的区域（即，k，j）。”[13]这是一个证明。用Cousot的结果计算方法是正确的。那就是：命题4.1（K）给定G=S ={s1，.，s n}，X，E，I是一个定时的au-tomata和φ =i∈{1，.，n}@= s iφ i一个描述simboli的谓词-计算一组状态，然后是µX。（φtruedX）可以计算如下：{Xij}（1≤i≤n），（0≤j）Xi0=predt（φi）Xij=Xij−1e∈Eikpredt（prede（Xkj−φσ（i，k）;对于1 ≤j.BRABERMAN，LO'PEZPOMBO和OLIVER O63∈∃−简体中文其中φ σ：{1，.， n}× {1，.， n} −→ {0，1}定义为：如果σ（i）> σ（j）φσ（i，j）=如果σ（i）≤σ（j），则为1使得σ Sn（即，σ是对遍历位置的顺序进行建模的置换。 也就是说，该方法对排序不敏感），并且Eik是从si到sk的边的集合。✷在许多应用中，不需要计算公式（如φ）的整个特征集。当我们只对知道系统是否可以从初始状态演化到φ-状态（即，inittrueφ）。 然后，我们引入一个简单的机制，一旦初始状态属于中间组7。事实上，我们将该机制引入到原始的KRONOS实现（表中的K RI列）和我们的修改版本中（K）。我们已经在AMD K7 1333 Mhz 256 Mbytes LINUX 7.2平台上运行了几个案 例 研 究 ： 通 信 协 议 CSMA-CD [15] 、 5 列 列 车 的 铁 路 交 叉 系 统（RCS）[12]、主动结构控制系统版本的新鲜度问题[5][9]、矿井排水设计的有界响应特性[4]和9个车站的FDDI协议[16]。实验数据表明，在所有情况下，迭代次数都减少了，但这种减少并不总是转化为速度的提高，特别是当φ不可达（表3中的K+我们的猜想如下：表示符号状态的数据结构（本质上是一组差分边界）矩阵，DBM [8]或区域）在我们的版本中倾向于对于RCS示例，表1显示了每次迭代后表示计算符号区域所需的区域的K和K。实验表明，我们的算法更适合早期检测（K†列）。这也可以用关于区域成熟的相同猜想来解释。5局部收敛（K部分）当在图上计算定点时，图的拓扑可以提供有用的信息。在[11]中，计算SCC（强连通分量）以执行不定时系统的两级迭代定点方法当地7.算子d是单调的（例如见[19]）。BRABERMAN，LO'PEZPOMBO和OLIVER O64联系我们迭代次数123456789K的区域数1651662137394650266034645065146514K的区域数†93020995744742777117711---表1RCS示例中每次迭代的区域数比较SCC的收敛从寻求全局稳定的主迭代中调用。该策略背后的想法是避免中间结果的传播，直到结果局部稳定。 我们在[13]中还表明，Cousot论文的理论结果命题5.1（K部分）给定G= S = s1，...，s n，X，E，I是一个定时自动机• C ={c1，...，ct}是集合S的一个划分。• {ci：ci∈C}0≤i是C的无限元素序列，使得（ni）（1≤i≤t <$（nj）（j∈N<$（nk）（j≤k <$ci=ck）且φ =i∈{1，...，n}@= s i <$φ i一个简单地表征a的谓词一组状态，然后是µX。（φtruedX）可以计算为：{Xij}（1≤i≤n），（0≤j）Xi0=<$φi<$Xij−1;ifsi∈/cj。Xij=0predt（Xij−1）<$e∈Eikpredt（prede（Xkj−1））;ifi∈c j.其中Eik是从si到sk的边的集合。✷它仍然是有效地获得节点集合C的合理划分的问题。一种替代方法是按照[11]中的方法计算SCC。然而，下面的观察使我们找到了一个更简单，在许多情况下更实用的解决方案。安全性和活性需求通常通过虚拟组件（观察者）与被分析系统（SUA）并行组成。因此，如果我们根据观察者的局部位置来划分粒子合成的节点集，我们将得到由最大SCC集所符合的合理划分。此外，由于在许多情况下观察者可以是非循环的[4]，如果组件是拓扑有序的，那么只有一个全局迭代是真正必要的。初步实验表明，在φ所表征的集合不可达的情况下，该策略可能导致验证时间（K部分）的重要改进BRABERMAN，LO'PEZPOMBO和OLIVER O65简体中文简体中文可达性：正确方法→KK−RIK<$−RIK部分示例↓秒ITER秒ITER秒ITER秒ITER有界195.302518.201017.10386.6067RCS⊥-0.91100.211⊥-CSMA/CD215.72850.1730.191218.20100新鲜⊥-1,6441639.683⊥-FDDI26.692827.39282.612171.7670表2不同方法验证时间和迭代次数的比较可达性：假方法→KK−RIK<$−RIK部分示例↓秒ITER秒ITER秒ITER秒ITER有界91.132289.582291.52929.7065RCS3.1093.00923.3061.3319CSMA/CD0.3780.3680.3550.3718新鲜11,8802211,91822⊥-1,49043FDDI⊥-8.72212.591⊥-表3不同方法验证时间和迭代次数的比较列）。请注意，迭代次数增加了，但这些迭代并不涉及所有位置。目前正在进行的工作是使用一种用于图分区的工具，如METI S[14]来计算合适的分区。6今后工作我们目前正在研究一种很有希望的两种迭代方法的组合，以便像处理init那样处理TCTL公式φ1Iφ2（该片段的例子是非zeno公式[19]）。利用METI S工具生成的控制图的某些划分，应用局部收敛性计算集合φ1和φ2然后，应用第4节中解释的早期检测算法来发现初始状态 在[[φ1]中的可能的sIφ2]]。我们希望加快速度，并获得更多关于数据结构如何影响抽象的见解对定点计算的改进。BRABERMAN，LO'PEZPOMBO和OLIVER O66引用[1] 巴尔河，C. Courcoubetis和D. Dill，Model-Checking for Real-Time Systems，Information and Computation，Vol.104，不。1，2-34，1993.[2] 巴尔河，和D. Dill，A Theory of Timed Automata，Theoretical ComputerScience，vol. 126，1994，183-235.[3] Bengtsson，J.，K.G. Larsen，F. Larsson，P. Pettersson，and W.李文龙，一个实时系统自动验证的工具套件，混合系统III，计算机科学讲义1066，Springer Verlag，1996，232-243。[4] Braberman ， V. ， “ 建 模 和 检 查 实 时 系 统 设 计 ” ， 博 士 。 论 文 ，DepartamentoodeComputaci'on，Uni versidaddeBuenosAires，2000年。[5] Braberman，V.，D. Garbervetsky和A. Olivero，使用信息改进时间系统的验证。出现在2002年的TACAS。也可作为技术报告TR 2001 -003获得。CSDepartmen t，FCEyN，Universidad de Buenos Aires.网址：http://www.dc.uba.ar/people/exclusivos/vbraber/tr01-003.ps。[6] Cousot，P.，“Methodes Iteratives de Construction et D'Approximation dePoints Fixes D'Operateurs Monotones sur un Treillis，Analyse Semantiquedes Programmes”. 博士 Grenoble国立综合理工学院Grenoble国立综合理工学院，1978年。[7] 道斯角，A. Olivero，S. Tripakis和S.陈文辉，混合动力系统的研究与应用，国立成功大学机械工程研究所硕士论文，2000。[8] Dill，D.，时序假设和验证的并行系统，在自动验证方法的研讨会论文集并行系统，计算机科学讲义407，施普林格出版社，197-212，1989年。[9] Elseaidy，W.，R. Cleaveland和J.Baugh Jr.，结构控制系统的建模与仿真，计算机程序设计科学，29（1-2）：99-122，1997年7月。[10] Henzinger，T.一、P-H Ho和H.王台HyTech：a model checker for hybridsystems，Software Tools for Technology Transfer 1：110-122，1997.[11] Kerbrat，A.，Lotos程序的可达状态空间分析，第七届分布式系统和通信协议形式描述技术国际会议，瑞士伯尔尼，1994年10月。[12] 康岛，I. Lee和Y. S.金，一种用于实时系统分析的有效空间生成，在软件测试和分析国际研讨会论文集，1996年。在Trans.软件工程，1999年。BRABERMAN，LO'PEZPOMBO和OLIVER O67[13] Lo'pezPo mboC. G.，“Mejoras a un algoritmo de mo del c he c king sim bo 'lico ， basadas en la to po olo g' ıa de los sistemas de tiempo real”.计 算 机 科 学 学 士 学 位 论 文 。 DepartamentoodeComputaci'on ，Facultaddecienciasexactasy naturales，Universidad de Buenos Aires，2001.[14] Karypis，G.，和V. KumarMultilevel Algorithms for Multi-Constraint GraphPartitioning Proceedings of 10th Supercomputing Conference，1998。[15] Nicollin，X.， J. Sifakis和S. Yovine，编译实时规范到扩展自动机，IEEE软。工程师：实时系统专刊，第18卷，第9页。794-804，1992年9月。[16] S. Tripakis“L'Analyse F ormelle des Syste m ` es T em p ori s ′ esen Practique”，Phd. Thesis，Uni vesi t'eJosephF.，Dece mber1998.[17] 王福，RED：具有时钟限制图的时间自动机的模型验证，第二届时间关键系统模型研讨会，2001。发表在《理论计算机科学电子笔记》上[18] 尤 文 ， S. ， “M 'eth o des et Outils p our la V' erification Sy m bolique de Syste m 'es T em p ori s' es ， ”Ph.D. Thesis ， InstitutNational Polyte chnique de Grenoble，1993.[19] Yovine，S.，模型检测时间自动机，嵌入式系统，G. Rozemberg和F. Vaandrager编辑，计算机科学讲义，施普林格出版社，卷。1494年，1998年10月