基于aadl的中国列车控制系统运行权限场景的行为建模与验证。

像大多数数字控制器一样,列车控制系统按照定义是混合系统,因为它们相互作用与或尝试控制物理世界的某些方面。具有约束条件的详细行为建模可靠性预测所需的功能和形式验证对混合系统设计人员来说是一个巨大的挑战。列车控制系统通过计算单元与控制单元之间的广泛交互进一步加剧了这一挑战。它们的物理环境以及彼此之间的相互依赖。在本文中,我们调查了行为使用建筑分析模型对中国列车控制系统3级(CTCS-3)进行建模和形式验证- ysis和设计语言(AADL)来应对这一挑战。 AADL是用于嵌入式系统,并且基于基于模型的工程范式。连同em-的结构建模使用核心语言构造的嵌入式系统,AADL还通过以下方式提供对语言扩展的支持:附件子语言。在系统需求规范文档中,CTCS-3的行为指定为一组相互配合以实现列车安全可靠功能的基本操作方案。本文探讨的运动授权(MA)方案被认为是基本且最关键的方案以防止火车相互碰撞。对控制系统的详细离散行为建模并使用带有软件的嵌入式系统行为语言(BLESS)附件子语言进行了验证和ADL的连续行为,以及网络与物理之间的相互作用(火车和控制系统)使用“混合附件”子语言建模。 MA场景的行为在系统