没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记174(2007)19-35www.elsevier.com/locate/entcs反例的自动解释方法莱昂内尔·范登伯格1,2保罗·斯楚珀3温迪·约翰斯顿4昆士兰大学信息技术与电气工程学院澳大利亚布里斯班摘要模型检查是一种用于验证有限系统的自动技术。模型检查器探索给定模型的完整状态空间,并根据一组需求对其进行检查。 如果存在一个状态,其中一个需求没有得到满足,大多数工具将生成一个反例。反例对于调试模型和确定建模系统中是否存在错误非常有用。然而,它们可能难以为最终用户所理解,这可能会限制模型检查在工业中的应用本文描述了一种特定于领域的方法来自动解释反例,并以直观的形式向最终用户呈现结果。我们的研究扩展了以前的工作模型检查铁路信号控制表与信号工程师从昆士兰州铁路。保留字:模型检查,反例,解释,铁路信号,验证,动画。1引言模型检测在工业应用中特别有趣,以支持验证安全关键系统的当前流程。模型检查器对给定模型的整个状态空间执行穷举搜索,针对一组属性对其进行测试。大多数工具要么向用户提供一个声明所有属性都为真的答案,要么以反例的形式报告违规行为[4]。一个反例是一个可能的路径,描述了从初始状态开始的系统变量的值模型检测是一种用于验证系统设计的有用技术,然而,也存在一些问题,1感谢同事Kirsten Winter和Peter Robinson以及昆士兰铁路公司的同事:George Nikandros、David Barney和David Tombs。该项目由ARC链接赠款LP 04551552 电子邮件地址:lionel@itee.uq.edu.au3 电子邮件地址:pstroop@itee.uq.edu.au4 电子邮件地址:wendy@itee.uq.edu.au1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2006.12.02720L. van den Berg等/理论计算机科学电子笔记174(2007)19要在实践中克服困难,取得成效。反例对于最终用户来说很难理解[9],特别是在可能有数百个变量的大型系统中,用户可能对模型如何工作知之甚少或一无所知。昆士兰大学和昆士兰铁路(QR)之间的先前研究产生了信号设计工具集[12],其中包括轨道布局编辑器,控制表生成器,控制表编辑器,以及在其初步阶段的验证管理器[14]。信令设计工具集产生的控制表之一是路由表。路线表的生成以前已经过验证[13],并与轨道布局一起用作数据源,验证管理器相信它是正确的。验证管理器是NuSMV模型检查器的接口[2]。它从轨道布局中收集有关点、信号和轨道位置的信息,并从信号控制表中收集锁定点和路线的规格。根据这些规范,在NuSMV输入语言中自动构建模型。 要验证的属性基于QR原则[11]和以通用术语表示为不变量,如回避火车相撞和脱轨的事故验证管理器调用NuSMV,如果违反属性,则生成反例。NuSMV生成的反例通常由第一个状态和一系列后续状态组成,第一个状态包括模型中所有变量的值,而后续状态只包括自前一个状态以来发生变化的变量当使用不变量时,被验证的系统属性总是在反例的最后一个状态中被违反。然而,这不一定是系统规范中发生错误的地方[8]。反例对于调试来说是很好的[4],但它们也可能难以让用户理解。反例和模型检查的一些问题包括:• 每个状态中的变量并不总是与被违反的属性有任何关系。• 反例可以有很多状态。通常,许多状态与系统规范中的错误无关,只需要模型检查器显示错误状态的完整路径• 状态爆炸问题[4]使得有必要抽象模型以减少状态空间[3]。抽象模型可能意味着排除或修改某些数据,并且模型的行为可能因系统规格而异。这些问题使得反例难以让用户解释。我们的反例更加复杂,因为铁路联锁规范中的冗余要求我们创建故意遗漏一些数据的模型,以便检查规范中的其他条目这导致模型行为与实际铁路联锁不同。我们的反例在形状上是线性的(关于使用小互锁产生的反例的示例,参见表1它们能很好地追踪L. van den Berg等/理论计算机科学电子笔记174(2007)1921跟踪类型:反例移动CR = 1request = reqC 6-> 状态:1.1-请求=请求6 1S路由锁8 1M = rtN阳性CR = 1Cb路由锁定5 1M = rtR-> 状态:1.9-pos FS = 1Cb-> 状态:1.3-阳性CR = 2Ca进站列车= FS阳性CR = 1例pos FS = 8Cb移动CR = 0进站列车= FS移动FS = 0移动FS = 0请求=请求8 1Mrequest = reqN 501pointState 511 = setR路由锁定6 1S = rtR路由锁定6 1S = rtN-> 状态:1.4--> 状态:1.10-pointState 500 = setRpointState 501 = setR阳性CR = 5Aa阳性CR = 2Ba请求=请求5 1M入站列车= CRpointState 501 = setNcurrentRoute CR = NoRoute移动FS = 1请求=请求6 2ScurrentRoute FS = NoRouterequest = reqC 5-> 状态:1.11-路由锁定5 1M = rtNcurrentRoute CR = 5 1M阳性CR = 2Aa路由锁定6 1S = rtN路由锁8 1M = rtR移动CR = 0路由锁定6 2S = rtN-> 状态:1.5-请求=请求4 1M路由锁定7 1M = rtN阳性CR = 8Bc路由锁定6 2S = rtR路由锁8 1M = rtN进站列车= FS-> 状态:1.12-路由锁8 2M = rtNrequest = reqC 6移动FS = 1路由锁1 1M = rtN路由锁定5 1M = rtNrequest = reqC 6路由锁1 2M = rtN-> 状态:1.6-路由锁4 1M = rtR路由锁2 1M = rtN阳性CR = 8Aa-> 状态:1.13-路由锁定3 1S = rtN阳性FS = 5Abpos FS = 1Bd路由锁定3 2S = rtNrequest = reqN 511request = reqC 4路由锁定4 1M = rtN-> 状态:1.7-currentRoute FS = 4 1M路由锁定5 1M = rtN阳性CR = 7Aa-> 状态:1.14-路由锁定6 1S = rtN阳性FS = 8Ab阳性FS = 1Ab路由锁定6 2S = rtNpointState 511 = setN请求=请求3 2S路由锁定7 1M = rtNrequest = reqC 8路由锁定4 1M = rtN路由锁8 1M = rtNcurrentRoute FS = 8 1M-> 状态:1.15-路由锁8 2M = rtN-> 状态:1.8-阳性FS = 2Ab-> 状态:1.2-阳性CR = 7Barequest = reqC 7入站列车= CR正FS = 8Bd路由锁定3 2S = rtR表1小互锁的反例列车运动和联锁行为直到不变量被违反。然而,我们仍然发现信号工程师很难理解NuSMV为我们的模型制作的反例。需要NuSMV生产的替代产品。我们研究了两种解释反例的方法-动画和自然语言解释。模拟是一种高效的技术。然而,在我们的应用程序中,从反例中动画化铁路联锁和列车行为存在许多问题,并且不经济。解释是一种更简单的方法,需要最小的成本来产生最终用户容易理解的输出。我们开发了一个解释器来读取反例,使用路线表和轨道布局来生成解释。只有相关数据以自然语言和表格形式呈现给用户。通过利用领域知识,解释器显著简化了NuSMV的输出,提供了错误的一般描述。在某些情况下,输出更具体,并告诉用户具体的错误是什么本文讨论了为什么动画不适合我们的应用程序,并描述了我们的解释器的细节通过提供特定领域的解释,我们展示了如何用用户领域的自然语言向用户呈现反例我们建议,对于最终用户对模型检查知之甚少的应用程序,特定于域的解释提供了更好的反馈。结果可以根据领域进行定制,并使用与领域术语一致的语言进行表示。第2节描述了验证管理器生成的不同列车模型和安全属性,以及这些模型和安全属性如何影响可读取性。22L. van den Berg等/理论计算机科学电子笔记174(2007)19领域专家的反例。第3节介绍了我们的调查动画和我们的原型解释反例。第4节描述了我们解释反例的实现,第5节描述了对工具有效性的评估我们将在第6节讨论相关工作,并在第7节总结结果。2铁路联锁系统的建模被验证的模型和性质对反例的可读性有重大影响模型越抽象,解释它就越困难抽象通常涉及将一些数据保留在模型的状态空间之外。这使得应用领域的专家在缺少他们希望看到的信息时很难理解反例。当存在大量与系统中的误差无关的数据时,解释反例也是困难的。2.1铁路联锁铁路联锁系统是一个由道岔、信号和轨道组成的系统,其设计目的是使列车能够安全地通过铁路布局。图1是铁路联锁的示例轨道布局。点(例如,511)是轨道上的可移动信号灯(例如5、6、7和8)使用类似于常规交通灯的颜色指示(例如红色表示停止),以向列车司机指示他们是否有权继续前进或是否必须停止。轨道电路(例如1C、5A、8B、8A、7A、8D和8C)是铁路联锁中的轨道区段。51C 5A 28B8D 8C5118B 8A 7A 2A 2B 2C67 8 1图1. 一个小的轨道布局。表2是对应于图1的信号控制表的一部分。 路由是两个相对的信号之间的路径。表2只包含一条路由5(1M),它从信号5开始,到信号1结束。 路由标识符中的第一个数字(例如,5)是路由开始的信号。第二个数字对于附加到信号的每条路由都对于本文,可以假设,L. van den Berg等/理论计算机科学电子笔记174(2007)1923它从1开始,并且对于每个附加路由递增。字母M或S分别表示主路由或分流路由表中包含的分流路径仅这些是作为主路由的分流路由。信号控制表规定了锁定准备使用的路由(设置反向)和保持路由(保持反向)所需的条件。标题为“点正常”、“点反向”、“路线正常”和“路线反向”的列按轨迹发生”。列包括使用路线的列车在相应点或路线的状态可以改变之前必须清除的轨道。The ”Tracks Clear” column providethe tracks that are required clear before a route can be locked信号线编号路线需要点航线路线保持Maint.按轨道发生率轨道清除正常反向正常反向5(1M)15115A5A 8B8A 7A6(2S)5A 8B8(1M)8(2M)5A 8B 8A2(1M)5A 8B 8A 7A表2一种小型信号控制表。2.2火车模型验证管理器生成NuSMV输入语言中描述的两个不同模型。不同模型用于检测信号控制表中的不同误差所有型号都包括一个联锁系统模型和一个或两个列车。系统要求或安全属性被建模为简单的不变量[14],例如,火车不得脱轨。模型是为特定的验证区域生成的,该区域是铁路联锁的一部分。一个验证区域至少应该包括一条路线和所有与之相对的路线。 为了建模的目的,我们将轨道电路划分为段,每个段定义轨道电路的唯一遍历。 如图2所示, 由诸如8Ba、8Bb、8Bc和8Bd的虚线箭头线描绘。验证管理器生成的模型包括列车及其位置(它们所占用的轨道段)、点及其位置(正常/反向)以及路线及其锁定(正常/反向)。模型中的每列火车都有一个变量currentRoute,表示火车当前使用的路线。改变变量状态的规则来自信令原则[11],24L. van den Berg等/理论计算机科学电子笔记174(2007)198BC8B取决于状态变量的当前值。在我们的抽象模型中,改变信号方面的规则只取决于其他状态变量的值,而不是当前方面。因此,为了效率,我们从状态空间中排除信号,通过检查信号所依赖的变量的当前值来建模它们沿着一条联锁线路行进,遵守信号原理中的规则。它们在红色信号时停止,也可以在任何轨道段上停止。没有与列车运行相关的速度。8Bd8Bb a8B图2. 轨道8B的轨道段示例。有两种基本模式。第一个模型我们称之为TC(轨道清除)模型,包括控制表的完整表示,即来自控制表的所有信号设备和锁定数据。该模型用于检查同向行驶的列车之间的碰撞。第二个模型我们称之为NTC(没有明确的轨道,意味着排除明确的轨道)模型。该模型排除了信号控制表中需要清除的轨道列,以消除冗余,并测试进路保持条件。允许列车在同一时间占用同一路线,甚至同一区段。 该模型用于检查在不同方向上行驶的列车之间的脱轨和碰撞。有四个安全属性/不变量,我们称之为脱轨,opplock,di路径和samepath。脱轨不变量使用单列车NTC模型,并在点设置不正确或在列车下方移动时检查列车脱轨。opplock不变量用于单列车NTC模型,并指出每当列车位于相反信号(即相反方向的信号)的第一条轨道上时,没有与该信号相反的路线设置。双路径不变量用于NTC模型和两个列车。它是用来检查迎面碰撞和侧击。同路径不变量用于TC模型和两个列车。它是用来检查列车运行到对方的后面。中的每不变量用于检测控制表中的不同错误。在脱轨、opplock和diploppath将检测到的错误类型之间存在重叠,但是为了检测尽可能多的错误,必须验证每个不变量2.3反例解释的模型设计效果模型的设计直接影响生成的反例。例如,由验证管理器生成的早期模型为验证区域中的每条路线使用一个变量它被中讨论的currentRouteL. van den Berg等/理论计算机科学电子笔记174(2007)1925第2.2节。当前路由变量减少了反例中状态和无关变量的数量,并使原始数据更具可读性。然而,信号工程师仍然很难解释反例。抽象模型可以使反例更难阅读。我们的模型通过排除信号进行抽象。这减少了状态变量的数量,但也意味着用户不知道任何信号的方面是什么。我们已经通过全面的测试证明了该模型是准确的。然而,信号工程师仍然发现该模型令人不安。NTC模型用于脱轨、反向锁定和反向路径模型。 该模型不包括无障碍轨道,专门用于检查路线锁定和等待条件中的错误。该模型允许两列列车同时锁定并使用同一进路和占用同一轨道区段,以便能够在信号控制表中检查其他锁定条件。允许列车占用相同轨道段的错误由TC相同路径模型检查。当信号工程师看到两列火车占用同一轨道段时,他们立即认为有错误。当他们发现控制表不允许这种行为,并且没有对模型如何工作的透彻了解时,他们会认为它是不正确的,并丢弃反例。因此,有必要对不了解模型的用户隐藏此细节。反例通常在每个状态中包含自前一个状态以来已更改的变量当验证铁路联锁时,为了只检查一条路线,必须包括所有相对的路线。如果检测到错误,则产生的反例将包含每个路线、轨道段、点、列车、每个列车的当前路线等的变量,即使在一个路线中仅发生单个这可能是压倒性的,因为一个小的验证区域可以包含多达30个变量。3提出反例有许多方法可以向用户提供反例,每种方法都可以根据制作反例的成本和方法的有效性进行评估。最明显的解决方案是提供由模型检查器产生的原始数据;成本为零,但由于已经讨论过的原因,效率不令人其他方法涉及一定程度的翻译,以更直观的方式呈现数据。然而,当解释抽象模型时,需要的翻译越多,产生错误解释的风险就越大。我们研究了两种方法,动画和解释,使反例更翔实。这两种方法都是旨在实现完全自动化,并与验证管理器和信令设计工具集集成。26L. van den Berg等/理论计算机科学电子笔记174(2007)193.1动画动画是一种优秀的,用户友好的方法,为用户提供视觉反馈。进行了一项可行性研究,以调查反例动画及其成本效益。抽象模型的动画制作涉及到许多问题。对于一个铁路联锁,有必要动画所有的信号,路线和点锁定。我们的模型不包括信号。因此,有必要模拟信号行为。这样做的唯一选择是使用QR这引入了信号根据模型的实际行为被不正确地建模的风险。在这种情况下,动画可能会掩盖错误或模拟意外行为。动画反例产生的路径不变量也有问题。动画将显示两列火车使用相同的路线,并在同一时间占据同一一旦发生这种情况,用户可能会错误地认为存在错误,但事实并非如此。由于这些原因,动画不适合我们的应用程序。3.2解释第二种方法涉及对反例的自动解释,以确定导致碰撞或脱轨的实际错误。关键概念是设计一种算法来解释反例,并产生对导致安全违规的错误的该算法需要是通用的,以处理我们所有的反例,尽管它们之间的差异。仅应收集与错误相关的数据并将其呈现给用户。为了有价值,算法的输出应该提供尽可能多的细节,而不误导用户。我们研究了这种方法,看看我们是否可以可靠地识别导致反例的错误。我们设计了一个原型算法,或解释器。通过使用领域知识,我们能够定位错误的路由和信号设备的谎言。在某些反例中,我们可以确定准确的误差,而对于其他反例,我们根据信号设备的锁定产生更一般的结果。在与昆士兰铁路公司进行试验后,我们确定最好以表格形式向用户展示解释结果。我们将在第4节中讨论实现的细节。4反例解释第3.2节中描述的概念被原型化用于概念证明。解释器是一个单一的算法,用于第节中描述的每个不变量。2.2. 解释器需要三个输入:(i) 反例作为文本文件。(ii) 控制表指定为XML文件。(iii) 被解释的反例类型。L. van den Berg等/理论计算机科学电子笔记174(2007)1927可以随时检查相同路径不变量。脱轨,opplock,和diplock路径不变量必须按照这个顺序运行,这样每个不变量检测到的错误类型是有限的,一些错误可以被排除。例如,当检查方向路径不变量时,不应有不正确的点设置。控制表也需要合理的格式。信令设计工具集在模型检查器之前执行大量检查时,会生成可接受的控制表奔跑吧[13]解释器执行三个基本步骤。首先,找到最近使用的路由被锁定的状态,并从该状态检索与错误相关的数据然后解释收集的数据,并在最后一步中格式化并以表格形式呈现给用户。 设计了一种通用的输出格式。表3中显示了一个示例,该示例对应于图1中的布局。包括一组典型条目,用于说明目的。结果是以信号工程师目前测试铁路联锁的方式呈现的。第一行是正在测试错误的路由。预计将在此路由中发现然而,错误可能在相反的方向上,路线 这只适用于opplock和两列反例,在脱轨的反例中没有相反的路线。第二行包括与发现的错误相关的列车位置、路线锁定和点的位置,以及允许错误发生的相应操作,例如设置相反路线的请求。动作的结果显示在第三行;它是动作的直接结果,可能包括正在设置的路线或改变路线的点。第四行描述发生的错误类型。默认情况下,以一般方式描述错误,以避免得出不正确的结论,但在某些情况下,表中的特定错误可以识别。试验路线5(1M)行动5(1M),占用8A轨道。请求8(1M)倒车。发生了什么8(1M)设置反向。误差8(1M)在5(1M)使用时设置为反向。表3反例的解释输出的模板表3是在轨道8A上检测到的碰撞的示例解释。碰撞的原因是8A从“维修”中丢失。按轨迹发生”。表2中信号控制表的列。反例的解释输出表明来自信号5的路线5(1M)当前正在使用中,列车占用轨道8A,并且路线8(1M)被允许反向设置。领域专家可以使用此信息来确定错误发生的位置,并快速定位并纠正问题。为了使该表有用,错误必须在路径5(1M)或8(1M)中,否则解释将比NuSMV产生的反例更少使用。28L. van den Berg等/理论计算机科学电子笔记174(2007)19解释所需的数据因每个不变量而异。所需数据和语义的描述如下。破坏• 点-火车出轨的点。• pointMoved-一个布尔值,如果点在列车下方移动或列车正在使用路线时,则为true,如果点已经设置不正确,则为false• trackOccupied-当点移动到列车下方或列车使用路线时占用的轨道。这仅在pointMoved为true时使用。• 路线- 列车出轨时使用的路线奥普洛克• route- 当设定了相反的进路时,列车正在使用的进路• trackOcc- 设置反向进路时列车占用的轨道• oppRoute-反向设置的反向路由。双径和同径• primaryRoute-当不变量被违反时,火车一直用作其最多状态转换次数的当前路线的路线。• secondaryRoute-当不变量被违反时,另一列火车一直使用的路线。• trackOccupied- 在次要进路被设置为反向状态之前,列车在主要进路上对每种反例的数据进行单独解释。反例可以有一个以上的输出格式,这取决于某些数据的值。每种反例的解释格式和例子如下。4.1脱轨解释有两种行为可以区分出轨反例。如果pointMoved的值为false,那么我们就知道在设置路线时,点的位置是不正确的。然而,如果pointMoved为真,我们就知道当火车在路线上时点移动了。我们在每种情况下使用单独的格式来表达反例。表4是当pointMoved为false时用于向用户呈现反例的格式,pointMoved是真的。 变量X用于指示一个变量的位置或位置的变化。点它的值可以是正向或反向。表6和表7分别是表4和表5所产生的反例基于表2中的信号控制表和图1中的轨道布局。L. van den Berg等/理论计算机科学电子笔记174(2007)1929试验路线路线行动请求点集为X的路径。发生了什么路线设置为反向。误差点不需要X来设置路线。表4其中点设置不正确的解释输出的模板。试验路线路线行动已占用的轨道。请求X点发生了什么点集X。误差点未由路径而trackOccupied被占用。表5当列车在路线中时,点在其中移动的解释输出的模板试验路线5(1M)行动要求5(1M)与511点设置正常。发生了什么5(1M)设置为反向。误差设置5(1M)不需要反向511点。表6点设置不正确时产生的输出示例试验路线5(1M)行动5(1M),占用5A轨道。请求511正常发生了什么511正常误差511点未被5(1M)持有,而轨道5A占用。表7当列车在路线上时,点移动时产生的输出示例。4.2Opplock解释奥普洛克反例有一种解释。不变量检测三种类型的错误,但解释器的输出是通用的,因此它允许30L. van den Berg等/理论计算机科学电子笔记174(2007)19用户可以很容易地确定问题。模板和随附示例分别在表8和表9试验路线路线行动路线设置为反向,轨道已占用轨道已占用。请求oppRoute反向。发生了什么oppRoute设置为反向。误差使用trackOccupied的路由。oppRoute设置为反向。表8opplock反例的解释输出的模板。试验路线5(1M)行动5(1M),占用8B磁道。请求6(1S)倒车。发生了什么6(1S)设置为反向。误差使用5(1M),占用8B。 6(1S)设置为反向。表9opplock反例的解释输出示例。4.3第二道诠释狄仁杰的反例有一种解释。不变量检测两种类型的错误,但解释器的输出是通用的,允许用户轻松确定问题。表10和表11分别提供了模板和随附示例。试验路线主要路线。行动primaryRoute设置为与轨道反向占用轨道有事。 请求二次航线反向。发生了什么secondaryRoute设置为反向。误差primaryRoute与trackOccupied跟踪一起使用。secondaryRoute设置为反向。表10查询路径反例的解释输出的模板。L. van den Berg等/理论计算机科学电子笔记174(2007)1931试验路线5(1M)。行动5(1M)设置反向,占用8B磁道请求2(1M)倒车。发生了什么2(1M)设置反向。误差2(1M),NG8B磁道占用。 2(1M)设置反向。表11difficulpath反例的解释输出示例。4.4Samepath解释Samepath反例有一种解释。在每一种情况下,解释器都能发现准确的错误。表12和表13分别提供了模板和随附示例。最后一行所述的错误通知用户信号的轨道清除列中缺少的轨道控制表试验路线路线行动轨道占用占用。 请求改变航线发生了什么路线设置为反向。误差设置路线时不需要清除trackOccupied。表12samepath反例的解释输出的模板。试验路线5(1M)。行动1C被占用 请求5(1M)倒车。发生了什么5(1M)设置为反向。误差设置5(1M)不需要清除1C。表13samepath反例的解释输出示例。5评价为了评估解释器,共生成了177个反例,并使用我们的原型进行解释。使用了小验证区域的控制表。反例是通过将错误注入到控制表中来生成的删除单个元素,例如需要清除的轨道,然后使用我们的原型模型构建器构建模型,并使用NuSMV运行这是迭代完成的每个测试只注入一个错误。根据已注入的错误表14总结了每个不变量的结果。在177个反例中,解释器正确地识别出了174个中包含错误的路由。32L. van den Berg等/理论计算机科学电子笔记174(2007)19的 案 件 。 剩 下 的 三 个 反 例 是 由 opplock 不 变 量 产 生 的 , 错 误 是 在 相 反 的 路 线(oppRoute)中发现的。在每种情况下,用户仍然能够确定错误是什么,并且解释提供了比原始数据更好的反馈。对脱轨反例的13种解释中有6种确定了控制表中的确切误差。其余七个解释较为笼统,错误是在主要路线。确定了由相同路径不变量产生的所有误差的精确误差。模型测试运行误差主要路线误差二级省道已识别确切错误破坏131306奥普洛克555230第二路径585800塞梅帕斯5151051总177174357表14评价结果昆士兰铁路的用户看到了NuSMV输出的原始数据,以及我们的翻译器产生的解释。在开发验证管理器的早期,昆士兰铁路的领域专家努力理解NuSMV产生的原始数据。用户需要花费大量的时间来了解列车运行情况,并找到与错误相关的路线和联锁设备。当用户意识到不同的列车被允许同时占用同一轨道时,问题进一步复杂化。从未见过反例的信号工程师被用来测试这些解释。最初,他们不愿意使用解释数据,并质疑为什么他们不能只看到原始数据。他们觉得自己有足够的知识来理解原始数据。然而,在看过我们的解释后,他们可以很快告诉我们他们会在哪里寻找错误。这些解释提高了用户查找错误的速度。还有一个额外的好处是,用户不必看到两列火车被允许同时在同一轨道上行驶,并且模型中没有信号。6相关工作反例是一个可用性问题,不仅是领域专家的问题,也是设计模型的工程师的问题。大多数研究,例如Clarke et al. [3],Pasareanu et al. [10]和Dwyer et al. [5],专注于消除错误或虚假的反例,而不是提高它们的可读性。这些文件都L. van den Berg等/理论计算机科学电子笔记174(2007)1933解决由于抽象而产生的错误反例。这对我们来说不是一个问题,因为我们的抽象是精确的,模型的行为在很大程度上保持不变。Huber [7]也对铁路联锁进行了建模,他承认反例是模型检查可用性的一个问题他建议,模型检查器的输出可以根据应用领域进行定制,并且只需要适度的工作来修改模型检查器并大大提高可用性。虽然这篇论文指出Huber没有测试他的建议,但这种方法与我们的工作类似,只是我们修改了输出而不是模型检查器本身。Loer和Harrison [9]讨论了模型检查的可用性问题。他们的方法是提供一个基于SMV模型检查器的工具包。他们对解释反例的研究还处于初步阶段,但他们的目标之一是支持错误痕迹的可视化。他们的方法是通用的,试图支持工业设计师可能遇到的所有问题,而我们专注于特定领域的应用程序,专门为信号工程师定制输出。本文描述了一些原型化的方法,包括表,自然语言,场景模板,场景脚本,消息序列图,操作序列图和动画。他们指出,与会者认为表格和操作顺序图最有用。 我们生成的输出是表格和自然语言场景的组合。操作序列图比我们的应用程序所需的要复杂得多,因为我们只需要显示放置在一个点或相反路线上的请求的结果Ball等人[1],Groce和Visser [6],以及Jin等人。[8]提供提高反例可读性的一般他们的工作很有趣,因为它不是特定领域的,然而,最终的反例仍然以依赖于用户理解反例痕迹的形式呈现,并且在某种程度上依赖于模型。Ball等人描述了一种方法,其中产生描述不同误差的多个迹线。他们的算法利用正确轨迹的存在这有助于定位错误并改善对用户的输出。Groce和Visser使用类似的方法来搜索负执行集和正执行集。负执行是指在不同的跟踪中产生相同的错误。 正执行是负执行的变体,其中不发生错误。通过比较这些集合,他们表明,共同的特征和差异可以用来提供更有用的反馈,而不仅仅是提出原来的反例。 Jin等人描述一种方法,在这种方法中,反例被分解为命中注定的和自由的片段确定的段是跟踪中指向错误的操作,而自由段是在避免它们的情况下可以防止错误的选择。他们注释了一个反例来描述不可避免的片段,并让用户决定自由片段是否是系统中的故障,或者是否可以避免注定的动作。在[1]、[6]和[8]中的每一个中使用的一般方法是改进反例/反馈,以便提供包括更多与错误相关的信息和更少不相关信息的良好反例。在我们的案例中,34L. van den Berg等/理论计算机科学电子笔记174(2007)19单个反例提供了定位错误的必要信息从单个跟踪中,我们可以确定哪些是相关变量,然后专门针对目标用户调整输出,而无需上述方法所需的开销虽然简化反例可以帮助我们的用户,但我们主要关注的是行为和对模型的缺乏理解我们的最终用户也不是程序员或软件工程师,他们不一定熟悉模型检查器或编译器的输出。7讨论为向最终用户提供反例,考虑了两种方法,即动画和解释动画进行了研究,但不适合我们的应用程序,因为我们的模型是从真实系统中抽象出来的。基于信令原理[11]设计并原型化了一个解译器。这创建了一个强大的算法,可以处理我们模型中的任何反例解释器搜索反例中的关键数据,并以解释的形式将其呈现给用户,并排除所有经常使用户混淆的不相关细节。只有通过使用领域知识,我们才能做出更好的解释。通过在控制表中注入单个错误来生成测试用例,以评估解释器这种方法是合理的,因为模型检查器在他们发现的第一个反例时就停止了,所以预计实践中产生的任何反例都我们还期望联锁的一般行为仍将遵循信令原则,并且解释器的输出不应改变。然而,我们仍然没有测试原型对反例在实践中发现。这是不可能的,因为验证管理器处于初步阶段,目前没有实际的反例数据。引用[1] 鲍尔,M. Naik和S. K. Rajamani,从症状到原因:在反例跟踪中定位错误,在:ACM Symp。《编程语言原理》,纽约,纽约,美国,2003年,pp. 97比105[2] Cimatti,A.,E. 克拉克角,澳-地Giunchiglia和M.Roveri,NuSMV:一种新的符号模型验证器,在:Proc. of Int. Conf. on Computer Aided Verfication,CAV495-499.[3] Clarke , E. M. , O. Grumberg , S. Jha , Y. Lu 和 H. Veith , Counterexample-guided abstractionrefinement,in:Computer Aided Verification,2000,pp. 154-169。[4] Clarke,E.M.,O. Grumberg和D.A. Peled,[5] Dwyer,M. B、J. Hatsoul,R. Joehanes,S.劳巴赫角S.帕萨雷亚努湾Zheng和W. Visser,有限状态验证的工具支持的程序抽象,在:ICSE177比187[6] Groce,A.和 W. Visser,What went wrong: Explaining counterexamples, in: Proc. of the 10th Int.SPIN Workshop on Model Checking of Software,Portland,Oregon,2003,pp.121-135.[7] Huber,M.,“Towards an Industrially Applicable Model Checker for Railway Signalling Data,” Master’sthesis, University of YorkL. van den Berg等/理论计算机科学电子笔记174(2007)1935[8] Jin,H.,K. Ravi和F. Somenzi,Fate and free will in error traces,in:Proc. of the 8th Int. Conf. onTools and Algorithms for the Construction and Analysis of Systems(2002),pp.445-458[9] Loer, K.和M. Harrison ,Towards usable and relevant model checking techniques for the analysis ofreliable interactive systems , in : Proc. of 17th IEEE Int. Conf. on Automated Software Engineering(ASE 2002)(2002),pp. 223-226[10] 帕萨雷亚努角美国,M. B. Dwyer和W. Visser,Finding可行的反例时,模型检查抽象的Java程序,在计算机科学讲义2031(2001),页。284-298.[11]昆士兰铁路信号和运行系统,信号原理-布里斯班郊区,技术报告S 0414,昆士兰铁路技术服务集团(1998)。[12] 罗宾逊,N.,D.作者声明:John W. Nikandros和D. Tombs,设计规范的自动生成和验证,在:Proc. ofInt. Symp.国际系统工程委员会(INCOSE),2001年。[13] Tombs,D.,N. J. Robinson和G. Nikandros,信令控制表生成和验证,在:铁路工程会议论文集(CORE 2000)(2002)。[14] 温特,K.,W. Johnston,P. Robinson,P. Strooper和L. van den Berg,用于检查铁路联锁设计的工具支持,在:Proc. 第10届澳大利亚安全相关可编程系统研讨会,澳大利亚悉尼,2005年。
下载后可阅读完整内容,剩余1页未读,立即下载
![doc](https://img-home.csdnimg.cn/images/20210720083327.png)
![rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![-](https://csdnimg.cn/download_wenku/file_type_lunwen.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- VMP技术解析:Handle块优化与壳模板初始化
- C++ Primer 第四版更新:现代编程风格与标准库
- 计算机系统基础实验:缓冲区溢出攻击(Lab3)
- 中国结算网上业务平台:证券登记操作详解与常见问题
- FPGA驱动的五子棋博弈系统:加速与创新娱乐体验
- 多旋翼飞行器定点位置控制器设计实验
- 基于流量预测与潮汐效应的动态载频优化策略
- SQL练习:查询分析与高级操作
- 海底数据中心散热优化:从MATLAB到动态模拟
- 移动应用作业:MyDiaryBook - Google Material Design 日记APP
- Linux提权技术详解:从内核漏洞到Sudo配置错误
- 93分钟快速入门 LaTeX:从入门到实践
- 5G测试新挑战与罗德与施瓦茨解决方案
- EAS系统性能优化与故障诊断指南
- Java并发编程:JUC核心概念解析与应用
- 数据结构实验报告:基于不同存储结构的线性表和树实现
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)