• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computers in railways XII: Computer system design and operation in railways and other transit systems >System safety property-oriented test sequences generating method based on model checking
【24h】

System safety property-oriented test sequences generating method based on model checking

机译：基于模型检查的面向系统安全性的测试序列生成方法

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

In this study, model checking is used to generate a suite of test sequences to validate whether the System Under Test (SUT) satisfies the defined safety properties. Firstly, a Coloured Petri Net (CPN) model is ed and derived from the system requirement specification of the SUT with a hierarchical modelling approach. A state space analysis is used to verify the model with respect to a set of correctness criteria that include the absence of deadlocks and livelocks. Secondly, some system safety properties defined by the experts are described with a non-standard query and extended computation tree logic. Finally, based on the model without deadlocks and livelocks, the negation of safety properties could be checked by analyzing the occurrence graph and the strongly connected components graph of the model. If the model does not satisfy the specified property, the process of model checking could return some counterexamples. From these counterexamples, the nodes and directed arcs that include the interface information are picked out as the interface messages, which are used to construct a test sequence. A case study of using this method on a railway control system is presented, where the CPN Tools is used to model and generate test sequences. All reachable states are analyzed to detect violations and generate the safety related test sequences, which include the required data to be executed on the SUT. The result shows this method is time-saving, labour-saving and can guarantee the conformance between the SUT and the safety properties.
机译：在本研究中，模型检查用于生成一组测试序列，以验证被测系统（SUT）是否满足定义的安全属性。首先，使用分层建模方法，从SUT的系统需求规范中创建并导出彩色Petri网（CPN）模型。状态空间分析用于相对于一组正确性标准（包括不存在死锁和活动锁）验证模型。其次，使用非标准查询和扩展的计算树逻辑来描述专家定义的一些系统安全属性。最后，基于没有死锁和活锁的模型，可以通过分析模型的出现图和强连接组件图来检查安全属性的否定。如果模型不满足指定的属性，则模型检查过程可能会返回一些反例。从这些反例中，包含接口信息的节点和有向弧被选作接口消息，用于构造测试序列。提出了在铁路控制系统上使用此方法的案例研究，其中使用CPN工具建模和生成测试序列。分析所有可达状态以检测违规并生成与安全相关的测试序列，其中包括要在SUT上执行的所需数据。结果表明，该方法省时，省力，可以保证被测件与安全性能的一致性。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号