并行LSC验证下的偏序符号自动机

理论计算机科学电子笔记145（2006）95-111www.elsevier.com/locate/entcs并行LSC验证偏序符号自动机Tobe Toben1，3Bernd Westphal2，4CarlvonOssietzkyUniversitüatOldenburrg，26111Oldenburrg，Germany摘要部分有序符号自动机（POSA）被用作可视化形式主义的语义基础，如基于场景的实时序列图（LSC）语言。为了检查模型是否满足LSC要求，LSC 因此，通过CTL和LTL模型检查的众所周知的复杂性属性，LSC的POSA的大小直接影响模型检查任务的运行时间。大小随着LSC所允许的并发性而增长，例如，当LSC元素的观察顺序通过将元素包围在共区时放松时。我们研究POSA与确定性的状态，即状态与不相交的注释传出转换的分解特性。我们设计了一个程序，分解成一组POSA的交集语言是等于原来的POSA的语言与确定性状态的POSA。当在主导态分解时，得到的POSA严格较小。由于针对LSC获得的POSA中的大多数状态是确定性的和支配性的，因此LSC的模型检查可以有效地分布。关键词：分布式模型检测，实时序列图，自动机分解。1这项工作得到了德国研究委员会（DFG）的部分支持，作为跨区域合作研究中心SFB/TR 14 AVACS的一部分。2这项工作得到了德国研究委员会（DFG）在项目USE（DA 206/7-3）中的部分支持，作为优先计划SPP 1064的一部分。3电子邮件：toben@informatik.uni-oldenburg.de4电子邮件地址：westphal@informatik.uni-oldenburg.de1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.00796T. 托本湾Westphal/Electronic Notes in Theoretical Computer Science 145（2006）951介绍对设计中的模块化系统的功能要求包括对单个模块的要求、对象内行为以及对模块之间的通信的要求、对象间行为。实时序列图（LSC）语言是一种用于场景的可视化形式，即。对象间通信的序列[4，9，7]。它是著名的消息序列图（MSC）语言的保守扩展[8]，但基本上通过提供模态来显著增强表达能力对于整个图表、对于像消息和条件这样的元素以及对于图表中的位置。为了简洁起见，我们为了更全面的介绍，读者可以参考文献[4，9，7]。图表的模式是存在的和普遍的，允许规范者区分示例和协议。如果系统运行符合场景（MSC的默认解释），则系统满足示例，如果系统的每次运行都符合场景，位置模式（即LSC元素连接到实例线的图形位置）是热模式或冷模式。前者需要进步，后者不需要LSC元件的模式，例如条件或消息是强制的或可能的。如果违反强制性条件，则运行不满足LSC。如果违反了可能的条件，则立即退出场景，并认为运行满足LSC。就像MSC一样，LSC元素的观察顺序由它们在每个实例行的相对顺序决定不同实例行上的元素是无序的，除非它们是同步的。同步元素是瞬时消息和条件，其位置必须同时观察，异步消息，其接收必须在发送后严格观察。但是观测的顺序不仅可以被限制，而且可以通过将多个元素封闭到一个共域中来显式地放松，用一条平行于实例线的虚线来表示例如，考虑图1（a）中所示的LSC主体5。瞬时消息a1和a2的发送和接收被包含在由虚线指示的共域由于消息 换句话说，图1（a）要求模块Inst2LSC包括LSC主体、名称、图表模式、激活条件和激活模式（参见图5）。秒4介绍后两个概念）T. 托本湾Westphal/Electronic Notes in Theoretical Computer Science 145（2006）9597a1，a2，a 3q0a1，a2，a 3a1，a2，a 3a1，a2，a 3a1，a2，a 3a1，a2，a 3a2，a3q1a2，a3a1，a2，a3q2a1，a 2，a 3a1，a 3q3a 1，a 2a1，a3a1，a 2的1一个2一个3a2，a3一个一个一a1，a213a3q4a2，a3a1，a3q5a1a1，a2q6a2一个3的1一个2BQ7BB八方真第2次试验Inst1的1一个2B第2次试验Inst1q0a1，a2a1，a 2a1，a2a1，a2a2q1q2a1a1，a2a1，a2年q3BB四方真(a) 两条信息共域。（b）图1（a）的符号自动机。（c）三个信息同区域。（d）图的符号自动机。1（c）.Fig. 1. 并行LSC示例。过渡注释中的逗号（'，'）读作连词，上划线读作否定。每个消息名称都指消息的发送和例如，图中从q0到q1的过渡。1（b）只有在发送和接收消息a1而不发送也不接收消息a 2时才能采用。以任何顺序接收LSC [9]的语义是用符号自动机来解释的，符号自动机是一种布尔希自动机的变体，其中转换是用简单的表达式来表示的，而不是用字母表的元素来为LSC获得的符号自动机实际上是部分有序符号自动机（POSA），其中自动机 中 的 唯 一 循 环 是 自 循 环 [12] 。 图 1 （ b ） 显 示 了 图 1 中 LSC 的POSA[9][10][11][12][13][14][15][16][17][ 19]每个自动机状态直接对应于LSC的部分观察或切割。例如，状态q1对应于已经观察到消息a1但尚未观察到消息a唯一合法的连续性是先观察到a2，然后观察图1（a）中的实例线为实线（非虚线）表示所有位置都具有热模式，因此强制执行进度因此存在98T. 托本湾Westphal/Electronic Notes in Theoretical Computer Science 145（2006）95在图中，只有单个CC出现在POSA中。1（b）. 如果一个词可以触发一系列的转换，那么一个布希S.T. 一个接受的国家是经常被访问的图1（c）基本上示出了与图1（a）相同的LSC，但是在Inst2用“b”消息应答之前添加了要从模块Inst1发送到Inst2的第三消息a3图1（d）中所示的相应POSA在状态数量和转换数量上都爆炸并不令人惊讶，因为它现在编码三个消息的所有交织。虽然是综合的例子，但图1所示的LSC并不是病态的，因为在需求中保留特定的操作顺序是常见的做法，特别是在更高级别的规范和需求开发的早期阶段注意，在图1中的小例子中，共域特别适合于证明LSC中的并发性对POSA的影响，但在实践中，不受限制的订单更频繁出现的来源是LSC的非相关部分中的元素不被同步元素同步如果规范中提到的模块应该在不同的资源上并发运行，则交织本质上是不受限制的，这必须在需求规范中反映出来。针对系统模型的LSC模型检查有两种方法。首先，POSA可以转换为与模型并行组合的观察者自动机[6]。例如，在通用LSC的情况下，如果并行组合全局地满足最终到达接受状态，则模型满足LSC。其次，POSA可以转换为CTL公式[12，10]并直接进行检查，LSC的子集可以转换为LTL公式[10]。由于模型在状态和转换方面的大小以及规范的大小至少线性地影响CTL和LTL模型检查的最坏情况时间复杂度，因此LSC的模型检查在LSC中存在大量并发的情况下面临规范方面的爆炸问题当使用观测器自动机时，检查公式是恒定的，但是模型和POSA在状态和转换方面的并行组合的大小线性地依赖于POSA的大小在本文的过程中，我们讨论了一种方法，这种爆炸问题的分布式模型检测。我们观察到，在为LSC构造的特定POSA中，许多节点可以在语法上被识别为决定性的，即传出转换的注释是不相交的。另外，它们的一些后继节点是支配的，即，到这些节点的每条路径都经过它们的支配节点。我们表明，POSA，然后可以分裂成（严格较小）POSA的交集语言是平等的T. 托本湾Westphal/Electronic Notes in Theoretical Computer Science 145（2006）9599原始POSA的语言。对较小的POSA进行模型检查可以分布式执行，从而加速模型检查过程，并使一些资源密集型任务变得可行。1.1相关工作否定索赔自动机分解的可利用性，即：[2，1]研究了属性自动机的否定，以获得分布式LTL模型检验过程。在分布式LTL模型检测算法中，他们利用否定声明自动机中的强连通分量来获得状态空间我们的方法是不同的，因为我们只分解财产因此，LSC模型检查可以使用任何模型检查器进行分配，并且不支持[2，1]中同步所需的通信开销注意，[1]独立地观察到，他们的方法很好地适用于右嵌套“Until”算子链的公式，本文回顾了Schlor[11]的工作，其中POSA是符号时序图的基础，符号时序图是另一种视觉形式。他设计了一个翻译POSA到LTL，并获得了一个引理，该公式的一个确定性POSA可以翻译成一个大的合取与析取条款表明，另一部分的公式是我们的方法遵循同样的思想，但已经在自动机的层次上应用了它。偏序约简的目的是从模型中移除一些对于特定规范不可见的并发。相比之下，我们的方法针对的是规范，其中所有并发都必须被保留。1.2结构本文其余部分的结构如下。节中2.在签名上引入POSA。秒3是本文的主要贡献，它给出了一个分解过程，该分解过程对出度大于1的确定性和支配性POSA态进行分解，得到严格较小的自动机，其交（或并）语言与原自动机的语言相同秒4激励这些结果如何可以应用于获得分布式LSC模型检查，以及为什么他们预计将适用于典型的LSC。秒5提供了实证结果，从我们的方法和SEC的评估6结束100T. 托本湾Westphal/Electronic Notes in Theoretical Computer Science 145（2006）952符号自动机一个系统性的自我管理者[9]基本上是一个有限的接受者，也就是那些经常访问一个接受状态的人。不同之处在于，符号自动机的转换是由签名上的表达式标记的，而不是像在布希自动机的一般情况下那样仅由字母表的元素标记的。如果签名中谓词的解释（以及变量的固定赋值）满足转换的标记表达式，则可以在系统自动机中进行转换因此，符号自动机在签名上接受的单词是签名中谓词的解释序列2.1预赛首先，我们介绍了签名、结构和赋值的（标准）概念可以在LSC中使用的布尔表达式和符号自动机中的转换注释都是在这样的签名上定义的。定义2.1签名S =（V，P）包括一组变量V和一组谓词P。一个元组M=（U，I），其中U是一个非空的具体值集合，称为论域，I是P中谓词符号的解释，称为S的结构。谓词PoverU的所有解释的集合用IntU（S）表示将变量映射到全域值的函数σ，即σ：V → U，称为V在U中的赋值。变量V在U上的所有赋值的集合由ValU（S）表示♦定义2.2设S=（V，P）是一个签名。上的布尔表达式S，用ExprS表示，由语法：：= true|均p0|p（x1，. ，xn）|¬ψ1|ψ1∧ ψ2其中p0∈P是一个0元谓词，p∈P为正元，x1，.，xn∈V变量我们将使用缩写false、、→和Participate。♦称结构M在值σ∈ValU（S）i <$M，σ下满足表达式<$i ∈ Expr S| = 0。该“|=”关系像往常一样在公式的结构上归纳地定义。一个布尔表达式<$∈ExprS称为重言式，表示为|=，i M，σ|对于S的每个结构M =（U，I）和每个赋值σ∈ ValU（S），所考虑的系统模型可以很容易地抽象为一组系统运行，即。一系列的谓词解释。注意，在我们的例子中，使用原子命题序列是不够的，因为核心LSC可以使用具体化变量和正性谓词。T. 托本湾Westphal/Electronic Notes in Theoretical Computer Science 145（2006）95101ισσισ定义2.3设S是签名，U是论域。 无限序列i = 101112. 当i ∈ 0时，S的谓词的解释序列的i∈ IntU（S）称为S在U上的解释序列. 所有解释的集合−→U上S的序列用IntU（S）表示。我们用i（i）表示i的第i次解释ii，用i/i表示子集i（i）i（i + 1）. 从第i个解释开始。♦2.2（偏序）符号自动机本节介绍符号自动机的语法和语义。符号自动机是在签名上定义的。它被接受的语言是一组如上定义的解释序列。定义2.4设S为签名。S上的符号自动机是元组A=（Q，qs，~，F），其中Q是有限状态集，qs∈Q是初始状态，~<$Q×ExprS×Q是转移关系，F<$Q是接受状态集。♦对于签名S上的符号自动机A=（Q，qs，~，F），我们定义二进制关系→，→，→：={（q，qJ）∈Q×Q|n∈Exp rS：（q，n，qJ）∈~}，→n：=→\{（q，q）|q ∈Q}。A的状态和转换大小为|一|Q：=|Q|和|一|~：=|--|，resp.，并且状态q∈Q的整数和整数是整数g（q）：=|{（qJ，q）∈→}|，则d eg（q）=|{（q，qJ）∈→ε}|.一个解释序列i被符号自动机接受，如果它在自动机中有一个接受运行，即从初始状态开始的一系列状态，其中i的每个位置处的谓词解释满足自动机中相应的转换注释。定义2.5设A=（Q，qs，~，F）是符号上的符号自动机，−→自然S和U是一个宇宙。 让= 101112. ∈IntU（S）是一个解释U上的序列，σ∈ValU（S）是一个赋值.无穷序列π = q0q1q2. . 其中qi∈ Q，i ∈0，称为A在i上的游程，其中σ i<$q0= qs且<$i∈0<$（qi，<$i，qi+1）∈~：（U，ιi），σ| = 0。我们使用ει（A）来确定在rσ下A的运行的设置。通过inf（π）<$Q，我们表示在π中无限频繁出现的状态的集合，I.E. inf（π）：={q∈Q|q=qi，对于无穷多个i≥0}。Arunπ∈πi（A）如果inf（π）<$F/=<$，则称为接受。S上的符号自动机A在σ下接受的语言是定义为Lσ−→（A）：={∈IntU（P）|{A}{A♦102T. 托本湾Westphal/Electronic Notes in Theoretical Computer Science 145（2006）95定义2.6在签名S上的符号自动机A=（Q，qs，~，F）称为偏序符号自动机（POSA），如果→的自反传递闭包是反对称的，即如果→n是Q上的偏序。♦正如在引言中已经指出的，为LSC获得的符号自动机最多包括自循环，但不包括涉及不同状态的循环，因此是POSA。3POSA分解在本节中，我们研究（部分有序）符号自动机的分解性质我们给出了一个建设性的定义，产生一个适当的分解在确定性的状态，我们确定的优势属性作为一个充分的标准，获得严格的状态更小的自动机。定义3.1设A=（Q，qs，~，F）是符号S上的符号自动机.一个状态q∈Q称为确定性i <$$>（q，<$1，qJ），（q，<$2，qJJ）∈~：qJ/= qJJ=<$|=2）。一个状态q∈Q称为可达确定性i，所有满足（QJ，q）∈→i的状态QJ∈Q都是确定性的。♦对于分布式模型检查，有两种分解属性是很有意义的。对应于图表模式存在，人们想要检查给定的系统，即。一组解释序列，至少一个解释序列是否被自动机接受在这种情况下，分解中自动机的语言的并集应该等于原始语言。然后，查询可以被分发，因为如果来自分解的一个自动机接受解释序列，则存在原始自动机的接受运行对应于图表模式universal，人们想要检查解释序列的整个集合是否在语言中。如果分解中的自动机的交集语言与原语言相等，则可以分布式地检查分解中的所有自动机是否接受所有的解释序列。定义3.2设A是签名S上的符号自动机。 集合{A1，. ，AN}，N> 0，称为S上的符号自动机(i) A的A-分解i ∈L（A）=(ii) A的E-分解i ∈L（A）=1≤i≤NL（Ai）和1≤i≤NL（Ai）.♦下面的定义构造了到达确定性状态q的普适q-分解。在分解中的每个自动机中，除了一个外，q的所有传出转换都被删除，并添加一个新的转换，该转换被标记为删除的转换表达式的析取，并导致接受sink状态。见图2、举个小例子。T. 托本湾Westphal/Electronic Notes in Theoretical Computer Science 145（2006）95103qsqq2 ψψ0水槽Truψ2ψ1年q1ψ3Q2真年q3真水槽水槽水槽水槽LLL真E真(a) 一(b) 的1(c) 一个2图二、A到{A1，A2}的泛q-分解下面的引理建立了所需的性质，即泛q-分解是A-分解.该程序由Schlo？r[11]的一个引理启发，其中该引理是一个disjunc-将不相交表达式i<$i化为等价合取i（<$i<$φi）其中φi是所有表达式j的析取，其中j/=i（见下文）。定义3.3设A=（Q，qs，~，F）是签名S上的POSA，q∈Q具有1outdeg（q）=N的到达确定性状态。（q<$i，qJ）∈→<$} < ${qi}O O水槽~i：={（qJ，n，qJJ）∈~O|qJ，qJJ∈Qi} <${（q，<$i，q<$i），（q，φi，qi我水槽 ，true，qi）}Fi：={qi其中qi{\displaystyle {\frac{i}f ∈Q是新的自动机状态，：= j=1. N，j/=i阿贾克斯，被称为A的泛q-分解.♦引理3.4（POSA分解）设A =（Q，qs，~，F）是签名S上的POSA，q ∈Q是可达确定态，其中1

下载后可阅读完整内容，剩余1页未读，立即下载