【摘 要】
：
采用UML与符号模型检验相结合的方法,对CTCS-3级列控系统需求规范进行形式化验证。使用引入事件、可见变量抽象的方法,对需求规范UML模型进行扩展和抽象。根据转换规则,建立
【机 构】
：
北京交通大学轨道交通控制与安全国家重点实验室
论文部分内容阅读
采用UML与符号模型检验相结合的方法,对CTCS-3级列控系统需求规范进行形式化验证。使用引入事件、可见变量抽象的方法,对需求规范UML模型进行扩展和抽象。根据转换规则,建立需求规范的NuSMV模型,并对NuSMV模型进行领域无关特性和领域相关特性的验证,通过反例对错误进行追踪、定位和修改。以需求规范中的模式转换为例,采用给出的形式化验证方法对其进行验证,验证结果确认模式转换满足活性、转移性、无死锁性、确定性及安全性的要求;验证过程表明UML与符号模型检验相结合的方法适用于CTCS-3级列控系统需求规范的
其他文献
中国铁道科学研究院坚持“行业服务为立院之本,成果转化为兴院之策”的建院方针,在铁路现代化建设中勇担重任,按照“五个一流”目标加快推进一流科研院所建设,充分发挥科技综
为解决铁路道岔区段轨距和线型难以保持、外轨外倾且侧磨严重等问题，在铁路普通轨撑的基础上研制道岔弹性轨撑。该弹性轨撑的背面粘贴了厚4mm的硫化橡胶垫，增加了其横向弹性；对
在悬索模型的基础上,通过将集中载荷替换成分布载荷在算法中引入接触线和承力索的抗弯刚度2个参数,通过提出拉出值等效吊弦分布的概念在算法中计算接触线拉出值对悬挂系统静
中国铁道科学研究院正在建设的最高试验速度500km.h-1的1∶1全尺寸高速轮轨关系试验台是高速铁路系统试验国家工程实验室的重要建设项目之一,是研究轮轨关系的重要技术装备。
在不改变现有钢轨焊接工艺的条件下，研究采用非接触式测量方法的钢轨几何参数在线自动测量系统。该系统主要由传感器集成控制单元、测量单元以及数据处理与管理单元组成；采用激
以随机振动理论为基础,对Scanlan基于桥梁的颤抖振分析理论加以气动导纳函数修正应用于列车抖振分析中。提出了列车抖振反应谱理论与计算方法。水平风谱引用Simiu经验公式,竖
根据对城市轨道交通ATP车载设备功能的分析,搭建了模拟车辆外部接口的城市轨道交通ATP车载设备测试环境,确定了测试ATP车载设备的10个安全输入参数和7个非安全输入参数。基于
基于已有的信息编码方法,结合生产制造业和产品的编码经验,提出基于对象的信息编码方法。该方法将铁路公用基础信息作为对象,采用基于对象的方法,分析对象的属性和对象之间的关联关系,形成铁路公用基础信息分类体系。根据分类体系构造类别码。分析对象的基本属性。根据选取的属性构造类别码和辅助码。采用专家知识库和优化算法优化选取适于编码的属性,利用对象的继承性,形成编码模型。根据编码模型和编码规则,将类别码、属性
根据车载雷达测速传感器的工作原理和雷达天线夹角的变化规律,建立测速传感器性能退化的数学模型。利用建立的数学模型和轨旁应答器提供的列车运行距离,推导出列车运行距离与
2011年2月17日,铁道部科技司组织验收专家组对中国铁道科学研究院承担的《高速铁路标准体系深化研究》及《铁路重载技术标准体系研究》课题进行验收。