《理论计算机科学电子笔记》160（2006）97-111www.elsevier.com/locate/entcsτ-模拟对时间系统增量建模的贡献FrancoiseBEllegarde1L IFC-LAB. d雅克·朱利安2号L IFC-LAB. d哈桑·蒙塔西尔3L IFC-LAB. d艾米莉·乌多4L IFC-LAB. d摘要我们感兴趣的是在时间系统的增量建模过程中保持线性时间属性我们考虑在合成框架中由时间自动机建模的时间系统。它们的要求由逻辑形式主义MITL（度量区间时间逻辑）来表达。我们建议使用τ-模拟作为在增量建模过程中保留这些属性的一种方法，即组件集成或改进。我们在时间自动机的语义学上建立了τ-模拟关系，以处理生命性属性的守恒。此外，我们实现了一个工具来验证这样的τ-模拟，基于OPEN-KRONOS库，并使用PROFOUNDER工具。关键词：τ-仿真、增量建模、时间系统、守恒、线性时间属性1电子邮件地址：bellegar@lifc.univ-fcomte.fr2电子邮件地址：julliand@lifc.univ-fcomte.fr3电子邮件地址：mountass@lifc.univ-fcomte.fr4电子邮件地址：oudot@lifc.univ-fcomte.fr1571-0661 © 2006爱思唯尔B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2006.05.01798F. 贝勒加德等人。理论计算机科学电子笔记160（2006）971动机虽然模型检查很有吸引力，但已知它是一种难以应用于大型系统的验证方法。这是由于使用该方法时出现所谓的状态空间爆炸问题。由于时钟的存在，这个问题在很大程度上集中在时间系统中，时钟是模拟时间流逝的变量。对定时系统建模的一种广泛使用的方法是使用组件。也就是说，系统的每个元素被建模为一个组件，并且通过使所有组件的并行组合，感谢一些并行组合运算符，获得完整的系统必须在系统上保持的要求然后在组件系统上进行验证，组件系统通常具有大量的状态，并且在这些状态上，模型检查可能难以应用。一种方法是利用系统的建模过程。然而，一些要求可能只涉及系统的几个组件，如果不是一个的话。因此，仅在这些组件上而不是在整个系统上验证这些要求似乎是有吸引力的。通过集成组件或通过微调实现的增量建模可能是这种重构的一个问题。验证可以在建模的每个步骤中执行，其中系统的大小小到足以应用模型检查。但是，如果在构建过程中验证的属性仍然保留在整个系统上，则此框架适用。我们建议使用τ-模拟来保证线性时间的保存。属性。模拟非常适合系统的增量建模，因为它们保留了安全属性。为了处理生存性性质和部分有界响应性质，有必要使用发散敏感的τ模拟。这种模拟已经被用于在非定时系统的情况下的增量建模例如，我们可以引用B事件系统的情况。[1]在那里，精炼被视为τ-模拟。在本文中，我们提出了一个适用于定时系统的定时τ-模拟，并表明，在非定时情况下，该模拟适用于使用经典的并行合成算子。||.也就是说，如果A和B是两个分量，则A||B τ-模拟物A。更重要的是，τ-模拟是一个w.r.t.全等||Cτ-模拟物B||C.||C.我们还完成了一个发散敏感的定时τ模拟，并证明它保留了逻辑MITL（度量区间时间逻辑）中表达的所有要求。本文的结构如下：在第2节中，我们回顾了我们用于时间系统的模型（即时间自动机）和时间系统的墨水思维模型的一些背景。我们还提出了我们用来指定系统的时间要求的逻辑形式，即，米特尔。然后，在第3节中，我们提出了我们为定时系统提出的τ-模拟关系，一个经典的保持安全性的关系，和一个发散敏感的关系来处理生存性的性质。在第4节中，我们证明了后面的内容保留了MITL中表达的所有属性。第5节回顾了时间自动机实现中的一些问题，特别是我们使用的符号表示，并讨论了验证模拟的方法。最后，第6节包含结论并计划未来的工作。F. 贝勒加德等人。理论计算机科学电子笔记160（2006）97992背景2.1定时自动机自Alur和Dill引入以来，时间自动机是研究最多的连续时间系统模型之一。这些是由称为时钟的实值变量扩展的有限自动机，模拟时间流逝。我们把非负实数R+的集合看作时间域。时钟值。让X成为一组时钟。 时钟值是v：X→R+的映射，为X中的每个时钟分配一个真实值。 我们注意到v（x）是时钟x的赋值，0是将0分配给X中每个时钟的赋值。估值操作。 设δ>R+，则值v+δ是将δ加到每个时钟的值上的值v我们还使用了[11]中结束的限维投影的操作。给定X的时钟Y的子集，以及X上的值v，v在Y上的限维投影，写为v Y，是仅包含v中的值与v中的时钟相关的新值。Y.评估[Y：= 0]v（重置操作）是通过将Y中的所有时钟设置为零，并保持其他时钟的值不变而从v获得的评估。时钟约束和多面体。C（X）组时钟约束由语法定义：g：：= x ^c |g × g|真，其中x> X，c>N，且{<，≤，=，≥，>}。形式为x~c的约束称为原子约束。我们说，一个估价v满足这样一个约束x~c，写v|= x~c或v›x~c if v（x）~ c（非原子约束的满足像往常一样是有限的）注意，一个时钟约束在一组X个时钟上，这些时钟终止于一个凸X-多面体。在本文的其余部分，我们为以x≥ Xx= 0结尾的X-多面体写零和真的X-多面体由x> x>x≥ 0。多面体上的操作。 重置操作和尺寸限制投影在评估上确定的范围可以直接扩展到多面体。 一个X-多面体从一个X-多面体到另一个X-多面体（ζ= vJ奏效（ζ if δ÷ R+·vJ+ δ ÷）的后向对角线投影。多面体上的所有这些操作都保留了凸性。定时自动机（TA）。让命题成为一组原子命题。一个关于Props的时间自动机是一个元组A=0 0→11→2 2F. 贝勒加德等人。理论计算机科学电子笔记160（2006）97101I，时间t的后缀σ t是TSS（q，I−t）ei（q）I−t）ei+1（q）（I -t）···我是我i+1i+1i+2i+2例如。作为一个运行的例子，我们使用了众所周知的铁路穿越时间系统，取自[2]。该系统由至少三个部件组成，即一个或多个列车、一个车门和一个负责车门打开和关闭的控制器。每个组件都配备了自己的时钟。具有一列列车的系统（称为TGC）的预期全局行为如下。在到达铁路交叉口之前，列车向控制器发送接近信号。一次单位（t.u.）稍后，控制器命令关闭进入T.U.的门。然后火车进入十字路口。火车的通过最多持续了三个月。当它在十字路口外时，它向控制器发送一个退出信号，控制器命令打开十字路口内的门。门在最多一个t.u. 稍后。 对每个组件建模的定时自动机如图1所示。每个状态都由名称指定，并且状态内的时钟约束表示状态的不变量。为了便于阅读，省略了不变量和真保护，就像转换时的空重置一样。非常接近C0C1是向上下来方法，{x}x≤5退出x >2，进入x≤5方法，{z}z≤1提高较低，z= 1z≤1退出，{z}在c3中C2向上下来了列车控制门图1. 列车、控制器和车门的定时自动机2.2定时系统度量区间时间逻辑（MITL） [4]是一种指定定时系统的线性时间它可以被看作是PLTL（命题线性时间逻辑）对时间系统的扩展，没有下一个运算符，并且所有其他时间运算符都由具有整数的非奇异区间I约束。边界（单数区间的形式为[a，a]，即，它是关闭的，左和右边界相等。语法。MITL公式可通过以下语法归纳得出：：：= AP |¬ϕ |φ εε|其中ap是原子命题。语义学。MITL公式在TSSσ上解释如下：• σ|=apiffer（σ，0）|=AP（即，p>L（disc（σ（0），• σ|如果它不是真的，那么σ|=，• σ|=φ ρ εiffσ|=φ或σ|= psi，较低，{y}Y11≤y，向上向下y≤2上升，{y}102F. 贝勒加德等人。理论计算机科学电子笔记160（2006）97我1211• σ|= φ U psi对于某个t> I，σt|= psi，且tJ奏效（0，t），σtJ|= φ。其他经典的时间算子可能是有限的：QI =trueUI（偶尔），QI= QI（总是）和1RI2=（（1）UI（2））（释放）。MITL公式在TA上的有效性。我们说MITL公式在TA A上有效，写为A| =，ifρ·（ρ奏效）⇒σ（ρ）|=）。例如。在铁路交叉口必须遵守以下两项要求：在控制器命令降低车门的时刻和列车出口（R1）且车门在两项要求内关闭的时刻之间，车门不得打开T.U.在控制器接收到"进近"信号（R2）之后。 在MITL语法中，R1写为Q（c2 ⇒isup），R2用Q表示（is up≤ c1 ⇒z，δ>RS→S}time-pred（z）={s|s \tS→S}DEFJ JEdisc-suc（e，z）={s| s> s>s> sDefJEJdisc-pred（e，z）={s| s> s>s>s（e，z，c）后的运算通过离散跃迁e，即，在进行离散跃迁e并允许一些时间经过（w.r.t是常数c）之后，可以从z中的某个状态到达的所有状态。pree（e，z）通过跃迁e限定z的前一个区域。DEFpost（e，z，c）=关闭（时间成功（磁盘成功（e，z）），c）DEFpree（e，z）=disc-pred（e，time- pred（z））用在post（e，z，c）中，闭（ζ，c）运算在多面体ζ上，而fines是一个新的ζJ（为了简化符号，在post的定义中，闭运算在一个区域上）。直观地，通过将c设置为大于c的所有下限并将∞设置为大于c的所有上限，从ζ的约束获得最终Ζ J的约束。在[11]中给出了正式模拟图形。时间自动机A的模拟图是一个有限的图，其中每个节点是一个区域，并且过渡是离散的过渡（区域内隐式的时间间隔）。形式上，让c是大于或等于cmax（在A的时钟约束中出现的最大常数）的自然常数。 W.R.T.的模拟图 C、书面SG（A，c），是一个元组Z是对（q0，时间成功（零）），并给出一个区域z和一个A的跃迁e，如果zJ=post（e，z，c），则zJ我有一个nd ddethegraphandz→ezJiatransitionof th egraph（theusoft he）在模拟图结束的后保证的定义中的关闭操作）。F. 贝勒加德等人。理论计算机科学电子笔记160（2006）971091模拟图的路径。 模拟图的路径是有限的或E0E1无限序列π=z0→z→z2·· ·。该路径称为非Zeno if当时钟x>X时，其中x在π中被无限次重置，或者x从路径中的一个点保持无界。我们将模拟图SG的路径集写成Π（SG）。5.2(DS)timed τ-模拟图为了执行仿真的验证，我们在应用于仿真图时对这些关系给出了新的定义。我们证明了这一点，给出了两个模拟图SG2和SG1，以及时间自动机A2和A1，它们分别被构造，如果SG2（DS-）τ-模拟SG1，则A2（DS-）τ-模拟一个1. 现在我们来看看一个模拟图（DS-）τ-模拟另一个图是什么意思。我们首先关注的是时间τ的表达式--模拟图上的模拟。回想一下，在语义层面上，这种关系由三个条件限定：抽象抽象的严格模拟，τ-动作的抖动，以及关于时间的，抽象之间的延迟没有延长。模拟图上的关系如下：严格模拟和抖动的子句以与语义级别相同的方式完成。关于关于时间的子句，由于时间在区域内中断，该条件被合并到关于严格模拟的子句中（包含在定义5.1的第1条中）。非正式地，它指出，在SG2中的每个抽象之前，时间不会比在SG1中更长。定义5.1（定时τ-模拟Z）设SG1=标签（e2）⇒1⇒JE1 Jz1·（z1→z1×label（e1）=label（e2）×poly（proe（e2， zJ）≤ z2）Xpoly（proe（e1，zJ）≤ z1）≤ zJZzJ）。(ii) 口吃：二一一二一e2 J J Jz2→ z2 ×标签（e2）= τ ⇒ z2 Z z1。定义5.2（定时τ- 模拟图上的让SG1和SG2是两个模拟图。我们说SG1τ-模拟SG2，写为SG2≤zSG1，如果z02Zz01。现在，我们将重点放在DS定时的τ-模拟上，我们称之为Zds。与TA上的关系一样，模拟图上的这种关系用两个额外的子句扩展了Z，这两个子句涉及SG2中τ-循环的缺失和死锁的不引入。定义5.3表示关系式Zds。我们首先给出了模拟图中不存在非芝诺τ-环的定义。110F. 贝勒加德等人。理论计算机科学电子笔记160（2006）97模拟图中的非芝诺τ -循环。为定时自动机的运行给出的定义可以扩展到模拟图的路径。考虑一个模拟的SG图，其中一些动作标签被重命名为τ。然后我们说SG不包含任何非芝诺τ-循环，如果：π，k·（π奏效（SG）×π非芝诺 ×k ≥0 ⇒J J J JE Jk，e·（k ≥ k ×（π，k）→（π，k +1）×标签（e）/=τ））。考虑两个模拟图SG2和SG1，因此SG2不包含任何非芝诺τ-循环。DS定时的τ-模拟Zds是包含在Z2×Z1中的二元关系。我们说z2Zdsz1iffz2Zz1and（poly2）\free（disc（z2））X1poly1（z1）\free（disc（q1））定义5.4（DS定时τ-模拟图之间的模拟）设SG1和SG2为两个模拟图。我们说SG1DSτ-模拟SG2，写SG2≤zdsSG1如果z02Zdsz01。我们先前证明了DS定时的τ-模拟S保留了MITL特性。当我们想在模拟图上验证这个模拟时，我们在这些图上完成了一个新的DS定时τ-模拟Zds。现在，为了利用Sds的特性（即MITL保存），我们必须证明两个模拟图是否具有w.r.t.关系。Zds则两个相关TA处于关系w.r.t.SDS.这由下面的定理来表达。定理5.5让A成为一个时间自动机，SG是从A得到的模拟图。 如果A中没有非芝诺τ-环，那么SG中也没有非芝诺τ-环。证明。它直接遵循[11]的引理5.9，特别指出A的每个非芝诺运行都铭刻在SG的唯一非芝诺路径中，并且对于每个非芝诺路径π，存在铭刻在π中的非芝诺运行。Q定理5.6设SG1和SG2是两个模拟图，（q1，ζ1）和（q2，ζ2）分别是SG 1和SG 2的两个区域。 我们有下面的陈述：对于（q2，ze2）中的每个状态（q2，v2），在（q1，ze1）s.t.中存在单个状态（q1，v1）。（q2，v2）Ss（q1，v1）。形式上：（q2，ζ2）Zds（q1，ζ1）⇒v2·（v2÷ ζ2⇒v1·（v1÷ ζ1>（q2，v2）Sds（q1，v1）。证明。定理5.5证明了与τ-周期相关的部分。对于其他子句，证明是通过定点归纳法完成的。定理5.7考虑两个TAA1和A2及其各自的模拟图SG1和SG2。 我们有：如果SG2≤zdsSG1，则A2≤dsA1。证明。如SG2≤zdsSG1，则z02Zdsz01。 考虑A2和A1的初始状态s02和s01。 根据定义，s02>z02和s01>z01。 我们知道s02是相关的（w.r.t. Sds），其中一个状态在z01s.t.它们在X1上的值相等（定理5.6）。因此，s01是该状态，s02Sdss01。QF. 贝勒加德等人。理论计算机科学电子笔记160（2006）971116结论和未来工作在本文中，我们提出在时间系统的增量建模过程中使用τ-模拟作为一种保证线性时间特性（用MITL表示）保持我们找到了两个关系：一个时间间隔为τ的模拟保持安全属性，一个发散敏感的时间间隔为τ的模拟处理所有的MITL属性，特别是生存性属性。我们实施了这些验证τ-使用工具和PROFOUNDER对工具中的模拟图进行模拟。OPEN-KRONOS图书馆[11]我们的目标是提出一种方法来逐步建模定时系统，同时保持广泛的属性。 我们已经知道时机已经成熟τ-仿真非常适合使用经典并行进行组件集成组成。特别地，给定定时自动机A、B和C、A||B τ-模拟A，如果A τ-模拟B，则A||C τ-模拟物B||C.然而，这些结果在发散敏感时间τ模拟的实践中并不总是有用的，因为经典的并行合成经常引入死锁，正如我们在我们处理的例子中所看到的。然而，使用我们的工具，我们应用我们的方法通过组件的集成对一些系统进行增量建模。 以铁路穿越和一个制造厂为例，它表明在建模过程中既保留了安全性，又保留了生命力。我们还将该方法应用于齿轮控制器的示例[8]。对于此系统，安全属性的维护不是问题。然而，由于用于组件集成的并行组合引入了死锁，因此不能保证生存特性然后，我们目前正致力于找到关于组分的充分条件，以确保在组成这些组分时，复合系统不是τ发散的，并且不包含更多的死锁。在集成组件的情况下，这些条件可以允许找到必须引入组件的正确顺序，以便保留MITL属性。为此，探索的一个方向是使用其他同步作曲。事实上，经典的合成操作员已经恢复了经常引入死锁的能力。在[10，5]中，研究了不同种类的合成算子，以获得它们的非阻塞能力。它们是在定时自动机的子类上研究的，即有截止日期的定时自动机在这个模型中，根据作者的说法，时间进展条件并不被表示为自那时以来位置中的不变条件，而是被表示为每个过渡的最后期限。虽然在可以启用转换时保持快速，但在必须启用转换时保持快速截止日期。然后，研究这个模型和其他组合运算符可以带来什么来处理死锁问题应该是有趣的。112F. 贝勒加德等人。理论计算机科学电子笔记160（2006）97参考文献[1] Abrial，J. R.、在不更改B的情况下扩展B（用于开发分布式系统），第一次会议B方法，法国南特，1996年，第169-190。[2] 阿鲁，R.， 斯坦福大学计算机科学系博士学位（1991年）。[3] 阿卢尔，R.和D.迪尔，《时间自动机理论》，《理论计算机科学》126（1994），第183- 235。[4] 阿鲁，R.，T. 费德尔和T.Henzinger，《放松守时的好处》，ACM杂志43（1996年），p。116-146。[5] 博诺，S.，J.西法基斯和S. Tripakis，定时系统中的应急建模，在：COMPOS1536年，1997年。[6] 道斯，C.和S。Yovine，用Kronos验证多速率定时自动机的两个示例，在：RTSS'98（1995）的程序。[7] 格拉布贝克，R.五、线性时间-分支时间谱II ;具有无声运动的序列系统的语义学，在：Proc. ofCONCUR66-81。[8] 林达尔，M. P.彼得森和W. Yi，齿轮控制器的形式设计与分析，技术转让软件工具3（2001），第353-368。[9] Pnueli，A. 程序的时间逻辑，载于：第18届IEEE研讨会论文集。《计算机科学基础》，1977年，第46-77。[10] Sifakis，J.和S. Yovine，定时系统的组成规范，载于：STACS347-359。[11] 特里帕基斯，S.，"时间系统在实
我的内容管理
展开
