国家自然科学基金(60634010)

作品数：62被引量：510H指数：13
导出分析报告
相关作者：唐涛毛保华丁勇刘海东杜鹏更多>>
相关机构：北京交通大学香港理工大学西安交通大学北京铁路局更多>>
相关期刊：《交通运输工程学报》《交通运输系统工程与信息》《铁道科学与工程学报》《交通信息与安全》更多>>
相关主题：CBTCCTCS-3级列控系统轨道交通形式化方法节能运行更多>>
相关领域：交通运输工程自动化与计算机技术机械工程经济管理更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
电动自行车干扰下的HCM2000模型算法研究
《价值工程》2016年第15期218-221,共4页赵强 成卫 孙娇 
国家自然科学基金(60634010)~~
在城市道路交叉口,电动自行车(简称电动车)对机动车通过交叉口的通行效率产生了很大干扰,本文对电动车产生的干扰进行了研究,通过对昆明市多个交叉口的数据分析,结合交叉口禁左的渠化设计,以绿灯时间内的干扰时间长度(干扰时间)、电动...
关键词：交通工程 通行能力 HCM2000模型算法 电动自行车 SPSS 干扰时间 
列车运行控制系统中安全通信协议的形式化分析被引量：11
《铁道学报》2012年第7期70-76,共7页陈黎洁 单振宇 唐涛 
国家科技支撑计划(2009BAG14B01);国家自然科学基金(60634010)
安全通信协议是保证基于通信的列车运行控制系统中通信安全的主要因素,其性质和最终实现正确的形式化验证具有重要意义。本文将欧洲列车运行控制系统安全通信协议规范中的一些未强制规定的要求明确化,选择分层赋时有色Petri网(CPN)对修...
关键词：安全通信协议 ETCS EURORADIO 有色PETRI网 形式化分析 
CBTC列车安全定位中通信中断时间的研究被引量：7
《铁道学报》2012年第6期40-45,共6页刘宏杰 陈黎洁 
国家支撑计划项目(2009BAG14B01);国家自然科学基金项目(60634010)
通信中断的存在会对目前城市轨道交通的CBTC列车安全定位产生影响,进而影响列车安全间隔距离。CBTC车地通信系统大多采用无线局域网技术。越区切换中断是导致通信中断的主要原因,根据IEEE 802.11协议的越区切换流程,本文推导出越区切换...
关键词：安全包络 估计的运行距离 安全间隔距离 通信中断 越区切换 802.11 
一种基于模型的形式化测试序列自动生成方法及在ETCS-2中的应用被引量：10
《铁道学报》2012年第5期70-80,共11页赵显琼 郑伟 唐涛 
国家自然科学基金(60634010);国家863高技术研究发展计划(2009AA11Z221);中央高校基本科研业务费专项资金(2009YJS013)
随着中国铁路列车运行控制系统的发展,对列控系统的研究越来越受到学术界的关注。本文提出一种基于模型的形式化测试案例和测试序列生成方法,并应用于ETCS-2级系统的测试中。首先提出有色Petri网(CPN)的建模规则,保证CPN模型适应测试生...
关键词：ETCS-2 有色PETRI网 测试生成 形式化方法 
磁悬浮列车跨系统运行Petri网模型被引量：3
《交通运输工程学报》2012年第2期112-118,共7页郑伟 
国家自然科学基金项目(60634010);国家863计划项目(2011AA010104);中央高校基本科研业务费专项资金项目(2011JB2004)
根据磁悬浮列车跨系统运行需求,研究了其运行控制系统的总体框架,明确了需要增加的功能子系统。基于系统理论,采用Petri网对系统关键属性、列车运行过程及各子系统的功能进行了层次化的建模。最高层模型描述系统整体关键属性,低层模型...
关键词：交通控制 磁悬浮列车 跨系统运行 PETRI网 系统理论 层次化模型 可靠性 
基于随机Petri网的GSM-R双层网络建模与性能分析被引量：4
《铁道学报》2012年第3期75-82,共8页陈黎洁 唐涛 
国家科技支撑计划项目(2009BAG14B01);国家自然科学基金项目(60634010)
利用随机Petri网,综合信道降质、链路中断、越区切换、灾害等因素,建立GSM-R的同站址网络与交织站址网络的故障模型,针对同站址与交织站址两种不同的网络结构,给出利用马尔可夫链求解可靠性与可用性的方法。通过马尔可夫链的有关概率分...
关键词：GSM-R 可靠性 可用性 随机PETRI网 同站址网络 交织站址网络 
多端口形式化测试自动生成方法在CTCS-3车载系统中的应用被引量：10
《铁道学报》2011年第7期44-51,共8页赵显琼 唐涛 
国家自然科学基金项目(60634010);国家高技术研究发展计划(863计划)(2009AA11Z221);轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005)
针对CTCS-3列控系统测试中普遍存在的需要多个端口协同测试的问题,在时间输入输出自动机(TIOA)的基础上,提出端口标记的时间输入输出自动机(LpTIOA)。LpTIOA除在模型中能够反映系统的时间约束特性外,还能反映系统输入输出行为对应的端...
关键词：CTCS 时间自动机 车载系统 UPPAAL 实时系统 COVER 
CTCS-3级列控系统规范的建模与形式化验证方法研究被引量：13
《铁道学报》2011年第7期67-72,共6页谢雨飞 唐涛 徐田华 赵林 
国家自然科学基金资助项目(60634010);轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005)
CTCS-3级列控系统规范是CTCS-3级列控系统设计与开发的基础,是实现互联互通以及确保系统高效率与安全性的关键环节。然而,依靠经验与直觉制定的规范不可避免地存在某些漏洞或者安全隐患,因此对CTCS-3级列控系统规范进行建模与形式化验...
关键词：CTCS-3级列控系统 系统规范 建模 形式化验证 
安全苛求系统综合功能危险源分析方法的研究被引量：2
《铁路计算机应用》2011年第7期1-4,共4页李雷 王海峰 唐涛 
国家自然科学基金重点项目(60634010)
基于经典方法改进的安全分析方法—综合功能危险源分析(IFHA),综合了功能故障分析(FHA)、故障模式及影响分析(FMEA)、瞬时故障和可操作性研究(HAZOP)以及故障树分析(FTA)的分析原理,通过不同分析阶段结果的关联以及统一的故障树表示,保...
关键词：安全苛求系统 安全分析 ZC系统 FHA FMEA FTA 
基于UML的CTCS-3级列控系统需求规范形式化验证方法被引量：10
《中国铁道科学》2011年第3期93-99,共7页刘金涛 唐涛 徐田华 赵林 
国家自然基金重点资助项目(60634010);轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005)
采用UML与符号模型检验相结合的方法,对CTCS-3级列控系统需求规范进行形式化验证。使用引入事件、可见变量抽象的方法,对需求规范UML模型进行扩展和抽象。根据转换规则,建立需求规范的NuSMV模型,并对NuSMV模型进行领域无关特性和领域相...
关键词：列车控制系统 需求规范 形式化方法 UML 符号模型检验 
全选清除导出
共7页<1234567>
检索报告 对象比较 聚类工具 使用帮助 返回顶部