基于tableau规则的局部CTL模块检测方法的有效性验证 在开放系统中的应用.

理论计算机科学电子笔记176（2007）125-141www.elsevier.com/locate/entcs本地模块检查CTL规范Samik Basu1艾奥瓦州立大学Ames，美国Partha S Roop，Roopak Sinha2，3奥克兰大学电子与计算机工程系新西兰奥克兰摘要模型检查是一种众所周知的技术，用于使用时序逻辑规范来验证有限状态模型。虽然模型检测适用于转换系统（也称为封闭系统），但它不适合开放系统（也称为反应系统），因为在验证过程中必须考虑环境中的非确定性。 模块检查是一种验证开放系统其具有封闭（内部）和开放（环境或外部）状态。 已经证明文[10]证明了模块检验分支时间逻辑CTL的复杂性是EXPTIME-完全的。模块检查的方法是全局性的，并且该方法试图确定所讨论的属性在所有可能的环境中都有效。本文提出了一种基于tableau规则的局部CTL模块检测方法。所提出的方法试图确定一个单一的环境，在该环境下，对给定模块的属性的否定是满意的。因此，这样的策略导致了模块检查的局部方法，在这种方法中，我们只探索与证明属性的否定可以使用算法也生成的适当见证（环境）在给定模块上得到满足相关的状态。 虽然我们的算法的最坏情况下的复杂性是相同的早期的复杂性，我们表明，实际实施所提出的方法是可行的，并产生更好的结果比全球的方法。保留字：模块检查，开放系统，基于表的验证1介绍反应式系统[7，13]是开放系统，在执行非终止控制程序的同时持续与其设备交互。实例包括1 电子邮件地址：sbasu@cs.iastate.edu2电子邮件：p. auckland.ac.nz3电子邮件：rsin077@ec.auckland.ac.nz1571-0661 © 2007 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2006.02.035126S. Basu等人理论计算机科学电子笔记176（2007）125操作系统、通信协议、导弹和航空电子系统以及用于核电站和简单家用电器（如微波炉、DVD播放器和洗衣机）的控制器。这些应用需要仔细的分析、设计和验证技术，因为它们通常是安全关键的。因此，在这些系统的设计、开发和验证中经常使用形式化技术[16，11，5，6，3，12，15]。形式化技术使用精确的语法和语义来定义系统的规范和模型，以便对正确性，可靠性和安全性等属性进行严格的验证。随着嵌入式系统的出现和广泛使用，这是无处不在的反应式计算系统，从简单的家用电器到非常复杂的应用在航空电子和国防，在反应式系统的设计形式化方法的需求正在增长。验证反应系统的一种非常常见的方法是模型检查。模型检查器将某些时态逻辑[14]中的公式作为期望的属性，并对系统的有限状态模型（称为Kripke结构[3]，一类特殊的有限状态机）进行形式分析模型检查过程本质上是对系统的有限状态模型的自动可达性分析任务。这个任务要么以证明时态属性对模型有效而终止，要么在失败时生成一个反例。在可达性分析阶段，模型检查器假设最终启用了模型的任何给定状态的所有转换。这一假设是基于模型被认为是封闭的这一事实，即， 所有国家系统是纯内部的，并且是系统基于一些内部计算来选择进行哪个转换。这种分析方法虽然适用于封闭的转换系统，但不适用于开放的反应系统。一个开放的系统与其环境保持着持续的交互。因此，这种系统的状态空间可以被划分为一组开放的状态（也称为外部或环境状态）和另一组封闭的状态（也称为内部或系统状态）[8，9]。环境状态对开放系统的外部环境中的事件做出反应，并且环境被认为是异步和不可控的。另一方面，系统状态不接受外部环境的输入，系统会根据内部决策（例如变量的值或函数返回的结果）自动选择其中一个转换Kupferman等人最近表明，由于环境状态的存在以及在规范中考虑分支公式时，模型检查可能对开放系统是不够的[9]。所提出的技术，称为模块检查，考虑到异步环境，同时做分支时间逻辑的证明。[6，5]进一步讨论有关开放系统验证问题本文阐述了模块检查反应式系统的必要性，并提出了一种替代方法，模块检查，有效率的实现途径相比，原来的方法。我们首先说明了模块检查的必要性，其次是我们的本地模块检查方法。S. Basu等人理论计算机科学电子笔记176（2007）1251271.1激励性示例-被收购方布鲁尔验证问题考虑一个如图1所示的简单的合作伙伴酿酒商模型。在此图中，环境状态用椭圆表示，而系统状态用圆圈表示。任何状态的每个转换都由从1开始的自然数标记。酿酒师提供五杯或十杯中杯或浓杯的咖啡。用户可以选择咖啡的杯数（使用开关作为输入）和咖啡的强度（使用另一个开关）。酿造器在接通之前通常处于关闭状态。因此，由命题OFF标记的初始状态是环境状态。一旦啤酒酿造器被打开，它就进入由命题CHOOSE标记的状态。这又是一个环境问题。在这种状态下，用户可以选择咖啡的杯数和咖啡的强度。根据选择（两个开关导致四种不同的可能性），酿造机进入以下任何一种状态： （五，中等），（五，强），（十，中等）或（十，强）。 一旦做出选择并且相应的状态当达到设定值时，必须打开冲泡周期开关以开始冲泡。因此，上述四种状态也都是环境状态。 一旦设定了冲泡周期，冲泡器就转换到标记为BREW的状态。这种状态是一种系统状态，因为不需要来自环境的输入来取得进展。在预定的时间段（其是冲泡过程所花费的时间量）之后，冲泡器从冲泡状态自动转换到完成状态。标记为DONE的状态也是一个系统状态，因为brewer基于一些内部条件采取两个可能的分支之一。如果检测到任何错误（比如没有足够的牛奶或没有奶粉），则转换到错误状态（标记为ERROR）。可替代地，酿造者可以达到标记为“服务”的状态，其中为所选择的实际被酿造者提供服务。CTL是一种分支时间时序逻辑，已被证明是非常有效的模型检测。让我们考虑以下CTL属性：AGEF（TENSENDAAF（SERV ESENDAERROR）），要求从任何状态都可以最终选择十杯咖啡，一旦选择，十杯咖啡将在未来。请注意，模型检查器将始终返回此问题的真实答案。但是，考虑以下情况。由于安装啤酒酿造器的工作场所的成本削减，不允许一次酿造十杯咖啡（这已经通过通告强制执行，十杯开关被掩盖）。因此，将不允许任何用户从CHOOSE状态进行此选择。因此，它将不可能保证选择十杯咖啡，因此该物业未能保持咖啡酿造模式。如果所有用户都请求五杯咖啡或茶（没有用户请求十杯任何饮料），也可能违反此属性。在这种情况下，即使机器能够分配十杯茶或咖啡，其操作的环境也会有效地禁用我不想这样做。这个属性说明，由于环境状态的存在，可能不总是能够满足分支时间时间属性。由于开放系统的环境是异步的，因此是不可控的，128S. Basu等人理论计算机科学电子笔记176（2007）125s0关闭1S1选择1S2S32 S 43s54五，地中海五，STR10，地中十，STR11S61111BREW1S7做12S8误差S9服务Fig. 1. 以可口可乐啤酒厂为例段可能永远不能实现某些期望的转变，从而导致属性的失效。因此，这个例子激发了模块检查问题：我们如何确保给定的属性在假设不确定环境的已知模块（具有环境和系统状态的模型）上保持不变模块检查的基本思想是证明该属性对环境状态中所有可能的选择都有效。 换句话说，模块检查问题是决定CTL公式在为所有可能的环境E提供的模M上，使满意。 这里，M× E表示模型和环境并行运行（稍后正式化）。这可以表示如下：模块检查，由M表示|因此，这就相当于决定是否要放弃。M×E|= 0;即，M| = o优惠券E。M× E|Kupferman等人[ 10 ]已经表明，时态逻辑CTL的模块检查问题是EXPTIME-完全的，不像模型检查问题的多项式复杂性。这种复杂性的原因可以从上面的等式直观地看出，因为必须对所有可能的环境进行证明。这与模型检查不同，在模型检查中，系统是封闭的，因此可达性证明在不考虑任何非确定性的情况下进行。环境保护虽然这听起来像是个坏消息，但通过下面的观察，模块检查的实际实现进一步地，从等式1，我们陈述：M| = o优惠券E J. （M× E J|=最惠M × E J|（2）S. Basu等人理论计算机科学电子笔记176（2007）125129在上面的例子中，可以在公式内部推动对布尔运算符的求反，这样所有的临时和布尔运算符都不会被求反。此外，由于E j的存在，确保M| = o，E J充当违规的见证人。这样的证人可以用来提供有用的见解的原因，违反了开放系统的所需的属性。这个过程的主要优点是，我们只寻找一个环境，使用它我们可以证明公式不满足。稍后我们将说明，我们可以使用一组tableau规则来本地执行EJ的计算。这种局部计算类似于在线模型检查[1]，其中构造了验证下系统的状态空间在需求驱动的基础上。尽管局部模块检查的最坏情况复杂度仍然受[10]的结果限制，但我们证明了所提出的局部模块检查方法可以产生更好的实际结果。本文的主要贡献是：(i) 我们提出了一套健全的和完整的tableau规则的本地模块检查。所提出的方法确定单个见证（环境），以便在见证下满足给定CTL属性的否定。证明只沿着生成见证所需的一组局部状态进行。(ii) 我们通过扩展NuSMV [2]开发了一个本地模块检查器。局部模块检查已被比较的最大环境下，给定的CTL属性是满意的，以证明所提出的方法的性能增益的生成。基准测试是NuSMV的示例，包含环境和系统状态。本文的其余部分组织如下。第二部分介绍了基本理论。第三部分阐述了CTL局部模块检查，并给出了系统和环境状态的tableau规则。第4节描述了本地模块检查器的实现，第5节包含从它获得的结果。结论性意见在第6节中。2预赛Kripke结构系统行为用Kripke结构M=（S，s0，→，P，L）描述，其中S是状态集，s0∈S是起始状态，→S×S是转移关系集，P是与M相关的命题集，L：S→2P是将每个状态映射到命题集的标记函数.时态逻辑：CTL。系统的属性使用分支时间时序逻辑CTL定义。CTL公式使用时间和布尔运算符在一组命题上定义如下：φ→ P|欧元/英镑|TT |ff |φ ∧ φ |φ ∨ φ |AXφ |EXφ |A（φUφ）|E（φUφ）|AGφ|EGφ130S. Basu等人理论计算机科学电子笔记176（2007）125请注意，CTL通常允许对时态和布尔运算符进行否定运算。然而，我们限制自己验证CTL公式的否定只能适用于命题。用满足CTL公式的Kripke结构M中的状态集M给出了CTL公式的语义，记为[M]]M见图二、[[p]] M={s |p ∈ L（s）}M={s |p/∈ L（s）}[[tt]]M=S[[]]M=Φ[[]]M=[[]]M[[]]M[[]]M=[[]]M[[]]M[[AX]]M={s|s→sj[[EX]] M={s|s → sj[[A（U）]]M={s|s= s1→s2→.. . 萨卡什维利角SJ|= i AFstate=busy）0.02/F/0（2）0.05/S/0环（7）（AGAF门1.输出） 阿佳夫！门1.输出）0.01/F/0（2）0.02/S/0柜台（8）AG（位2，值 = 0）0.00/S/0（5）0/F/0（10）第一章AGAF（十个EFServe）0.0084 S/3（7）0.001/S/0中文（简体）AGEF（（M CP.missionaries= 0）（MCP.cannibals= 0））0.001/S/5（2）0.05/S/0中国（1758）trueAU（step= 0）1.250/F/0（21）1.290/S/0定期（3952）AG（aux=/第11页）9.580/S/0（701）51.270/F/0中文（简体）5.持久性7.73/S/0（223）3704/S/960中文（简体）AG（（e − 1.r.out = 1|e − 2.r.out = 1）（e − 1.r.out = 1|e − 3.r.out = 1）（e− 2.r.out= 1|e− 3.r.out = 1））5.490/F/0（141）41.17/S/790pqueue（10000）pqueue（10000）EG（out l[1] = 0）AF（out l[1] = 0）34.20/F/0（1904年）34.930/F/0（2101）35.130/S/034.960/S/0手机（45025）AGtrueAU（b0 = 0）12.720/S/0（231）34.190/S/1空闲（87415）trueAU（step= 0）77.190/F/0（38088）79.920/S/0中文（简体）EF（sender.state=get）130.77/F/0（59808）133.880/S/0表1实施结果第三列。第四列包含生成满足给定CTL属性的最大环境的结果6。请注意，对于许多模块，原始属性及其否定都在不同的环境下得到满足。大多数模型有多个起始状态。在这些情况下，本地模块检查器（和最大见证生成器）在每个开始状态上执行。具有密集转换关系的模型，如dme1和syncarb5，需要更多的时间。具有相对稀疏的转换关系的模型（如abp4和idle）花费的时间较少，尽管它们具有更高数量的可达状态。当模块（abp4，pqueue，periodic）满足原始CTL公式时，本地模块检查器花费的时间稍长6结论模块检测扩展了开放系统的模型检测。 已经表明在[10]中，分支时间逻辑CTL的模块检验的复杂性是EXPTIME完全的。上述模块检查方法生成所有可能的环境，以便模型和环境的组合满足CTL属性。在本文中，我们提出了一个本地的方法来检查CTL模块。所提出的方法试图确定一个见证人环境，以便证明人和模型的组成满足对属性的否定。当这是可能的，原始属性不满足模块。我们已经发展出一套完善的画面规则，6结果的格式为TimeTaken（秒）/Result（SUCCESS或FAILURE）/Nu