基于UML的铁路联锁系统中的多对象检查生成反例的方法

理论计算机科学电子笔记190（2007）61-72www.elsevier.com/locate/entcs通过多对象检查生成场景MaikKollmann布伦瑞克技术大学信息系统研究所Mühlenpforrdtstrae23，38106Braunschweig，Germany袁文汉2不伦瑞克铁路系统工程与交通安全技术大学Pockelsstraße 3，38106 Braunschweig，Germany摘要如今，许多系统都是应用各种UML符号来表示（技术）系统的结构和行为。此外，对于铁路联锁系统（RIS）等安全关键系统，需要满足安全要求。基于UML的铁路联锁系统RI）作为设计和开发RIS的一种方法。它由基础设施对象组成，并使用UML对系统行为进行建模。通过Rhapsody仿真验证了该设计。自动验证技术，如模型检查，已经成为证明基于状态的系统正确性的标准。不幸的是，模型检测的一个主要问题是状态空间爆炸，如果太多的对象必须考虑。多对象检查通过一次检查一个对象来避免状态空间爆炸。我们提出了一种方法来增强多对象检查生成反例的顺序图的时尚提供基于模型的测试方案。关键词：场景生成，反例生成，状态建模，多对象检测，基于UML的铁路联锁系统1介绍如今，在系统开发的不同阶段，统一建模语言（UML）符号[19]被用作建模工具来指定（技术）系统的结构和行为。这些系统包含通过通道或总线进行交互的组件或对象，以提供特定的功能。在1电子邮件：M. tu-bs.de2电子邮件：Y. tu-bs.de1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.08.00662M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）61此外，对于像铁路联锁系统（RIS）这样的安全关键系统，需要满足安全要求。安全关键系统提供安全操作的证明确定了这种系统是否符合所需的安全完整性等级（SIL）[5，2]。一般来说，安全关键系统要求达到SIL 4，即最高级别。根据EN50128 [5]，SIL 4 RIS强烈建议证明RIS软件满足的安全要求达到了可容忍的水平。RIS负责为计划通过或停靠火车站的列车建立安全路线。安全路线确保列车不会驶入已被其他列车占用或可能被其他列车占用的轨道一条安全的路线可以确保沿线的点和信号等基础设施元素的正确设置。这些元素可以使用UML类图和UML状态机建模[15，3]。下一步是证明混凝土联锁模型工作正常，并且符合安全要求。这种要求是没有冲突的路线，等自动验证技术，如模型检查已成为一个标准，证明基于状态的系统的正确性。不幸的是，模型检查会导致状态空间爆炸问题，如果有太多的对象必须考虑。多对象检查[11]通过其每次检查一个对象的性质来避免状态空间爆炸。多对象检查依赖于健全和完整的多对象逻辑D1和D0[9]，这些逻辑基于众所周知的逻辑，如CTL或LTL。D1应该是更直观的具体说明，因为相互作用不同的物体之间可以被指定。然而，它不能直接应用模型检查来验证。D1中的公式可以转化为D0公式的等价集合.每个检查条件都绑定到D公式中的特定对象.因此，D0公式可以通过模型检验自动验证。多目标检测与传统的检测模型有着相似的性质正在检查它们提供了一个自动的证明，证明某个（安全）属性成立。此外，如果检查条件不成立，模型检查提供了分析系统模型的机会。如果模型违反了检查条件，多对象检查会从模型检查工具中为最外层的对象提供一个反例。考虑到上述与其他物体的通信，必须手动分析这个反例轨迹。我们提出了一个基于混合器的方法来合成一个多对象的反例，是封闭的对象之间的相互作用。像SPIN [14]或SMV/NuSMV [18，4]这样的模型检查工具包含了说明模型不满足检查条件的能力，这些检查条件具有所涉及状态的我们认为，从用户的角度来看，像消息序列图这样的图形表示是最方便的，除了为某些场景提供图形化表示之外，序列图已经成功地应用于生成测试用例[7]。在这篇文章中，我们提出了一种方法，自动生成测试用例的系统规格的基础上，而不是手动推导它们。M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）61632铁路联锁系统RIS通常根据车站的布局进行专门设计。当车站的布局改变时，相应的RIS必须修改。这就造成了资源和时间的巨大浪费[23]。为了减少修改RIS的工作量，可以采用面向对象的方法来开发RIS。该方法只需在车站布局发生变化时指定新的对象相邻结构，而无需对整个联锁系统进行地理联锁作为联锁系统的内部逻辑，联锁系统由基础设施要素作为对象组成。这些对象通过事件和动作彼此交互，以开发安全路线。可以通过使用状态建模来捕获对象、事件和动作。在文献[1]中，提出了Statemate [13]，并将其应用于联锁系统的功能需求建模相反，在这项工作中，UML状态机用于状态建模。应用地理联锁并以UML为规范工具开发的铁路联锁系统称为基于UML的铁路联锁系统（UML-based RI）。图1显示了用于检查开发基于UML的RI的可行性的火车站CStadt。车站内有不同类型的基础设施：轨道、点和信号。Fig. 1. CStadt站轨道布置轨道是列车运行的基本基础设施要素铁路车辆在轨道上的许可移动可分为列车移动和调车移动。列车只允许在正线上运行，而组成列车，称为调车运行，只在侧线上进行[20]。在图2中，主要轨道是GA1，GA2，GA3和GA4。在基于UML的RI的当前模型中，仅分析列车运动。列车也可以通过道岔或交叉口转向另一条轨道，而不是只向前直行。 道岔和道口由点组成。点（例如，W1）可设置为左右位置。为了保证列车能够驶入当前轨道，RIS需要保证道岔的正确位置图二. 基于UML的RI64M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）61沿着轨道，人们可以找到另一种基础设施组件：信号。信号（例如，P1）可用于通过显示方面来控制列车运行。在这项工作中将考虑两种类型的方面，他们是明确的和停止方面。某些信号还可以指示相应轨道区段的允许速度。在当前工作中不考虑速度指示如前所述，RIS的主要任务是为接近的列车制定安全路线。安全路线有两个要求。一是合理设置了沿线基础设施要素。例如，这些点被设置在正确的位置，并且没有其他列车可以从发散方向驶入安全进路。侧翼保护是为了防止其他列车通过道岔驶入安全路线。 此外，没有发出任何冲突路线 与此同时，安全路线。这意味着属于路线的基础设施元素只能由一列火车专用。如果接近列车的请求路线满足这些要求，换句话说，它是一条安全路线，那么该路线和沿着该路线的基础设施元件将专门为该列车锁定。没有其他列车可以使用相同的路线，因此可以避免碰撞。上述安全要求可以通过执行两个程序来确保：检查基础设施要素的可用性和为路线提供安全防护。3多目标系统与多目标检测处理状态空间爆炸的可能解决方案之一是开发一种方法，使得可以在不建立完整状态空间的情况下验证条件，并且在验证期间仅考虑条件中涉及的对象的那些状态变量。在这种方法中，涉及单个对象的公式的正确性可以通过局部检查该对象的状态空间来验证当有更多的对象被定义时，一个公式被称为全局条件。这种全局条件可以分解为每个对象的一组局部条件和对象之间的通信全局条件的正确性可以通过检查这些局部条件和对象之间的通信的存在来多目标检测是一种包含上述思想的方法。该方法不需要建立完整的状态空间，就可以有效地验证基于状态的多目标系统。在多目标检测中，系统由多个对象组成，对象之间以类似RPC的方式同步通信。对象之间的通信必须在验证之前指定。每个对象都有一个描述其属性的签名，例如，其属性，操作和有效命题。该签名可以例如在有限状态机（FSM）中捕获。设I是表示顺序对象的恒等式的有限集合稍微误用了术语，当我们指具有单位i的对象时，我们说对象i。每个对象i∈I都有一个单独的原子状态谓词符号集合Pi，即它的签名。在应用中，这些谓词符号可以表示属性的值，M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）61651111我1FiLT L* =i.LiLT L：：= i：LiLT L | i! LiLT L | i? LiLT L|1 1 1 1i：lastLiLT L | i! 最后LiLT L | i? 最后LiLT L|1 1 1i：untilnowLiLT L | i! 直到LiLT L | i? 直到LiLT L|1 1 1LiLT L ：：=|Pi|LiLT L | LiLT L ∧ LiLT L | LiLT L ∨ LiLT L |1 1 1 1 1 1LiLTLLi LT L | Li LT L ⇔ Li LT L |1 1 1 1XLi LT L |FLi LT L |GLi LT L |Li LT L ULi LT L|1 1 1 1 1YLi LT L |OLi LT L | Li LT L S L i LT L |Li LT L S Li LT L|1 1 1 1 1iLTL1@：J |@！J|@？J|CiLT L：：=... |......这是什么？|...（j∈J，J<$I\{i}）图三. 多目标逻辑D1的定义（与局部逻辑LTL）动作被启用、哪些动作已经发生等。我们使用多目标逻辑D1（参见 如图3所示，在[9，10]中，逻辑i.对于每个对象i ∈ I，LiLT L在签名Pi上。 D允许使用公式jLT L1jLTLjLT L1j：L1，j！L1，j？L1等，对于任何其他对象j∈I作为子公式，i.LiLT L. 这些成分称为通信子公式。涉及多个对象的全局条件由多对象逻辑D1指定。逻辑D1允许指定一个对象局部填充的时间公式或命题。它还允许指定时间如果其他对象之间存在同步通信，例如，公式o1。（<$EF（state=critical）o2：（state=critical））表示当前在对象o1和o2之间存在同步通信，使得o2为o1保证o2是在临界状态下（cf.图4）。（状态=临界）在该方法中被称为通信子公式。图四、对象o1和O2必须不驻留在的关键部分合在一起：o1. （<$EF（state=critical）2：（state=critical））有一个子逻辑的D1称为D0（参见。图5）。涉及与不同对象通信的公式不能直接用D0表示。然而，两个对象之间的同步通信可以用D0中对象的属性显式指定。[9]提出了一种变换，将全局D1检查条件分解为D0条件和通信符号的集合（参见图6）。这些符号必须根据通信要求与现有符号匹配。此外，D0条件可以在局部验证。非正式地说，DC66M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）610Di：：= i.LiLT L | i.Ci000LiLTL：：=|Pi|LiLT L | LiLT L ∧ LiLT L | LiLT L ∨ LiLT L |0 0 0 0 0 0LiLT L LLL L | Li LT L ⇔ Li LT L|0 0 0 0XLi LT L |FLi LT L |GLi LT L |Li LT L ULi LT L|0 0 0 0 0YLiLT L |HL i LT L |Li LT L S L i LT L |Li LT L S Li LT L|0 0 0 0 0@：J| @！J|@？J我：：=... | (Pi⇒ j. Pj）|. . . ...这是什么？（j∈J，J<$I\{i}）图五. 多目标逻辑D0的定义（带有局部逻辑LTL）符号是由内而外确定的D1公式中的i ∈D0公式10j成立。 这在[17，11]中详细说明。ψ 我是阿吉（...） j：（）.. . ）（你好（...） 问：j.. .）（q：i）见图6。 D1到D0变换3.1模型检测在[11]中，已经成功地证明了多目标检查使用模型检查来确定通信符号并根据通信要求与现有符号进行匹配。模型检验包括根据检验条件（也称为公式（M））验证系统|= φ，M是模型φ为公式）。需要验证的系统被指定为（标记的）变迁系统T，称为模型M。 一个变迁系统T=（S，s0，L，→）由一组状态S（s0∈S是初始状态）和标号变迁（L组标号;→S×L×S是一组标记的跃迁）[24]。系统需要满足的任何检查条件在时序逻辑[16，6]中定义，称为公式φ。在模型检查中，时态逻辑用于描述系统随时间的属性。时态逻辑将时间建模为状态序列。因此，人们可以使用时序逻辑来描述随着系统演化而必须保持的条件[16]。不幸的是，如果在验证过程中必须考虑太多对象，则模型检查会导致状态空间爆炸问题[22]。模型检测的一个广泛使用的特性是，如果一个检测条件被评估为不确定，则能够生成反例。每个反例都由一系列说明不一致性的状态组成。反例的性质已在[12]中讨论过。由于没有模型检查工具可以确定哪个状态序列适合于CM. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）616700举例说明错误，如果可以选择不同的序列，估计特定反例的质量是基于用户的观点。然而，在这方面取得的进展甚微[8]。反例的表示在模型检查工具中各不相同。它们中的大多数都是状态序列的文本表示，而其他工具则使用表格或序列图。3.2多对象检查反例如上所述，在多对象检查中，如果最外面的D公式成立，则D1公式成立。否则，如果这个D公式不成立，则必须生成一个反例。如果使用模型检验来验证最外层的D0公式，则生成反例的初始部分。这是一个全球性的反例，称为局部反例。如果初始局部反例不包含与其他对象的通信，则它是全局多对象检查反例。类似地，每当局部反例包含与其他对象的通信时，局部反例是全局反例的一我们专注于类的多对象检查反例中存在的对象之间的通信。所有过渡系统的初始状态，不包含任何通信。因此，初始的局部反例是指有限或无限长的模型检验反例。必须保持对象的通信伙伴之间的通信顺序算法执行如下：• 对每个被识别为被调查对象的• 检查是否可以为每个对象保留通信。• 每当发现另一个通信伙伴时，重新启动算法，直到覆盖所有通信。该算法的工作原理是每个通信伙伴提供相应的通信方案。 如前所述，确定反例的表现力是困难的，为每个对象选择随机反例并不能保证可以生成全局反例。每当对象的通信伙伴不提供所需的通信方案时，其中一种可能性是，该对象的反例没有被适当地选择。这个问题可以通过自动为显示不同通信方案的发起对象选择不同的反例或者，用户可以交互式地检查到目前为止已经生成的全局反例的一部分这两种解决方案都有缺点。第一个解决方案实现了一种贪婪/回溯算法，具有所有众所周知的优点（缺点）。局部反例再生的次数越多，算法的效率就越低。最后，全局反例可能并不像预期的那样清楚地说明错误。相反，应用第二种策略，用户可能没有足够的信息来决定部分全局反例是否显示原点68M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）61的错误。这些观察结果构成了以下验证驱动的反例生成策略：• 根据用户指定的超时，生成不同的本地反例。• 如果时间耗尽，用户可以判断实际的反例是否有用。• 如果用户不能利用给定的反例，他可以通过提供领域知识来指导算法。3.3反例生成算法在基于UML的RI中的应用我们在第2节中介绍了一个基于UML的RI。检查条件（例如，如果一个基础设施对象o没有被使用（state = unused），那么总是可以使用这个对象：F：= o来建立一个路由（lock = route）。（G（state=unused））（锁=路由）），需要定义该模型期望填充的值。在[15]中，通过仿真、模型检验和多目标检验等方法对类似的要求进行了检验。上述反例的生成算法可以通过检验条件F来证明。由于检查条件F最初不成立，我们很容易发现错误的情况：GA3可能没有使用，但它可能收到来自邻居W3和W1的路由请求。在这种情况下，安全（但不起作用）的响应是拒绝两个路由请求rr。我们已经应用了反例生成算法，并在第一步中为对象W3和W1创建了两个观察者（参见图7）。见图7。 拒绝两个并发路由请求W3的观察者监视W3的行为，使得观察者自动机中的转移tJ∈TJ是W3中具有相同通信的那些转移t∈T的投影观察者自动机中的状态表示状态，发生在W3的自动机中的转换ti和ti+1检查W3是否可以像预期的那样与GA3进行通信可以通过检查观察者自动机的行为是否可能来评估（参见图8）。W3和它的观测器在观测器中指定的跃迁上同步图9中生成的序列图展示了联锁视角之外的全局场景它以与上述相同的方式生成。M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）6169example11示例见图8。为对象W3和W1见图9。 可以相继建立连接路线3.4基于多目标检测测试用例通常是从给定的规范手动导出的该推导对系统的一部分进行建模。这些测试用例也可以用来模拟开发系统的行为。系统设计模型和测试模型都可能包含错误。在铁路领域，由（形式）规范给出的许多检查条件φ定义了某些结论ω在某些前提下成立的含义λ[21]。大多数前提和结论定义了系统中的某种状态，并构成了具有以下结构的检查条件：G（（λ1 <$λ2<$...λn）<$Fω）。由于每个λx，1≤x≤n属于一个特定的对象i，给 出 了符 合 对象间 通 信 要 求 的 D1 公 式 . 公 式 φexample ： = G （ （ λshared trackelement<$λroute1<$λroute2）<$F（ωsharedtrackelement））翻译如下：Dφ：= 共享跟踪元素。（G（（λ）共享轨道元素路由1：（λ路由1）（λ路由2：（λ路由2））（ω F（ω共享轨道元素）通过预先验证系统模型，让所有这些检查条件φ评估为TRUE。通过否定G（λ1<$λ2<$.）的结论，自动导出检验条件φ test。λnFω）。这种否定也适用于D1公式我们导出以下检查条件以生成用于检查条件φD1示例的测试用例：Dφtest：=共享轨道元素。（G（（λ）共享轨道元素路线1：（λroute1）路线2：（λroute2））<$F（ω共享轨道元件）这样的检查条件显然是对多目标检查的70M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）61测试并且应用贪婪/回溯算法来生成合适的反例（参见，第3.2节）。它们说明了系统从初始状态到条件（<$Fω）不成立的状态的可能演变。这些演化可以用来自动指定测试用例，给出了实现的设计模型在[7]中，给出了消息序列图到测试和测试控制符号版本3（TTCN-3）测试用例的翻译。结合生成的检验条件φD1以及到在实现中，可以容易地导出TTCN-3测试用例。对于铁路领域，要求覆盖率已被接受为适用于已安装联锁系统的所有要求的覆盖率标准，因为这种系统产生的风险已被容忍数年甚至数十年。如果所有的需求都是原子的，每个需求都属于一个测试用例，那么成功地应用所有这些测试用例将最终确定测试过程。4结论在这方面的贡献，多目标检查的反例生成策略进行了描述。我们已经证明了我们的策略的有用性，通过案例研究，具有UML为基础的RI。RIS被认为是安全关键系统。需要在整个系统生命周期中保证正确的行为为了节省开发和修改RIS系统的资源，本文研究了一种面向对象的联锁系统建立方法在基于UML的RI中，基础结构元素被认为是基础结构对象。RIS的对象相互协作以作为联锁系统。多对象检查已成功地应用于验证基于UML的RIS。我们专注于验证模型的安全性。本文中提供的图形反例有助于纠正状态机显示明显未处理的情况。我们相信，这种方法，提高不同学科的专业之间的理解和沟通，可以改善系统的整个开发过程。我们还展示了通过设计更全面的验证策略改进系统开发的进一步步骤它提供了说明性的反例，并自动生成测试用例。因此，我们已经证明了如何TTCN-3测试用例可以在系统开发的早期阶段，从检查条件。铁路工程师谁是熟悉序列图符号的积极反馈表明，我们的工具的用户界面的进一步发展。未来的工作将通过同时确定多对象检查通信符号并在验证过程中重用中间结果来增强反例生成过程M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）6171引用[1] Banci，M.，A. Fantechi和S.格内西，格式方法在开发分布式铁路联锁系统中的作用，在：E。Schnieder和G. Tarnai，编辑，第五届铁路和汽车系统自动化和安全的形式化方法研讨会论文集（FORMS/FORMAT2004）（2004），pp. 220-230[2] 贝尔河，IEC 61508简介，in：T. Cant，editor，Tenth Australian Workshop on Safety Critical Systemsand Software（SCS 2005），CRPIT55（2005），pp. 三比十二[3] Berke nköoter，K. 和你。Hannemann，将RailwayControlDo二、0Pro filee. ，i n：J.G'orski，editorr，C omputerSa，Rel i abiity，anddSec urity，25t h Internati onalConference，SAFECOMP 2006，Gdansk，Poland，September 27-29，2006，Proceedings，2006，pp. 398- 411[4] 卡瓦达河A. Cimatti，M. Benedetti，E. Olivetti，M. Pistore，M. Roveri和R. NuSMV：A newsymbolic model checker，http://nusmv.itc.it/（2002）.[5] CENELEC，“E N 501 2 {6|8|9}- R a il w a y A p li c a t i o n sGui dTrans portSys s t e m s t em s e s te s[6] Clarke，E.M.，O. Grumberg和D.A. Peled，[7] Ebner，M.，TTCN-3 Test Case Generation from Message Sequence Charts，Technical Report IFI-TB-2005-02 ， InstitutfürInformatik ， Georg-August-Univer s itüatGüotingen ， Germamy （ 2005 ） ， 在ISSRE 04电信和UML语言集成可靠性研讨会上发表（ISSRE04：WITUL），IRISA，Rennes，France，2.2004年11[8] Edelkamp，S.，A. L. Lafuente和S. Leue，Directed explicit model checking with57+。[9] Ehrich，H.- D.和C. Calcott，《分布式信息系统中的通信》，Acta Informatica36（2000），pp. 591-616.[10] Ehrich ， H.- D 、 C. Calcium ， A. Sernadas 和 G. 邓 克 ， 并 行 信 息 系 统 的 逻 辑 ， 在 ： J.Chomicki和 G 。Saake，editors，Logics for Databases and Information Systems，Kluwer Academic Publishers，1998pp. 167-198.[11]Ehrich，H.- D、M. Kollmann和R. Pinger，Checking Object System Designs Incrementally，Journal ofUniversal Computer Science9（2003），pp. 106-119[12] Groce ， A. 和 W. Visser ， What went wrong ： Explaining counterexamples ， in ： SPIN Workshop onModel Checking of Software，2003，pp. 第121-135页。[13] 哈雷尔，D.，H. Lahover，A.Naamad，A.Pnueli，M.波利蒂河Sherman，A.Shtull-Trauring和M. Trakhtenbrot，Statemate：复杂反应系统（2002），pp. 135-146。[14] Holzmann，G. J.，模型检查器SPIN，Software Engineering23（1997），pp. 279-295.[15] 亲爱的Y M. 和M. Kollmann，基于UML的铁路联锁的模拟和验证，在：S。Merz和T. Nipkow，编辑，第六届关键系统自动验证国际研讨会的初步会议记录，法国南希，2006年，第100页。168-172.[16] Huth，M.R. A. 和M.D. Ryan，[17] 科曼， M. 和 Y. M. 阿坚，一代 的 反例 为 多目标 系统，在：E. Schnieder和 G. Tarnai ， 编 辑 ，第 六 届铁 路 和 汽 车 系统 自 动 化 和安 全 的 形 式化 方 法 研 讨 会论 文 集（FORMS/FORMAT 2007）（2007）。[18] McMillan，K.L.，[19] OMG，[20] Pachl，J.， “Railway Operation and Control,” VTD Rail Publishing, New Jersey,[21] Pavlovic，O.，R. Pinger，M. Kollmann和H. Ehrich，联锁软件的形式验证原理，在：E。Schnieder和G.Tarnai，编辑，第六届铁路和汽车系统自动化和安全的形式化方法研讨会论文集（FORMS/FORMAT2007）（2007）。72M. Kollmann，Y.M.Hon/Electronic Notes in Theoretical Computer Science 190（2007）61[22] Valmari，A.，状态爆炸问题，在：关于Petri网的讲座I：基本模型，Petri网的进展，卷是基于高级课程Petri网（1998年），pp。429-528.[23] van Dijk ， F. ， W. Fokking ， G.Kolk ， P. van de Ven 和 B. van Vlijmen ， Euris ， 一 种 特 定 化 方 法SAFECOMP '98：Proceedings of the 17th International Conference on Computer Safety，Reliability andSecurity（1998），pp. 296-305[24] Winskel，G.和M. Nielsen，Models for concurrency，in：S. Abramsky，D. Gabbay和T. S. E. Maibaum，编辑，Handbook of Logic in Computer Science，Oxford University Press，1995。