图转换系统中的时间约束优化和可达性分析方法

理论计算机科学电子笔记109（2004）137-147www.elsevier.com/locate/entcs带时间的SzilviaGyapay1，2A′kos Schmidt1 Da′nielVarro′1，3布达佩斯技术经济大学测量与信息系统系H-152 1布达害虫，Magyartudo'soküoru'tja2. ，Hungary摘要安全关键系统的设计通常需要同时满足多个逻辑和数值约束，以提供功能正确和最佳的目标系统。在本文中，我们提出了一种结合优化和可达性分析的方法，使用SPIN模型检查器[5]来处理用图变换系统建模的问题。首先，我们按照[9，10]将图转换规则编码到Promela（SPIN的输入语言）然后，我们限制有效的执行路径的时间顺序的转换序列的额外的逻辑条件。所需的可达性属性（作为逻辑条件）用于在新路径满足该属性时潜在地降低全局最佳成本变量。 该问题的最佳解决方案是通过一个单一的穷举运行的模型检查器编码的数值约束到一个动态LTL公式，以削减违反分支定界算法的非次优路径。保留字：图变换、优化、模型检测。1介绍最近，图转换系统（GTS）与时间的概念已经在[3]中引入，为大量使用超时，定时约束，延迟等概念的嵌入式和安全关键系统建模提供正式支持。此外，这些问题的正确性对于这些系统的成功运行至关重要。这种方法定义了1这项工作得到了匈牙利国家基金OTKA T038027的支持2电子邮件地址：gyapay@mit.bme.hu3电子邮件地址：varro@mit.bme.hu1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.062138S. Gyapay等人理论计算机科学电子笔记109（2004）137全局时间排序的变换序列，以捕获附加到顶点的时间值的一致性。由于违反这种时间限制通常是关键的，图变换系统的形式分析在实践中经常需要使用现成的分析工具（如模型检查器或定理证明器）来证明系统的功能正确性。最近的一些研究活动[1，6，10]一直专注于图转换系统的模型检测在[9]中，基于[10]的编码，报告了用于将图转换系统映射到Promela（模型检查器SPIN[5]的输入语言然而，需求通常需要构建一个同时是正确的和最佳的，即， 系统必须同时满足逻辑和数值条件。例如，安全关键系统中的一个典型要求为此，我们需要将可达性分析与优化相结合。组合技术的主要基础可以基于[8]，其中通过将分支定界技术嵌入模型检查器S引脚[5]来解决最优调度问题同样的问题已经解决了一个Petri网的基础上使用过程[4]中的网络综合优化算法在本文中，我们概述了一个组合的可达性分析和优化技术的图转换系统的时间。(i) 首先，我们推导出一个功能等价的转移系统（TS）的图转换系统没有时间跟踪[10]，收集所有潜在的规则应用程序。(ii) 然后，向每个转换添加附加条件，以将模型检查器遍历的执行路径限制为按时间排序的转换序列。(iii) 可达性属性（即，期望的目标配置）被编码为单独的Promela过程。如果在执行路径上达到了所需的配置，并且该解决方案的成本优于到该特定点为止找到的最佳解决方案的成本，则我们减少这个存储最佳成本的全局变量。(iv) 为了通过模型检查器的单次穷举运行找到最优解，通过分支定界技术修剪状态空间以获得次优解。分支定界技术被编码到要验证的属性中（声明当前成本最终将大于或等于每个执行路径上的最佳成本），因此它在模型检查过程中动态变化。S. Gyapay等人理论计算机科学电子笔记109（2004）1371392GTS中的带时在本节中，我们将演示如何使用图转换系统对优化问题进行建模。作为一个激励性的例子，我们讨论了一个车间调度问题（稍微修改过的版本），即[8]中讨论的个性化机器的例子该示例是AMETIST项目中进行的案例研究的简化版本2.1个性化机器问题空卡片个性化站个性化卡片perst=10perst=10perst=10perst=10移入pers_inpers_outt=1pers_inpers_outt=1pers_inpers_outt=1pers_inpers_outt=1移出t=1t=1t=1t=1 t=1t=1移位t=1移位t=1移位t=1移位t=1移位t=1第一小区输送细胞最后信元Fig. 1.个性化机器Personalization Machine问题是智能卡的个性化调度在图1中，描绘了个性化机器的示意图。空的智能卡通过传送带（由传送单元组成）传送到个性化站。个性化过程包括以下主要步骤（其中操作成本，即，它们所花费的时间也在图1中描述）：（i）卸载机将智能卡放在传送带的第一个单元上（使用卸载和转移操作）;（ii）传送机可以将卡转移到下一个单元作为单个移动。如果卡到达最后一个单元并且它还没有被个性化，则它将被发送到空卡并且在稍后的阶段中再次重新加载;（iii）卡可以通过自由的个性化站（pers in）从带上取下，卡的个性化立即开始，即，机器用个性化数据（pers）对卡片进行编程，并将其带回传送带（pers out）;（iv）最后，卡片由装载机从传送带的最后一个单元移除（移出和装载操作）。我们的目标是找到一个最佳的时间表来个性化n智能卡，m个性化站。卸载t=2载荷t=2装载机卸载机140S. Gyapay等人理论计算机科学电子笔记109（2004）137CC：ConvCell时间=t1conv_hold=假Lpers_outmyCellP：工作站pers_hold=truepers_holdC：卡时间=t2card_hold=truepersonalized=trueRT=max（t1，t2）CC：ConvCell时间=T+1conv_hold=true转换保持C：卡时间=T+1myCellP：工作站pers_hold=falsepers_hold个性化工作站pers_hold：boolmyCell卸载时间：intunl_hold：boollastCellfirstCell输送单元time：intconv_hold：装载机time：intload_hold：unl_hold转换_holdnextCell负荷保持卡time：intcard_hold：boolpersonalized：2.2定义静态结构：类型和实例图个性化机器问题的静态结构建模使用类型和实例图，这是传统的UML类和对象图的形式化的基于图的表示。类型图中的图节点对应于类，而边对应于关联。属性经常被解释为特殊节点。实例图表示建模的系统，并且它通过类型同态（形式化实例关系）连接到类型图。实例图中的图节点对应于对象，边表示链接，而属性在UML术语中称为槽。在图2的左边部分，个性化机器问题的类型图被描述为一个UML类图。 它由卡、卸载机、装载机、个性化站和传送带单元节点组成。 为了对操作成本进行建模，所有节点（个性化站点除外）都具有时间属性。时间属性表示逻辑时钟，用于记录在相应节点上应用的最后一个操作完成的时间。卡片（和其他对象）的当前位置和状态由边和属性表示，并带有holdpost fix。通过将个性化属性设置为真，卡被视为已处理。图二. 类型图和一个图变换规则2.3动态行为建模：随时间变化的图形转换图转换[7]通过替换实例图的一部分，提供了对类型化和属性化图模型的S. Gyapay等人理论计算机科学电子笔记109（2004）137141将特定模式与另一个图形进行匹配。在带时间的图变换[3]中，时间属性是一个逻辑时钟（通常），具有可以附加到节点的非负时间属性在定义时间如何以一致的方式以离散的步骤进行方面具有突出的作用。图变换规则p=（L，R）包含左侧图L和右侧图R，其中两个将规则p应用于实例图G，用R的像替换G中L的匹配。 这是通过（1）发现一个事件来执行的（2）去掉G中与L中不属于R的元素相匹配的部分，（3）对称地将新的节点和边粘到G上，这些节点和边可以映射到R上，但不能映射到L上，从而得到导出图H。图转换系统（GTS）由一组图转换规则组成，而图转换（序列）是从GTS中选择的一系列构造性规则应用，它从初始图模型演化系统。带时间的图变换系统由以这样一种方式操纵时间属性的规则组成，1.局部单调性：R在H中出现的所有时间值都高于L在G中出现的任何时间值。2.统一时间戳：R在H中出现的所有时间值都相等。这个统一的时间戳就是规则应用的时间。3.时序变换序列：如果序列中连续规则应用的时间单调增加，则图变换序列称为非正式地，条件1确保规则的应用需要正时间。条件2说明规则应用的原子性，即，同时观察右侧的所有效应。 条件3表示系统应该沿着可以由中央调度器（具有系统的全局图像）执行的时间排序的虽然条件1和2可以在编译时通过图转换规则的结构来满足，但条件3只能在运行时通过仔细选择（i）要应用的下一个规则和（ii）规则的下一次出现来为了空间的考虑，我们只介绍了个性化机器问题的一个规则，当个性化机器在个性化之后将卡放回传送带时。如果（1）存在已经被个性化的卡（C.personalized=true），（2）它还没有被授权人释放，（3）它没有被授权人释放，（4）它没有被授权人释放，（5）它没有被授权人释放，（6）它没有被授权人释放，（7）它没有被授权人释放，（8）它没有被授权人释放。142S. Gyapay等人理论计算机科学电子笔记109（2004）137站还没有（在卡和个性化站之间存在个人保持链接），以及（3）连接到个性化站的传送单元是空的（CC.卡保持=假）。规则的应用产生个性化卡被放回传送带的实例图：（1）卡被个性化站释放（P.pers hold=假，并且pers hold链接被删除），以及（2）卡被放回传送带上（在单元和卡之间创建conv hold链接，并且设置相应的hold属性），以及（3）卡和传送单元的时间戳被设置为max（t1，t2）+1。注意，rule out满足局部单调性和统一时间戳条件：（1）R中的时间戳大于L中的时间戳，以及（2）R中的所有时间戳都相等。3从带时间的GTS到过渡系统转换系统（TS）是一种常见的数学形式，用作各种模型检查工具的输入规范，其中系统通过执行非确定性条件类规则来操作状态变量。图转换系统与时间编码成一个行为上等价的TS在一个两步的过程。首先，我们收集图转换规则到TS中的转换的所有潜在应用，以正确处理单个图转换步骤[9，10]。然后，通过对规则应用的时间（戳）附加逻辑条件，将有效的执行路径限制为按时间排序的转换序列。由于空间限制，我们只粗略地将图转换规则编码到目标TS中的转换中，并省略了[10]中讨论的几个概念细节（例如由元模型驱动的状态变量的声明或由初始模型驱动的初始化阶段）。3.1GT规则的编码图变换规则的潜在应用被编码成对应TS的语义上等价的转换（其中TS的转换由保护和状态变量更新组成行为等价意味着当GT规则适用于某个匹配时，相应转换的保护应该评估为true，从而可以触发转换（反之亦然）。• GT规则的所有潜在匹配在编译时被收集到转换的保护中。这些警卫主要由S. Gyapay等人理论计算机科学电子笔记109（2004）137143{›→}L图施加的逻辑条件和属性条件。此外，在双推出方法的情况下，守卫可能还需要包含标识和悬挂条件[2]。• 将规则应用于某个匹配的效果被编码为状态变量更新。这些更新应该处理是否创建或删除某个图形节点或边，或者是否为属性分配了新值虽然这种编译时预处理可能很耗时，但由于必须找到规则的所有潜在匹配，因此我们只需遍历状态空间的一小部分。这是因为图变换规则定义了对系统状态的局部修改，因此与模型检查期间遍历整个状态空间所需的时间相比，它通常可以忽略不计。下面描述了当应用在潜在匹配CC上时，对（图2的）规则输出进行编码的等效Promela转换4作为演示cc1，Pp1，CC1（表示卡C1的个性化已经在站P1处完成，因此卡C1被放回到传送单元CC1上）。：：原子{convCell[cc1]conv_hold[cc1]==falsemyCell[p1][cc1]persStation[p1]pers_hold[p1]==truepers_hold[c1][p1]card[c1]card_hold[c1]==truepersonalized[c1]==true->pers_time’[cc1] = max(time[cc1]+1, time[c1]+1);在保护中，我们检查对应类型的节点和边的存在（例如，convCell[cc1]和myCell[p1][cc1]）和属性条件（例如personalized[c1] == true）。状态变量的更新是根据GTS随时间变化的情况，去除pers保持边沿，产生新的conv保持边沿，并更新时间3.2确保时间有序前面的编码将时间属性作为GTS中的常规属性进行处理。这样，在目标TS中存在不按时间排序的执行路径。为了将执行路径限制为按时间排序的转换序列，每个转换都需要几个扩展。我们引入了一个新的状态变量prev time，它存储了前一个规则应用程序的时间（戳），因此它可以被上的所有转换全局访问。4注意，[10]中的原始技术使用了进一步的优化来减少状态变量的数量，并消除了当前论文中省略的死转换。144S. Gyapay等人理论计算机科学电子笔记109（2004）137只有一条路由于我们的目标是将有效的执行路径限制为按时间排序的路径，因此每个转换的保护都扩展了一个文字，以检查当前规则应用程序的时间是否大于（或等于）以前的规则应用。如果保护评估为真（即，序列保持时间顺序），则状态变量Prev_Time也被更新以存储当前规则应用的时间。在rulepers out的情况下，需要以下扩展来转换前一个示例。max（time[cc1]，time[c1]）+1>= prev_time&&... ->prev_time' = m a x （ t i m e [ c c 1 ] ， t i m e [ c 1 ] ） +1 ; .注意，由于图变换规则的结构通常意味着条件1和2，因此只有条件3必须被编码到Promela描述中。总之，为了将我们的研究限制在时序变换序列上，需要对转换系统本身进行更改，但这些更改是独立于工具的，因此它们可以应用于具有基于转换系统的输入语言的任何模型检查器。同时，第4节中介绍的技术仅适用于S引脚。给定从具有时间的GTS导出的过渡系统，检查器S引脚可以自动验证任意LTL公式的有效性通过这种方式，我们能够决定某些属性（需求）是否在GTS的任何时间顺序执行路径上保持。4组合优化和可达性分析为了同时执行优化和验证，我们将自己限制在用作功能需求（逻辑约束）的可达性属性上。因此，我们的最终目标是找到一个最佳的转换序列（ex-paths），导致由可达性属性定义的期望情况。我们现在采用[8]的技术来实现S引脚的优化。在可达性属性中，我们询问所期望的情况是否在系统的至少一个执行路径上的至少一个状态中变为真因为-通常，在LTL术语中，可达性属性具有G-p的形式，其中p是描述期望情况的属性。如果模型检查器发现属性Gp有效，则期望的情况不可达，否则期望的情况是可达到的，并且模型检查器将导出导致这种情况的状态序列作为反例。在SPIN 中，LTL 公式被转化为具有高优先级的特殊Promela 过程（automata）。事实上，可达性属性可以被解释为一个特殊的错误转换（称为never claim），如果在任何时候触发，它会中断模型检查器的运行并检索错误跟踪。S. Gyapay等人理论计算机科学电子笔记109（2004）1371454.1更新解决方案的最佳成本然而，在优化的情况下，这种错误转换的触发不应该中断模型检查过程，它只表明找到了满足可达性属性的当前执行路径的总执行时间）小于先前找到的执行路径的最佳成本最后，模型检查器应该继续调查下一个执行路径。为了实现这种行为，我们需要依靠SPIN4.0，它支持通过以下原语将嵌入式C代码包含到Promela模型(i) c state：向Promela模型添加新的C变量;（ii）c expr：在guard中评估C表达式;以及（iii）c code：将任意C代码片段作为原子语句添加到Promela模型。(i) 首先，我们使用以下公式在Promela模型中定义全局变量最佳成本：c state构造如下：cstate“int best cost”“Hidden”。范围存储在状态向量中，并且对于所有执行运行都是全局(ii) 变量最佳成本在验证开始时初始化为MAX COST（最坏情况下的进度成本估计）。#defineMAX_COST1000init{c_code { best_cost= MAX_COST;}}(iii) 每当找到一个新的解决方案，即，在可达性属性的错误转换中，执行路径的成本（时间）（即，变量prev时间）与迄今为止的最佳成本进行比较。如果prev时间较小，则我们找到了更好的解决方案，因此可变最佳成本为减少和跟踪保存。下面的Promela代码表示可达性属性reach prop，它声明每张卡c1，... CN最终应该是个性化的#define reach_prop（personalized[c1]&&... &&personalized[cn]）reach_prop->c_code {if（now.prev_time best_cost）{ best_cost = now.prev_time;/* 进一步旋转特定代码以保存当前跟踪 */}}4.2使用动态LTL公式的分支定界分支定界[11]是一种用于解决离散和组合优化问题的方法分支定界方法的本质是通过构造一个枚举来枚举所有可能的解146S. Gyapay等人理论计算机科学电子笔记109（2004）137树当构建树时（即，状态空间），我们可以停止考虑执行路径（部分解决方案），如果它是肯定的，所有路径通过这个状态(i)要么导致无效的解决方案（逻辑切割），要么（ii）成本更高最佳路径（numerical cut）遵循[8]的指导方针，我们将分支定界技术编码到要由SPIN验证的属性中。我们检查成本（即，形式上，对应的LTL是F（较高成本），其中到达属性是期望的可达性属性，较高成本被定义为#define higher_cost（c_expr { now.prev_time >= best_cost}）当检查F（较高成本）时，模型检查器枚举所有解决方案（即，导致期望情形的时间排序的变换序列），但是每当（i）执行路径的成本超过最佳成本（即， prev time>best cost），或者（ii）当前路径是具有新的（更优的）最佳成本的解决方案（因此prev time = best cost），或者当到达属性在某个路径上永远不能满足时的逻辑切割由于每当找到满足可达性的更优解时，可变最佳成本就会减少，因此正在检查的LTL公式在验证期间动态变化。5结论在本文中，我们提出了一个同时优化和验证的系统建模为GTS与时间。通过这种方式，我们能够通过使用模型检查器找到导致期望系统配置（由可达性属性定义）的最佳时序变换序列S针。作为我们目前研究的下一步，我们的目标是评估所提出的技术对基准示例的实际限制。引用[1] Balda n，P. 和B。K？nig，应用程序针对以下系统的graphtranbe haviour：A. Corradini，H. Ehrig，H.- J. Kreowski和G. Rozenberg，编辑，Proc. ICGT 2002：第一届国际图形转换会议，LNCS2505（2002），pp. 14比29[2] Corra d ini，A. 、乌桕属U. 我不知道，F. Rossi，H. Ehrig、R. 他叫M. 刘伟，“图变换的基本概念与双推出方法”，《世界科学》，1997年，第10163[3] 你 好， S 。 、 R.HecelandD. Varr'o ， Graphtransformationwitime ： Causallity yandlogicalclocks ， in ： A.Corradini ， H. Ehrig ，H.- J. Kreowski 和 G. Rozenberg ， 编辑 ，Proc. ICGT2002：第一届国际图形转换会议，LNCS2505（2002），pp. 120-134S. Gyapay等人理论计算机科学电子笔记109（2004）137147[4] 贾佩、S.和A.Pataricza，Petri网模型可达性分析的优化方法，在：G。Tarnai和E. Schnieder，editors ， Formal Methods for Railway Operation and Control Systems （Proceedings ofSymposium FORMS-2003，Budapest，Hungary，May 15-16）（2003），pp. 53比60[5] Holzmann，G.， 模型检查器SPIN，IEEE软件工程学报23（1997），pp. 279-295.[6] Rensink，A.，模型检验图文法，M. Leuschel，S. Gruner和S. Lo Presti，editors，Proc. of the3rd Workshop on Automated Verification of Critical Systems（AVOCS 2003），TechnicalReport150-160.[7] 罗森伯格，G.，编辑，[8] Ruys，T. C.的方法，使用SPIN 4.0分支定界的最优调度，在：Proc.10th International SPINWorkshop，LNCS2648（2003），pp. 1比17[9] 我的天啊。 和D. Vo，CheckVML：Atoolforormodelcheckingvisualmodelinglanguages，in：P. Stevens，J. Whittle和G. Booch，editors，Proc. UML 2003：6th International Conferenceon the Uni Fied Modeling Language，LNCS2863（2003）. 92比95[10] 好的，D。，Automatedformalverificationofvisualmodelinglanguagesbymodelchecking，Journalof Software and Systems Modelling（2003），被接受为Special Issue on Graph Transformationand Visual Modelling Techniques。[11] 温斯顿 ，W 。 L. ， “Operations Research - Applications and Algorithms,” Duxbury Press,Belmont, California, USA, 1994, 3rd