属性驱动的列车控制系统需求建模与验证

属性驱动的列车控制系统需求建模与验证

何丽芸, 赵林, 程瑞军

文章导航 > 铁路计算机应用 > 2014 > 23(2) : 1-6.

何丽芸, 赵林, 程瑞军. 属性驱动的列车控制系统需求建模与验证[J]. 铁路计算机应用, 2014, 23(2): 1-6.

引用本文:

何丽芸, 赵林, 程瑞军. 属性驱动的列车控制系统需求建模与验证[J]. 铁路计算机应用, 2014, 23(2): 1-6.

HE Liyun%ZHAO Lin%CHENG Ruijun, . Property-driven modeling and verification for requirements of Train Control System[J]. Railway Computer Application, 2014, 23(2): 1-6.

Citation:

HE Liyun%ZHAO Lin%CHENG Ruijun, . Property-driven modeling and verification for requirements of Train Control System[J]. Railway Computer Application, 2014, 23(2): 1-6.

属性驱动的列车控制系统需求建模与验证

北京交通大学轨道交通控制与安全国家重点实验室,北京,100044

详细信息

中图分类号: U284.4:TP39
计量
- 文章访问数: 85
- HTML全文浏览量: 4
- PDF下载量: 66
出版历程
- 收稿日期: 2014-02-14
- 录用日期: 2014-02-14
- 刊出日期: 2014-02-14

Property-driven modeling and verification for requirements of Train Control System

HE Liyun%ZHAO Lin%CHENG Ruijun,

摘要: 形式化语言越来越多地用来描述列车控制系统需求规范,其精确的语法和语义一方面有助于创建精确的需求模型、消除理解差异,另一方面也为进一步分析验证提供了基础.通过提出一种基于属性的需求分析方法,利用具体的形式化技术来分析需求.首先将由自然语言描述的需求规范转换为属性描述语言(PSL)形式化规范,并通过仿真和博弈分别进行语义检查和可实现性验证,最后通过断言来检验形式化语言所刻画的系统的精确性和完整性.该方法从自然语言形式的需求约束中直接提取相关需求规范,构造形式化模型并进行验证,为需求的早期确认提供了一种新的实用途径.并以CTCS-3级列控系统RBC切换场景为例,说明该方法的有效性.
- 需求规范 /
- 验证 /
- 列车控制系统 /
- 仿真 /
- 可实现性

参考文献(0)

资源附件(0)

计量

文章访问数: 85
HTML全文浏览量: 4
PDF下载量: 66
被引次数: 0

/

下载: 全尺寸图片幻灯片

分享

用微信扫码二维码

分享至好友和朋友圈

返回