理论计算机科学电子笔记175（2007）63-72www.elsevier.com/locate/entcs随机图变换系统的验证维塔利·科齐乌拉UniversitaütDuisburg-Essen，Germanyvitali. uni-due.de摘要本文描述了随机图变换系统（GTS）的检验所得到的一些统计结果。作为一种验证技术，我们使用Petri网对GTS进行过近似。 我们要验证的属性由Petri网的标记给出。我们还使用反例引导的抽象精化方法来精化所获得的近似。一个软件工具（A UGUR）支持核查程序。本文的想法是看看有多少生成的系统可以使用这种技术成功验证。保留字：随机图变换，Petri网，AUGUR1引言在过去的几年中，基于近似的图变换系统（GTS）[13]的分析技术已经开发出来[2]。GTS是用Petri图来近似的，Petri图是一种附加了超图结构的Petri网.然后可以用标准验证技术分析Petri网。验证遵循所谓的CEGAR方法（反例引导抽象细化）。这种方法背后的思想是从系统的粗略初始抽象或过度近似开始，并检查是否可以使用这种抽象来验证某个属性如果它不能被验证，则在近似中获得违反此性质的运行，也称为反例。这个反例要么是真的，要么是假的，即，它是由近似引入的。在后一种情况下，近似被这样一种方式重新定义，使得反例消失。这个过程是重复的，但是在无限状态系统的情况下，通常不能保证它会终止，因为要验证的属性通常是不可判定的[9]。DFG项目SANDS支持的研究。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.04.01764诉Kozioura/理论计算机科学中的电子笔记175（2007）63支持这种验证方法的软件工具（AUGUR）已经被定义[7]，并且已经进行了一些成功的案例研究（例如，参见红黑树案例研究[1]）。尽管如此，验证在一般情况下仍然是不可判定的（因为GTS的图灵完备性）。有趣的问题是，有多少GTS可以在实践中使用Petri网和分析Petri网的标准技术对GTS进行过度近似来验证本文是对这一问题的首次尝试我们生成一些随机GTS，并在一个维吾尔人在以获得统计结果。我们考虑由一些参数识别的GTS的一些类别。2图形转换系统图转换系统（GTS）是一种表达性强且有用的规范形式主义，允许描述并发和分布式系统的动态特性[13，6]。GTS在计算机科学的不同领域有许多有趣的应用，它们可以用来指定堆上的指针结构以及网络中的移动进程。一个图转换系统由一个初始图和一组重写规则组成为了获得更多的可伸缩性，我们考虑超图，其中一条边（超边）连接到一系列节点（而不是有向图中的一对节点）。初始图是描述系统初始状态的超图。重写规则由两个超图（左手边和右手边）组成，并指定系统可能的动态转换如果在系统的当前状态中找到左手边的实例，则可以应用此规则，并且规则的左手边的实例将被其右手边替换。嵌入规则指定如何将右侧连接到图的其余部分。图重写的最常见方法之一是DPO（双推出）方法，其名称来自以下事实：重写步骤由两个模拟图粘合的推出来描述。我们目前支持DPO规则的受限版本，其中我们只允许离散接口，即，我们不能描述边的保留，并且禁止节点的合并和删除。但是，可以删除边。从理论的角度来看，扩展到非离散接口并不是很困难，而合并和删除会导致更严重的问题。特别是删除意味着我们必须处理负面的应用条件，这只能用Petri网中的抑制弧来建模。如果满足上面提到的限制，也可以处理图转换的其他方法（例如单推出有关图转换系统的更多信息，请参见[13，5，6]。下面我们给出一个非常简单的GTS的例子来说明AUGUR的主要特征。在该系统中，外部和内部过程可以交叉连接，并且可以创建新的连接。这意味着我们产生了一个树状结构诉Kozioura/理论计算机科学中的电子笔记175（2007）6365连接连接连接的结构-从两个连接开始-并让移动过程沿着树的某个分支非确定性地移动。扩展网络的转换和进程的移动可以交错进行。初始图由一个私有服务器和一个连接到它的内部进程组成通过一个连接分离，存在一个外部进程。在这个例子中，我们计划验证以下属性：表示外部进程的超边和表示私有服务器的超边将永远不会共享同一节点。3图变换系统的图2描述了本文中使用的验证技术我们有一个GTS和一个（可达性）属性1，我们想要验证它作为系统的输入。首先，我们构造了一个Petri图，它是同时具有超图和Petri网结构的GTS的过近似[2]。在分析块中，我们首先计算与要验证的属性对应的Petri网标记（通常从Petri图的超图结构上的正则表达式中获得[11]）。然后在覆盖性算法的帮助下分析标记[10]。如果标记是不可覆盖的，那么我们终止与这意味着在GTS的约简期间不能到达否则我们1检查GTS的可达性属性已经是一个相当复杂的问题，我们在这里限制我们的实验，而不是检查GTS的一般时间属性内部流程外部过程初始图私人服务器连接连接外部过程外部工艺交叉连接外部过程连接1 2连接1 2内部流程内部工艺交叉连接内部流程连接1 2连接1 2创建连接1 21 2Fig. 1. 示例图形转换系统连接66诉Kozioura/理论计算机科学中的电子笔记175（2007）63GTS超时Petrigraph财产分析计数器= 0超时已验证未知计数器> mCOUNTERcounter−examplePROPERTY实例是真实的杂散假反例超时计数器++精化Petrigraph图二.验证技术有两种可能所获得的到可覆盖标记的迹线（反例）可以是真实的或虚假的（即，仅在过近似中可再现，而在原始GTS中不可在实反例的情况下，我们以“PROP-ERTY”结尾否则，我们开始一个反例引导的抽象精化过程[4，9]，并获得一个精化的Petri图。细化过程可以迭代预定次数。如果我们仍然没有验证结果，那么我们以“UNKNOWN”结束。对于每个操作，设置超时，以便当达到超时时，验证过程以“超时”停止。我们说，如果性质被验证或者我们找到了一个（非伪的）反例，则GTS的验证问题就解决了我们使用上一节的例子来演示验证技术。为了分析该GTS，该工具构造了一个过度近似，这是一个所谓的Petri图（即，一个在其上具有Petri网结构的超图，见[2]）。超边同时也是网的位置。例如图3示出了0深度（即，图1中的GTS的粗略）过近似。在图3中，黑色的小矩形和箭头表示Petri网的变迁，黑点表示初始标记，其余结构表示超图。请注意，网络的位置与图的超边重合。这个Petri图在以下意义上是一个过近似：（i）每个可达图都可以通过（通常是非内射的）图态射映射到它的超图组件，以及（ii）它的边的多集图像对应于网的可达标记。更一般地说，在网的可达图和可达标记之间存在一种模拟关系。对于一个标记m，我们说m表示一个图G，只要存在一个从G到底层超图的映射，使得映射到一个位置的边的数目与抽象细化（m次）约展开诉Kozioura/理论计算机科学中的电子笔记175（2007）6367私人服务器内部外部工艺流程1 11连接1内部流程2 1交叉连接外部工艺交叉连接创建连接图三.零深度近似马克m.具体而言，初始标记表示GTS的初始图（以及其他图）。此外，每个转换都与一个规则相关联，并且在应用于图时过度近似该规则的结果我们在这里不描述如何计算Petri图，除了说计算是基于近似展开算法。的al-出租m的设计方式，良好的性质的GTS模型，如局部性（状态变化只在本地描述）和并发性（没有不必要的事件交织）被保留在近似Petri网。更多的细节可以在[2，3]中找到。在这种情况下，过度近似相当粗糙。具体地观察，每个由四种类型的边组成的图（“私有服务器”，“连接”等）可以映射到底层图，因为所有节点都已合并为一个。我们通过这种近似获得的唯一信息是某种类型的边的数量。例如，初始标记报告在初始图中存在类型“私有服务器”的一个边由于近似值过于粗略，因此无法看到进程是否事实上，初始标记表示（在上面定义的意义上）违反要检查的属性的图。同样明显的是，这个反例是虚假的，即，它在原始系统中没有对应物，因为“真实”初始图不违反该性质。一般来说，在AUGUR中实现了一种技术，告诉用户一个反例是否是虚假的，其中反例是Petri网的运行，产生一个标记，表示违反要分析的属性的图。如果找到了一些虚假的反例，可以用两种不同的方法来重新定义过近似(i) 人们可以改变过近似的精确度（深度）。(ii) 人们可以通过禁止合并某些节点来构造一个细化的过度近似在我们的例子中，我们选择第二种可能性，这通常会导致较小的68诉Kozioura/理论计算机科学中的电子笔记175（2007）63内部流程创建连接外部过程交叉连接交叉连接1 1 1 2 1 1内部流程连接外部过程1内部流程1交叉连接连接11创建连接内部流程私人服务器见图4。1-深度近似Petri图我们采用上面得到的反例，构造出精化的过近似（见图4）。表示私有服务器和外部进程的边现在被分离（因为相应的节点已经被分离），并且上面发现的虚假反例被消除。同样明显的是一个外部进程连接到私有服务器的图。这可以使用AUGUR来显示，这意味着该属性可以以自动方式成功验证。4随机图变换系统在本文中，我们生成GTS的超边有arity（连接节点数）1或2。 边可以被标记（我们为每个arity考虑两个标签）。我们不允许两条边在规则的左侧具有相同的标签。我们也不删除任何节点。因此，我们下面只描述添加到规则右侧的节点。以下参数描述了生成的GTS的类：(i) 规则左侧的最小/最大节点数(ii) 规则右侧的最小/最大附加节点数（参见上面的解释）。(iii) 规则左侧的最小/最大边数(iv) 规则右侧的最小/最大边数(v) 初始图中的最小/最大节点数。(vi) 初始图中的最小/最大边数。(vii) 最小/最大规则数。诉Kozioura/理论计算机科学中的电子笔记175（2007）63692_12_22_11_1L误差1_1在本文中，我们考虑以下几类由参数定义的随机系统。(i)（1，2; 0，1; 1，2; 1，2; 2，5; 2，5; 3，5）(ii)（1，2; 0，2; 1，3; 1，3; 2，5; 3，7; 3，7）(iii)（二、三、一、五、三、七、三、七、三、十、三、十、五、十）每一类GTS都严格包含在下一类GTS中。在每个类中，我们生成100GTS。这些数字相对较小，因为我们试图保持生成的GTS的大小可管理，以获得足够的统计材料。在每个GTS中，我们插入额外的特殊规则图五. 误差准则我们要验证的属性是如果可以应用“错误”规则 如果规则“错误”不能被应用，那么我们应该得到答案“已验证”。图6表示从第一类生成的GTS初始图1_11.1113.122.4.1 2 1 11错误代码：2_1见图6。 生成的GTS（第一类系统）2_21_12_21_22_12_22_12_11_12_1误差70诉Kozioura/理论计算机科学中的电子笔记175（2007）635统计结果实验在2*Xeon 2.4 GHz，2GB RAM上完成。我们为抽象细化过程固定了3次迭代，并将30分钟作为超时值。 在表1中，表示了在生成系统的验证期间获得的平均值，即构造的过近似中的节点、边和转换的数量以及验证时间（包括超时）。验证时间以秒为单位计量，代表整个验证程序的时间系统类节点边缘过渡验证时间14.217.674.070.0127.4714.510.5559.87310.0122.2825.78351.53表1已验证系统的平均值图7中的图表（（a）、（b）和（c），暂时忽略（d））描述了上述三类随机系统的验证结果75 7550 5025 25反例验证超时未知反例验证超时未知75 7550 5025 25反例验证超时未知反例验证超时未知见图7。 验证结果(b)二等(a)头等舱(c)三等I(d)第三类II诉Kozioura/理论计算机科学中的电子笔记175（2007）6371一个有趣的值也是一类GTS验证过程中的细化步骤总数。这个值增长得相当快：第一类系统为0步，第二类系统为18步，第三类系统为83步。但请注意，每个GTS的细化步骤数限制为3。正如我们在图中看到7我们已经成功地解决了第一类系统中所有100个GTS的验证问题这些图给我们一个想法的可能性和限制的验证方法的基础上过近似的GTS与Petri网。为了获得更好的验证结果，我们可以增加细化步骤的数量和/或超时间隔。如果我们对属于第三类的相同系统开始验证程序，最多有五个改进步骤，超时两小时，那么我们可以另外解决五个GTS的验证问题，图7（d）。这种情况下的平均验证结果见表2。抽象细化步骤的总数为109。系统类节点边缘过渡验证时间311.8726.5733.061273.74表2具有五个细化步骤和两个小时超时的6结论在本文中，我们考虑了随机GTS验证的统计结果，通过用Petri网近似它们。验证技术已实施在AUGUR 1中，该工具已被用作我们实验的基础 的本文的目的是展示有多少随机GTS可以用这种技术进行验证显然，在真实案例研究中出现的系统通过具有更规则的结构而不同于随机系统，但本文给了我们一些关于这种方法的可能性和困难性的（近似）概念。统计结果可以被看作是相当积极的，因此，验证方法的近似GTS的Petri网可以被看作是一个有前途的方法验证的GTS。当然，也有必要将这些结果与其他方法的相关结果然而，我们目前还不知道任何这样的结果，已公布的随机系统。GTS验证的一些实验结果已在[12]中报道请注意，我们在这里工作在不同的设置中，因为我们考虑潜在的有限状态GTS，而[12]考虑有限状态GTS。作为未来的工作，我们在这里提到了具有更高程度的超边的随机GTS的实验，检查单个参数对结果的影响，通用系统的实验（根据某些正则模板生成的随机GTS），属性GTS的实验以及目前正在开发的新版本工具AUGUR 2[872诉Kozioura/理论计算机科学中的电子笔记175（2007）63引用[1] PaoloBaldan，AndreaCorrradini，JavierEsparza，TobiasHeinde l，BarbaraK？on i g，anddVi taliKoziour a. 红黑树在2005年COSMICAH '05的Proc.会议记录见RR-05-04号报告（伦敦大学玛丽女王学院）。[2] PaoloBaldan，andreaCorrradini，anddBarbaraKöonig.语法分析是语法转换系统的一种技术在Proc. ofCONCUR Springer-Verlag，2001. LNCS 2154.[3] PaoloBaldanandBarbaraKöonig. 一个程序 是 针对 系统 的 一系 列应 用程 序。 在proc ICGT '02（InternationalConferenceonGraphTransformation），第14-29页。Springer-Verlag，2002. LNCS 2505.[4] E. Clarke，S. Grumberg，S. Jha和H. Lu，Y.和维斯反例引导的抽象细化。计算机辅助验证，第154-169页。斯普林格，2000年。LNCS 1855.[5] H. Ehrig，G.恩格斯，H. J. Kreowski和G.罗森伯格，编辑。图文法和计算的图形变换手册，第2卷：应用程序，语言和工具。世界科学，1999年。[6] H. Ehrig，H.- J. Kreowski，U. Montanari和G.罗森伯格，编辑。图文法和计算手册的图变换，卷3：并发性，并行性，和分布。世界科学，1999年。[7] BarbaraKéoniganddVitaliKozioura. AUGUR-atolthen ssys s t e n s ys t e s t a t e nsys t a t a t e n s t a t a te n s t a t a t ens t at aEATCS Bulletin，87：125-137，November 2005.出现在正式规范列中。[8] BarbaraKéoniganddVitaliKozioura.一种用于语法转换系统分析的新方法。在GT-VMT '06（图形转换和可视化建模技术研讨会）的论文集ENTCS。[9] BarbaraKéoniganddVitaliKozioura. Counterexample-guidedabstrenefine menteren e在TACAS '06的Proc.施普林格，2006年。LNCS。[10] W. Reisig. Petri Nets：An Introduction. EATCS理论计算机科学专著。Springer-Verlag，柏林，德国，1985年。[11] 我不想让你失望。 VerifikationdynamischerSysteme：ReguléareAusdrückezurSpezi kationverbotenerPfade。2004年9月，斯图加特联合大学出版社出版了一本书。 不。2192年。[12] ArendRensink，A'kosSchmidt，andD'anielVaro'. 用于解决问题的模式：两种方法的组合。 在proc ICGT2004：第二届国际图形转换会议，LNCS第3256卷，第226-241页，意大利罗马，2004年。斯普林格。[13] Grzegorz Rozenberg，编辑。图文法和计算的图形变换手册，卷1。世界科学，1997年。
我的内容管理
展开
