...
首页> 外文期刊>International Journal on Software Tools for Technology Transfer >Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B
【24h】

Formalising the Hybrid ERTMS Level 3 specification in iUML-B and Event-B

机译:在iUML-B和Event-B中正式形成混合ERTMS 3级规范

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

摘要

We demonstrate refinement-based formal development of the hybrid, 'fixed virtual block' approach to train movement control for the emerging European Rail Traffic Management System (ERTMS) level 3. Our approach uses iUML-B diagrams as a front end to the Event-B modelling language. We use abstraction to verify the principle of movement authority before gradually developing the details of the Virtual Block Detector component in subsequent refinements, thus verifying that it preserves the safety properties. We animate the refined models to demonstrate their validity using the scenarios from the Hybrid ERTMS Level 3 (HLIII) specification. We reflect on our team-based approach to finding useful modelling abstractions and demonstrate a systematic modelling method based on the state and class diagrams of iUML-B. The component and control flow architectures of the application, its environment and interacting systems emerge through the layered refinement process. The runtime semantics of the specification's state-machine behaviour are modelled in the final refinements. We discuss how the model could be used to generate an implementation using code generation tools and techniques.
机译:我们展示了基于混合动力的“固定虚拟块”方法的完善改进形式,该方法用于新兴的欧洲铁路交通管理系统(ERTMS)3级列车的运动控制。我们的方法使用iUML-B图作为Event- B建模语言。我们使用抽象来验证移动授权的原理,然后在随后的改进中逐步开发Virtual Block Detector组件的详细信息,从而验证它保留了安全性。我们对改进的模型进行动画处理,以使用Hybrid ERTMS Level 3(HLIII)规范中的场景演示其有效性。我们反思了基于团队的方法来找到有用的建模抽象,并演示了基于iUML-B的状态图和类图的系统建模方法。应用程序的组件和控制流体系结构,其环境和交互系统通过分层的优化过程出现。在最后的改进中,对规范的状态机行为的运行时语义进行了建模。我们讨论如何使用代码生成工具和技术将模型用于生成实现。

著录项

相似文献

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

客服邮箱:kefu@zhangqiaokeyan.com

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

  • 服务号