基于CTL模型的稠密实时系统模型检测新方法

理论计算机科学电子笔记133（2005）41-60www.elsevier.com/locate/entcs基于CTL模型的实时系统分析穆斯塔法·布拉赫拉1阿尔及利亚Biskra大学计算机科学系Mohamed Benmohamed阿尔及利亚君士坦丁大学计算机科学系摘要提出了一种稠密实时系统模型检测的新方法。稠密实时系统由时间自动机建模，其性质由时序逻辑TCTL具体化。TCTL属性的具体化被简化为CTL，其时间约束被捕获在一个新的时间自动机中。这个时间自动机将与指定被分析的实时系统的原始时间自动机组成然后，利用基于强互模拟的状态空间划分精化方法，对乘积时间自动机进行抽象其结果是一个不定时自动机模的TCTL属性，它表示一个等效的有限状态系统，使用现有的CTL模型检查工具进行模型检查关键词：实时系统，模型检测，时间自动机，强互模拟，分区细化。1介绍许多被提出来推理实时系统的形式化框架都是基于时间自动机[2]。这些自动机配备了时钟，用于测量时间的变量，范围在非负实数Numbers（R+）。因此，状态空间是无限的，并且不能通过枚举所有状态来直观地表示。在不同的描述1电子邮件：mbourahla@hotma il. 网2电子邮件：ibnm@yahoo.fr1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.05742M . Bourahla，M. Benmohamed / Electronic Notes in Theoretical Computer Science 133（2005）41-60语言用于指定实时需求，我们特别感兴趣的时间逻辑TCTL [1，10]。实时模型检测工具由于引入了密集时间，使得定量推理更加复杂，大多数已发布的实时模型检查算法都基于向后/向前可达性分析[4，12]，该分析已在几个成功的验证工具中实现。其他算法基于组合技术[11]，其中实时系统的组件在验证过程中逐渐移动到规范中。基于分区细化的实时模型检查技术[17，19]构建了一个尽可能粗糙的符号状态空间。从某个（隐式）初始划分开始，迭代地细化划分，直到可以确定验证问题。本文在不改变经典CTL模型检测算法的基础上，提出了一种从TCTL模型检测到CTL模型检测的归约技术 因此，所生成的模型可以被翻译成 直接检查现有的CTL模型检查器之一。 给定一个定时自动机A和一个TCTL公式，我们构造了一个等价的CTL公式和一个新的时间自动机A+，增加了从公式中提取的行为和特定时钟。我们证明了A满足λ当且仅当A+满足λ。对所构造的时间自动机A+的行为进行建模的变迁系统包括两种变迁，即代表系统离散演化的无时间动作和对应于时间流逝的时间流逝由于时间的密度，有无限多的时间转换。一个有限模型可以通过定义一个适当的当量来获得，等价关系导致有限个等价类。这些关系背后的主要一个重要的问题是构造一个标记的转移系统（表示一个时间自动机）的商关于一个等价关系。在本文中，我们定义了一个基于强双模拟的等价关系[13]，我们的算法使用它来生成商图。定时自动机中的每个边沿代表一个离散转换，该离散转换具有关于源和目标状态、使能条件和在进行该转换之后要重置的时钟集合的信息。最初，时间自动机将时间系统的状态表示为状态块（区域）（也称为符号状态）。我们称之为状态的初始划分。如果存在一个具有不同于真的使能条件（这是一个约束）公式的输出边，则我们使用状态块的不变量和该转换的使能条件M. Bourahla，M. Benmohamed / Electronic Notes in Theoretical Computer Science 133（2005）4143∃产生的子块表示等价状态的类别，其中每个子块具有满足或不满足使能条件的新不变量。如果没有状态块需要精化，精化过程将终止。所产生的抽象时间约束的有限图可能太大。有可能使用基于等价的约简[5，19]的一种方法来约简这个有限图。相关工作类似的工作可以在[6]中找到，其中模型检查基于对仿真图的探索。模拟图是从区域图[1]和初始区域生成的可达图。因此，由于模拟图中的节点是区域集，并且只有离散转换是显式的，而时间在节点内隐式地流逝，因此模拟图比区域图小得多。利用仿真图解决了一种基于自动机的分支时间时序逻辑（TECT L）的模型检测问题。基于模型的检验过程在于解决空性问题，也就是说，检验一个自动机（系统自动机和属性自动机的自动机乘积）是否有满足给定接受条件的无限执行序列。在我们的工作中，捕获时间约束的属性自动机是从TCTL规范自动生成的。 我们的商图是直接从初始自动机产生的时间系统规范，类似于仿真图，而不经过区域图。商图比初始自动机粗，但比初始图细，因此比初始图大。在[16]中已经提出了另一种算法，该算法也结合了基于符号的方法和符号方法。在这项工作中，一个符号图是动态构造的验证过程，根据公式（指定在扩展的时间逻辑的微演算）进行检查。在[9]中给出了密集时间TCTL（具有冻结量化器的TCTL [3]）的导数的类似约化。这种方法通过一个新的原子命题和新的转换来处理重置量化器，从而增强了[1]中使用的区域图。另一个相关的工作可以在[8]中找到，其中通过向模型添加额外的指定时钟将TCTL（在离散时间上解释）转换为CTL来执行验证。因此，为了对增强模型进行模型检查，CTL逻辑被扩展，因此模型检查器也被扩展。在[18]中可以找到与我们基于等价的时间抽象最接近的工作其中[5]中用于最小模型生成的算法（这是Paige和Tarjan [15]算法的增强，以避免细化不可达类）适用于时间自动机的有限状态空间。44M . Bourahla，M. Benmohamed / Electronic Notes in Theoretical Computer Science 133（2005）41-60该算法利用判定过程计算类的交集、集差和类的前趋，并检测类是否为空。此外，TCTL规格化被减少到CTL逻辑扩展与新的原子命题，以处理规格化约束。在此基础上，基于经典的CTL模型检测器技术，开发了一个TCTL模型检测器。其他技术是基于抽象的系统和属性中指定的约束，使用谓词抽象的框架作为抽象解释[7，14]。本文的其余部分组织如下。 在第二节中，我们给出了用于描述时间系统的时间自动机的形式。第3节介绍了逻辑TCTL和我们将TCTL规范转换为CTL规范的方法此外，在本节中给出了转换正确性的证明在第4节中，我们提出了生成时间系统的有限双相似图第5节解释了使用这些图进行CTL模型检查的方法，以及如何将结果投射回原始的时间系统。最后给出了结论。2用时间自动机我们通过时间自动机[2]对实时系统进行建模，通过添加时钟来扩展时钟是随时间均匀增加的实值变量。可以为同一个时间自动机定义几个独立的时钟。一个时间自动机A是一个元组Q，X，E，L，I，Q，其中：• Q是一组有限的位置。 我们用q0∈ Q表示初始位置。• X是一组有限的时钟。赋值v是将非负实值v（x）∈ R+赋给每个时钟x ∈X的函数。 赋值v[X：= δ]将值δ赋给集合X中的所有时钟。赋值的集合被表示为VX。 对于δ∈R+，v+δ表示对所有x ∈ X，vJ满足vJ（x）=v（x）+δ的方程vj.• E是一组有限的边。 每个边e ∈ E是一个元组<$q，θ，X，qJ <$，其中· q，qJ∈Q分别是源位置和目标位置，· θ∈ Θ是控制转换触发的相关时钟约束。它被称为它的使能条件或它的警卫。我们用Θ表示X上的约束集。 约束被定义为形式为x <$c的原子的结合，其中x ∈ X，<$∈ {<，≤，>，≥，=}，c是自然常数。· X = X是在进行此转换后要重置的时钟集。• L：Q →2AP是将每个位置关联到一组原子参数M. Bourahla，M. Benmohamed / Electronic Notes in Theoretical Computer Science 133（2005）4145从集合AP的命题。• I是满足条件I（q）∈Θ到每个条件q∈Q的函数称为q的不变量。true，{x}∅q0真x= 1，{x}x≥2，{p}年q1x≤1x=1，{r}q2真Fig. 1. 时间自动机图1示出了时间自动机的示例，其中AP ={p，r}并且Q ={q0，q1，q2}。A的一个态是一个对<$q，v<$∈ Q × VX ，使得v满足I （q）。 初始态是对<$q0，v0<$ch，对所有x ∈ X，v0（x）=0. 设S表示A的状态集。 我们将用L（q）来指代L（s），对所有s ∈ S，其中s=<$q，v<$。集合S可以被划分为区域（符号状态）。区域z =（q，Vz）是来自S的状态的集合，其与相同的离散状态q ∈ Q和赋值的凸集Vz={v |<$$>q，v<$∈ S}。定时系统的状态可以通过改变位置并重置一些时钟的边沿（离散过渡）来改变，或者通过让时间流逝而不改变位置（时间过渡）。设e=<$q，θ，X，qJ <$∈ E是一条边. 状态q，v具有离散变换，sitiontoqJ，vJ，denotedq，v→−e qJ，vJ（我们应该注意到，关于θ的赋值集总是在关于I（q）的赋值集内）。 设δ∈R+. 这是一个时间转换，toq，v+δ，denotedq，v−→τ对于所有δJ≤δ，v+δJ，i f，i nv a rintI（q）. 我们记M=（S，S，s0）A的转换系统，其中是离散跃迁或时间跃迁，s0是初始状态。一M的运行r是一个无限序列，0是1个序列和transition。We记R为M的游程的集合。 一个运行是发散的，如果∞i=0时 δi（所有在该运行中的延迟δi）发散。我们记R∞为M的发散游程的集合。在下文中，我们将考虑仅具有发散运行的时间自动机（如果自动机具有非发散运行，也称为zeno运行，则可以将行为限制为发散运行[10]）。从理论的角度来看，我们表示的定时模型作为一个标记的过渡系统（LTS），其中每个离散的过渡有一个标签（行动）。如果进行转换，则该动作重置由该转换指示的时钟集合。时间转换有一个名为τ的特殊标签，用于记录时间流逝，这被认为是一个内部或隐藏的动作。 让一个是动作的集合，A τ= A <${τ}。给定 一个有标号的转移系统46M . Bourahla，M. Benmohamed / Electronic Notes in Theoretical Computer Science 133（2005）41-60LT S=（S，Aτ，T，s0），S是从s0到T的可达状态的集合。T <$S ×Aτ×S是（离散或时间）跃迁关系，s0是初始状态。 对于每个标签a和每个状态s，我们考虑像集Ta（s）={SJ∈ S|（s，a，SJ）∈ T}。我们将这个符号扩展到状态集：Ta（B）=<${Ta（s）|s∈B}。T-1表示逆关系。3减少TCTL规格定时系统的许多重要性质在实时时序逻辑TCTL中找到了自然的表达，它扩展了分支时间逻辑CTL [1，3]。这个扩展要么增加了具有时间边界的时间运算符，要么使用重置量化器。我们使用一个版本的TCTL与时间界限。时间计算树逻辑TCTL的公式由文法归纳定义，：：= true |p |¬ψ|ψ ∧ ψ |ψ∃U∼cψ|我知道了。其中p ∈ AP是一个原子命题，为了简单起见，将p限制在集合{≤，≥}中，c∈N（N是自然数的集合）。时间算子Q c和Qc分别代表真Uc和<$Qc<$，时间算子Qc和Qc分别代表真Uc和<$Q c<$。TCTL的公式被解释在由转移系统M表示的时间自动机的状态集合上。设M中的一个可达状态为<$q，v <$∈ S，并设一个TCTL-公式<$. 满足关系，用q，v表示|= M，根据的语法归纳定义：• 格河|=Mtrue• 格河|=Mpi <$p ∈ L（q）• 格河|=M<$iq，v|=M• 格河|=MjJJi q，v|=Mjq，v|=MJJ• 格河|=M<$J <$U<$c<$JJi <$<$r ∈R∞且r（0）=<$q，v <$，<$i. j≤iδjr（i）|= JJ和j JJ当且仅当<$q，v<$|= MJ和q，v|= MJJ. 归纳假设是：|= Mj（q，qJ），v| = M+J和q，v| = M<$JJ<$$>（q，qJ），v<$|= M+JJ。通过TCTL <$（q，qJ）的语义，v<$|= M+jJJ。对于=JUcJJ。 通过TCTL的语义，可以得到：q0，v我的天|=MjJ和jJ，我们证明了<$q，v<$|= M惠益q，v|= M+ m，其中M+和m是通过调用U ntime（m）构造的。 归纳假设是：|= MJ J+J Jψ优惠券q，v|=+拉吉其中，MJ 和构造 时间（）。根据算法U ntime，m=M，并且M+=M+。根据TCTL的语义，|= M<$J当且仅当不为（q，v|= MJ）。通过归纳假说，|= M<$J当且仅当不为（q，v|= M+ψ 1997年）。JM. Bourahla，M. Benmohamed / Electronic Notes in Theoretical Computer Science 133（2005）4151MJMM拉吉MMMk=00001现在，通过TCTL语义，我们可以得出：|= MJ当且仅当格河|=+拉吉 我知道 这意味着，|= M<$当且仅当<$q，v<$|= M+ N。对于=jJJ。 首先我们证明了，|= Mq，v| = M+N。 根据TCTL的语义，|= M<$j<$$>JJ当且仅当<$q，v<$|= MJ，格河|= MJJ. 归纳假设是：|= MJ惠q，v| =M+ MJψ和q，v |=JJ惠q，v| =+吉吉JJ，其中是从TCTL子构造的CTL公式（时间自动机），式分别为M+和M+是一个过渡系统，AAJ 和AAJJ。 根据自动机合成的性质3，我们有q，v|= M+J和q，v| = M+JJ。然后，我们可以通过使用TCTLq，vq的序列，|=M+jjJ（M+是A A jAj的转换系统）。现在，我们证明，|= M+q，v| = M。我们知道，从n构造n，并且n的形式为N，j 子公式J和自动机AJ都是从子公式J构造的（JJ和AJJ也是从JJ构造的）。根据归纳假设（q，v|=+拉吉J惠 |=J和q，v| =+吉吉JJ惠|= MJJ），使用组合属性TCTL-属性 3和TCTL的语义，我们可以得出结论，|= M+jJJq，v| = MjJJ.对于φ = φJφU≤cφJJ。考虑M中的一个状态<$q，v<$。假设q，v，|= M- 是的 然后，根据TCTL的语义，存在游程r=Vq0，v0，Vq1，v1，···，<$qi，vi<$，···∈R∞，其中<$q0，v0<$=<$q，v<$，其中i≥0，使得<$iδk≤c，我的天|= M<$JJ，对于所有0 ≤ j 1 <$x ≤2），它不是凸的）。(vi) 如果θ是凸的，那么这个运算符将返回θ本身，否则它将返回表示下凸赋值的约束。 约束θ是在一个时钟变量上定义的（例如[x<1x<1）。(vii) [θ|如果θ是凸的，那么这个运算符将返回θ，否则它返回表示上凸赋值的约束。 约束θ是在一个时钟变量上定义的（例如[x <1 <$（x> 1 <$x≤ 2）|x> 1 x ≤2）。下面的算法定义了一个区域，该区域是从当前分区的集合E中任意取的边e=q，θ，X，qJ的源，其中θi=true。该修正基于时钟变量x，该时钟变量x也是从约束θ中的时钟变量集合中任意选取的。该区最多可分为三个分区. 这些子区域具有相同的位置q，但具有不同的不变量。它们的并集n等于soI（q）。由于这两个变量是不同的，为了简单起见，我们将它们的位置q表示为不同的，以区分它们，这将不会对算法结果产生任何影响第一个子区（具有离散状态qx）h，因为i变量tI（qx）=θxI（q）|x和一个不连续的edgeqx，θ|x，n，qJn.如果[I（q）<$x\θ<$x <$m]，我们有一个具有离散状态的子区域qL，其中ani nv a ria ntI（qL） =[I（q）|x| θ | x |θ||I（q）]|X. 他在一个小地方传出的edgeqL，true，n，qxn。 If[I（q）<$x\θ<$x|f=n，我们有一个第三个子区，它具有离散状态q u和一个不变量I（qu）=[I（q）<$x\θ<$x|I（q）|X. 这个副区有一个向内的边缘qx，true， 这三个新的子区域S将由原子命题集合L（q）来标记。M. Bourahla，M. Benmohamed / Electronic Notes in Theoretical Computer Science 133（2005）4155JXLu在该迭代结束时，边缘e和区域Z将被移除并由新的边缘和新的子区域代替。来自和到达区域Z的其他传出和传入边缘将根据新分区进行更新，有关更多详细信息，请参见算法。时间自动机的非顶点性及其约束的凸性保证了所产生的分区具有保持凸性和非顶点性的区域此外，算法终止。算法2划分细化（A=Q，X，E，L，I）{如果（E ∈ E |e = θ/= true）{设x是约束θ中的时钟变量。EOld<${e};Cq <$qxwithI（qx）=θ<$x<$I（q）<$x andL（qx）=L（q）;JENew<${q，θ<$x，，q<$};if（[I（q））{Cq<$C q<${ql}其中ithI（ql）=[I（q）<$x\θ<$x<$$ > I（q）<$xandL（ql）=L（q）;ENew←ENe w<${<$ql，true，n，qx <$}}if（）I（q））{Cq<$C q<${qu}withI（qu）=）I（q）<$x\θ<$x<$$ >I（q）<$xandL（qu）=L（q）;ENew←ENe w<${<$qx，true，<$，qu<$}}对于每条边eJ=<$q，θJ，XJ，qJ <$∈ Edo //输出边E旧← E老 {eJ}JJJJif（[I（q）<$x\θ<$x<$/=< $ $ >θ<$I（ql）/=<$）ENew<$ENew <${<$ql， θ<$I（ql），X，q<$}J JJJif（θ<$I（qx））ENew<$ENew<${<$qx， θ<$I（qx）， X，q<$}J JJJif（）I（q）<$x\θ<$x <$/=< $ $>θ<$I（qu）/=<$）ENew<$ENew<${<$qu， θ<$I（qu），X，q<$}端对于每条边eJJ=<$qJJ，θJJ，XJJ，q<$∈ Edo //传入边E旧← E老 {eJJ}JJ JJif（[I（q）<$x\θ<$x<$