铁路信号系统基于故障树的SDL模型的验证覆盖率

理论计算机科学电子笔记116（2005）99-111www.elsevier.com/locate/entcs铁路信号系统基于故障树的SDL模型的验证覆盖率1M. Banci2，M. Becucci2，A.Fantechi2，E. Spinicci2Dipartimento di Sistemi eInformaticaUniversit`adegliStudidiFirenze意大利佛罗伦萨摘要在本文中，我们提出了一个应用程序的形式化验证技术，以基于组件的通用电气运输系统公司借出的铁路信号系统SDL模型。MSC驱动的验证技术已被应用于验证系统的多配置功能。这项工作解决了验证一个面向组件的设计SDL模型的问题，与部分重用以前验证的MSC方案，如果一个新的组件正在引入或修改：一些可能的解决方案的基础上所采用的工具提供的覆盖度量和信息进行了讨论。关键词：基于代理的SDL模型，铁路信号，验证，MSC场景1介绍近年来，支持形式化规范和验证的商业工具的可用性促进了形式化方法的使用作为防止在安全关键系统中引入软件故障的手段，特别是使用工具支持的特定形式。这方面的两个主要例子是SDL [1]，一个在电信行业内开发的标准，以及Statecharts1这项工作得到了意大利大学和研究部在COFIN 2001项目2电子邮件：[banci，becucci，fantechi，spinicci]@dsi.unifi.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.083100M. Banci等人理论计算机科学电子笔记116（2005）99[3]由iLogix Statemate工具支持我们参考[7]和[6]中的两个不可表的例子，将这种形式化应用于铁路信号系统，这是我们研究的应用领域。在与通用电气运输系统（GETS）的合作中，我们首先研究了在GETS开发周期中引入SDL技术用于多配置铁路信号系统[4]，评估合适的验证技术[5];下一步是研究以前SDL规范的基于组件的设计方向。实际上，一个SDL模型应该保留多配置特性，它需要通过在给定拓扑结构下连接的不同数量的通用组件来描述，也就是说，通过定义可配置的组件类型：在给定配置中，每个组件类型所需的实例数量可以通过合适的配置参数来设置。在这类模型中，插入新组件或修改现有组件不仅意味着改变现有组件与新组件之间的接口，而且还意味着修改模型的拓扑结构。这涉及对所有已定义的情景再次执行验证活动在面向组件的SDL模型中，必须开发和验证基本组件规范;然后，根据给定的配置，将每个组件的一个或多个静态副本互连。然后将对获得的模型进行最终验证;消息序列图（MSC）[2]可用于定义模拟和测试场景。在本文中，我们讨论了MSC驱动验证的应用，以验证，通过指出引入新组件时测试场景的重用，从所采用的案例研究中提炼出一个简单的配置。本文的结构如下：在第2节中的案例研究的描述，以及基于组件的SDL模型的概述。第3节及其小节介绍了所采用的验证方法，详细说明了用于评价所执行的确认活动并最终获得结果的覆盖率测量。2案例研究：SCA系统SCA系统（Sistema Conta Assi，计轴系统）由通用电气运输系统公司（General Electric Transportation Systems，G.E.T.S.）开发，是一种设备，用于计算属于在给定铁路区段中行驶的列车的轮对的数量。该操作使用放置在轨道旁边的进入和离开铁路区段的轮对数量的连续计算允许确定区段本身是否空闲（如果离开轮对的数量等于进入轮对的数量M. Banci等人理论计算机科学电子笔记116（2005）99101轮对）或仍然被列车占用。该信息用于通过适当的（外部）信号机信号启用或禁止下一列列车进入该区段。SCA系统由几个控制和采集单元组成，称为UCA（Unita`ContaAssi，轴耦合单元），沿轨道放置UCA-PRA连接如图1所示。Fig. 1.单段配置的SCA系统，突出UCA-PRA互连。PRA由两个名为DRT（Detettore Ruota Treno，火车轮检测器）的磁传感器组成，每个传感器位于一个铁轨上，以实现冗余。两个磁探测器必须连续地给出相同的信号。如果只有其中一个发送通过车轮的信号，UCA进入典型的反应是将所有信号设置为红色。UCA单元位于区段的开始处;它们接收并处理由DRT调制的信号，以确定在轨道上运行的轴的数量;这些数据通过调制解调器发送到远程UCA。使用远程数据，UCA可以确定该区段是否仍然被占用，并且在第一种情况下，它通过启用自动锁定继电器来停止后续列车。由于轨道通常可以在两个方向上运行，UCA能够检查进入铁路区段的列车和离开的列车。远程UCA之间的连接，如图1所示，显示了系统的基本配置：单段SCA只能检查一个102M. Banci等人理论计算机科学电子笔记116（2005）99铁路部门。 它由两个UCA组成，每个UCA放置在部分的一端;它们可以接收来自多达3个PRA的信号。此外，SCA系统可以根据组成UCA的数量和位于外部NOVRAM中的一组参数呈现多个配置，这些参数决定了给定配置的功能。我们参考[4]、[5]，了解其他配置及其功能的详细描述。在本文中，我们研究了一个特殊的情况下，单节配置，其中的主要轨道包括一个点，从一个次要的轨道离开。在这种SCA系统中，两个PRA与入口UCA相连，以这种方式进行所谓的侧翼保护（见图2）。由于存在额外的PRA，PRA和UCA之间的通信可能会比单段配置中的噪声更大，因此可能需要对来自DRT的信号进行额外的滤波图二. 带跟踪点的单节SCA。2.1SCA建模我们现在简要概述此配置的SDL规范：该模型主要再现与来自两个连接的PRA的信号的采集和处理相关的入口部分UCA子系统。实际上，在面向组件的SDL设计中，我们需要将M. Banci等人理论计算机科学电子笔记116（2005）99103处理来自两个PRA的数据所需的读取、过滤和轴序列检查过程的所有副本。图3a显示了这个细化链，直到AnalyzeTableSlot过程，该过程根据PRA计数的轴数确定区段是空闲的还是被列车占用。在PRA和连接的UCA之间存在噪声信道的情况下，可以调整所选配置，引入辅助滤波过程：事实上，在此SDL模型中，可以使用现有滤波器之间的相同接口插入新的滤波器组件;这反映了添加系列软件滤波器而不是以更高的成本修改和使现有滤波器更复杂的实际情况。在图3b中，描述了在下面的部分中，我们将展示一种基于MSC的验证技术，该技术从用于验证图3a的模型的一组MSC开始。我们还将指出面向组件的设计如何允许部分重用这些场景来验证修改后的模型。3面向构件设计验证SDL 规范的第一种方法是通过模拟。在[4]中报告的实验中，Cinderella SDL工具的模拟功能被用于对SCA系统进行初始验证，以确定其是否符合系统要求。在仿真活动期间，系统被处理为黑盒，其在适当的输入激励之后必须向系统环境发送期望的输出信号。仿真本质上是在规范级别执行的测试活动;在实践中，仿真验证工作场景的正确执行，即系统状态空间中的路径。相反，验证包括通过执行适当的算法来探索由系统过程生成的状态空间（通常由行为树表示）：或者是穷举搜索直到达到指定的深度，或者是在选择下一个要探索的状态时遵循各种不同标准的部分搜索不幸的是，尽管验证算法更强大，但通常不能探索系统的所有可能状态，因为状态空间爆炸现象会出现，特别是对于由并发状态机（如SCA）组成的复杂系统。实际上，这一事实阻止了调度来自环境的所有可能信号在系统理论术语中，作为持续的激励信号），特别是当104M. Banci等人理论计算机科学电子笔记116（2005）99图三. 不带和带辅助过滤组件的SCA模型（虚线圆圈）。采用穷举探索算法。因此，像SCA这样的大型系统的验证需要测量所执行的验证活动的实际数量。我们可以将覆盖率的概念转移到SDL模型的验证中，该概念广泛用于软件测试领域，以测量系统已被执行测试的百分比：选择程序的特定结构作为覆盖率的单位，因此语句覆盖率，分支覆盖率，条件覆盖率等概念可以用于测试。. . 通常使用。在SDL规范的情况下，Telelogic TAU等商业工具将覆盖概念应用于构成SDL模型的符号：如果所有符号都包含在一个验证分类中，则通过验证分类实现100%的符号覆盖。M. Banci等人理论计算机科学电子笔记116（2005）99105出现在系统状态机的SDL描述中（即，在SDL过程中）的图形元素已经被运用。这确保了SDL过程中定义的所有状态都得到了正确的验证，但可能没有考虑过程变量的所有可能值：事实上，如果我们认为系统由扩展有限状态机（EFSM）组成，两个系统状态是不同的，不仅因为过程的不同状态，而且因为分配给过程变量的不同值因此，符号覆盖从变量的值中抽象出来。由于无法探索整个状态空间，因此系统的验证仅限于探索接近工作场景的系统行为;因此，我们使用MSC驱动的验证来验证使用消息序列图形式主义描述的感兴趣场景; Telelogic TAU SDL和TTCN套件[8]中提供的SDL验证器允许通过采用Holzmann的位状态算法[ 9 ]（已在SDL规范[ 10 ]中体验过）执行此部分验证技术3.1增量和MSC驱动验证由于案例研究SDL模型的面向组件设计，最自然的验证技术是执行系统的增量验证为了在考虑的配置和组件中使用SCA系统的验证，我们需要使用合适的MSC场景来减少状态空间爆炸，这是由连接组件之间的约束交互的逐渐增长所产生的我们首先考虑并验证了无辅助过滤组件的SCA配置（图3a）;一组53个MSC已成功验证，获得91.75%的符号覆盖率这些MSC可以分为两组：• -10个MSC，表示黑盒交互（SDL系统与其环境的输入-输出信号）;• 43个MSC，用于执行SDL流程的内部状态验证前一组的MSC意味着在系统级验证与环境交互的模型的行为，将调度内部过程的转换的任务留给验证器工具;应用后一组的MSC对于调查来自环境的内部动态和特定的不可见系统状态是必要的，例如故障安全类型。图4示出了第一类型的MSC，其与进入区段的轴的计数有关;该MSC旨在验证106M. Banci等人理论计算机科学电子笔记116（2005）99系统对来自DRT的正确输入信号序列的响应，以执行区段占用（根据来自DRT的输入的滤波规则，对每个信号StateOfDrt采样三次）;图5中的MSC改为验证如果来自DRT的轴序列不正确，则系统进入内部故障安全状态错误见图4。 MSC方案涉及外部I/O行为。3.2确认为组件修改后的回归测试在SDL模型中添加或修改组件需要根据系统需求重新验证所描述的场景我们可以采用MSC验证技术作为修改后模型的适当回归测试活动。组件插入/修改后预期有两个结果：• SDL模型上的符号覆盖将被减少;• 有些场景将无法验证。这些后果是由于模型中SDL符号的插入或更改以及系统中引入的新功能M. Banci等人理论计算机科学电子笔记116（2005）99107图五. MSC方案，指定与错误处理相关的内部动态。见图6。 将新零部件与模型的其他零件连接。此外，在面向组件的设计中插入模块是基于图6所示的规则，即新组件应该符合与它将链接到的模型其他部分的接口，使用相同的在所采用的案例研究中，插入辅助滤波组件导致符号覆盖率下降，在对53个MSC的集合进行回归验证后，结果等于70，76%，这验证了原始模型。在53个MSC中，有27个没有得到验证;在验证方面，据说它们已经被侵犯。在27个被违反的MSC中，7个属于第一组，描述系统与环境的相互作用，而其他20个指定内部行为。108M. Banci等人理论计算机科学电子笔记116（2005）99我们可以使用覆盖查看器和SDL跟踪实用程序（由SDL验证器提供）来检测在修改后的模型的哪些部分中，违反的MSC的执行已经中断，从而支持重新设计 以获得期望的符号覆盖。见图7。 MSC违规后辅助过滤组件的部分覆盖。图7显示了应用于新过滤组件的违规MSC的部分覆盖（以灰色显示）;这是由于MSC描述的原始场景的通信语义与新组件的通信语义不一致。实际上，引入一个串联组件意味着与之交互的其他进程之间同步模式的改变。在使用前面提到的工具检测到系统结果的哪些部分未被覆盖之后，以下标准可能有助于重用相应的不再验证的MSC。为了定义一个MSC，如果我们对引入了新的串联元件的系统感到满意，我们应该集中精力研究这个元件所需的输入产生下一个组件所需的输出，如满意的MSC关于原始系统所指定的：因此，我们需要标记位于插入组件之后的细化链中的过程;然后，M. Banci等人理论计算机科学电子笔记116（2005）99109见图8。重复使用被违反的MSC：应该以适当的方式刺激添加的组件（虚线图），以便在处理链中获得相同的行为为了从该过程获得相同的输出信号，即相同的外部行为，我们需要在处理链中向后分析，并且从刚好在新组件之前的过程开始直到环境，检测哪些是导致新组件产生由标记的过程所期望的信号的激励序列，以便给出期望的输出。这在图8中举例说明，它显示了图5中所示场景的第一部分的重新定义，其中进程Drt-Seq tf到达内部状态DrtLiberi：原始场景的通信语义（即，需要哪些信号作为输入以让进程产生特定输出）建立了状态DrtLiberi的转换是可能的，如果信号DrtState由进程FiltrateDrt发送。在修改后的MSC中，在两个先前进程之间存在新的过滤组件Filtrate-DrtX 2意味着，为了在输出中产生先前由FiltrateDrt进程发送的相同DrtState信号并且因此允许DrtSeq tf在状态DrtLiberi中的传输，两个信号DrtState必须由FiltrateDrtX 2接收，相应于新组件的语义。这驱使我们复制来自110M. Banci等人理论计算机科学电子笔记116（2005）99环境（信号StateOfDrt）直到FiltrateDrt进程。需要在新场景中添加的信号被绘制为虚线。如果我们知道新组件和现有组件的通信语义，这些准则就可以应用：如果我们知道组件的内部结构，或者如果我们有MSC描述其所有可能的行为，这是可能的;后者只适用于小组件。此外，我们可以注意到，添加的组件越接近处理链的起点，则回归验证的覆盖范围将越小，因为MSC将很快被违反;然而，在这种情况下，MSC的重用将导致更便宜，因为从新组件向后应用到环境的更改将更少。4结论我们讨论了通过商业支持工具（即Telelogic TAU SDL验证器和模拟器）验证SDL指定系统的经验。经验集中在已经验证的模型的变化的回归验证上，显示了所使用的工具如何特别是，我们已经解决了在模型中添加新软件组件的情况，并且我们研究了如何使用消息序列图描述的违规场景来定义旨在全面覆盖新模型的新模拟场景。需要更多的实验来确认该方法的通用性;特别是，连接组件的不同拓扑结构将在未来的工作中解决。作为最终考虑，我们希望强调基于组件的SDL建模为自动代码生成带来的好处，因为在表示将下载到目标设备的系统时，这种工作正在进行处理的比较使用性能和复杂性估计的基础上的静态分析指标之间的C代码生成的Cmicro代码生成器的Telelogic TAU和手写版本开发的GETS。此外，我们可以注意到MSC指定的验证场景的可用性如何允许使用合适的工具自动执行测试用例生成，例如TelelogicTTCN。M. Banci等人理论计算机科学电子笔记116（2005）99111确认我们要感谢通用电气运输系统公司提供的案例研究。引用[1] ITU-T，建议Z.100-规范和描述语言（SDL）。日内瓦，1992年[2] ITU-T，建议Z.120-消息序列图（MSC）。日内瓦，1999年。[3] D. Harel，Statecharts：复杂系统的视觉形式主义。计算机程序设计科学，第8卷，第231-274页，1987年。[4] S. Bacherini，S.比安基湖卡佩基角Becheri，A.Felleca，A.Fantechi，E.Spinicci，使用SDL建模铁路信号系统。2003年5月在布达佩斯举行的FORMS 2003铁路运行和控制系统形式化方法国际研讨会论文集。[5] A. Fantechi，E.Spinicci，使用SDL建模和验证多配置铁路信号系统。TACoS 2003国际测试与分析研讨会论文集 基于组件的系统，华沙，2003年4月[6] J. Bohn，W. Damm，H. Wittke，J. Klose，A. Moik，使用Statemate和实时序列图建模和验证列车系统应用程序。综合设计和工艺技术，IDPT-2002，美利坚合众国，2002年6月[7] A. Cimatti，P. Pieraccini，R. P. Traverso，A. Villafiorita，重要协议的正式规范和验证。FM'99会议记录，法国图卢兹，1999年9月。LNCS 1709，Springer-Verlag。[8] TelelogicTAU 4.4用户手册，TelelogicAB，www.telelogic.com。[9] G. J. Holzmann设计和计算机协议验证。Prentice-Hall，1990年。[10] G. J. Holzmann验证SDL规范：实验。第九届协议规范、测试和验证国际研讨会论文集，荷兰特文特大学，1989年6月。