...
【24h】

The Metro Rio case study

机译:大都会里约案例研究

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

摘要

This paper reports on the Simulink/Stateflow based development of the on-board equipment of the Metro Rio Automatic Train Protection system. Particular focus is given to the strategies followed to address formal weaknesses and certification issues of the adopted tool-suite. On the development side, constraints on the Simulink/Stateflow semantics have been introduced and design practices have been adopted to gradually achieve a formal model of the system. On the verification side, a two-phase approach based on model-based testing and abstract interpretation has been followed to enforce functional correctness and runtime error freedom. Formal verification has been experimented as a side activity of the project. Quantitative results are presented to assess the overall strategy: the effort required by the design activities is balanced by the effectiveness of the verification tasks enabled by model-based development and automatic code generation.
机译:本文报告了基于Simulink / Stateflow的Metro Rio自动列车保护系统车载设备的开发情况。特别关注的是为解决所采用的工具套件的形式缺陷和认证问题而采取的策略。在开发方面,已经引入了对Simulink / Stateflow语义的约束,并采用了设计实践来逐步实现系统的正式模型。在验证方面,遵循了基于模型的测试和抽象解释的两阶段方法,以增强功能的正确性和运行时错误的自由度。正式验证已作为该项目的附带活动进行了试验。提出了量化结果以评估总体策略:设计活动所需的工作量与基于模型的开发和自动代码生成所实现的验证任务的有效性相平衡。

著录项

  • 来源
    《Science of Computer Programming》 |2013年第7期|828-842|共15页
  • 作者单位

    Dipartimento di Sistemi e Informatica (D.S.I.), Universita degli Studi di Firenze, Via di Santa Marta 3,50139 Firenze, Italy;

    Dipartimento di Sistemi e Informatica (D.S.I.), Universita degli Studi di Firenze, Via di Santa Marta 3,50139 Firenze, Italy;

    General Electric Transportation Systems, Via Pietro Fanfani, 21,50127 Firenze, Italy;

    General Electric Transportation Systems, Via Pietro Fanfani, 21,50127 Firenze, Italy;

    General Electric Transportation Systems, Via Pietro Fanfani, 21,50127 Firenze, Italy;

  • 收录信息 美国《科学引文索引》(SCI);美国《工程索引》(EI);
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

    Formal methods; Model-based development; Code generation; Railway;

    机译:正式方法;基于模型的开发;代码生成;铁路;

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号