首页> 外文期刊>Design Automation for Embedded Systems >Applying infinite state model checking and other analysis techniques to tabular requirements specifications of safety-critical systems
【24h】

Applying infinite state model checking and other analysis techniques to tabular requirements specifications of safety-critical systems

机译:将无限状态模型检查和其他分析技术应用于安全关键系统的表格需求规范

获取原文
获取原文并翻译 | 示例

摘要

Although it is most often applied to finite state models, in recent years, symbolic model checking has been extended to infinite state models using symbolic representations that encode infinite sets. This paper investigates the application of an infinite state symbolic model checker called Action Language Verifier (ALV) to formal requirements specifications of safety-critical systems represented in the SCR (Software Cost Reduction) tabular notation. After reviewing the SCR method and tools, the Action Language for representing state machine models, and the ALV infinite state model checker, the paper presents experimental results of formally analyzing two SCR specifications using ALV. The application of ALV to verify or falsify (by generating counterexample behaviors) the state and transition invariants of SCR specifications and to check Disjointness and Coverage properties is described. The results of formal analysis with ALV are then compared with the results of formal analysis using techniques that have been integrated into the SCR toolset. Based on the experimental results, strengths and weaknesses of infinite state model checking with respect to other formal analysis approaches such as explicit and finite state model checking and theorem proving are discussed.
机译:尽管它最常用于有限状态模型,但近年来,符号模型检查已扩展为使用编码无限集的​​符号表示形式的无限状态模型。本文研究了一种称为动作语言验证程序(ALV)的无限状态符号模型检查器在以SCR(软件降低成本)表格表示形式表示的安全关键系统的正式要求规范中的应用。在回顾了SCR方法和工具,代表状态机模型的动作语言以及ALV无限状态模型检查器之后,本文提出了使用ALV正式分析两种SCR规格的实验结果。描述了ALV在验证或伪造(通过生成反例行为)SCR规范的状态和转换不变量以及检查不相交性和覆盖率属性中的应用。然后将使用ALV进行形式分析的结果与使用已集成到SCR工具集中的技术进行形式分析的结果进行比较。根据实验结果,讨论了无限状态模型检查相对于其他形式分析方法(如显式和有限状态模型检查以及定理证明)的优缺点。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号