期刊文献+
共找到3篇文章
< 1 >
每页显示 20 50 100
基于混合通信顺序进程的高速铁路列控系统形式化建模与验证方法 被引量:2
1
作者 吕继东 李开成 +1 位作者 唐涛 袁磊 《中国铁道科学》 EI CAS CSCD 北大核心 2012年第5期91-97,共7页
针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法。引入了HCSP的假设条件,建立列控系统的行为模型;定义了HCSP到混合自动机(HA)的转换规则,将HCSP模型转换成HA模型;利用模型检验工具... 针对高速铁路列控系统的混杂特性,提出一种基于混合通信顺序进程(HCSP)的列控系统形式化建模与验证方法。引入了HCSP的假设条件,建立列控系统的行为模型;定义了HCSP到混合自动机(HA)的转换规则,将HCSP模型转换成HA模型;利用模型检验工具PHAVer对HA模型进行自动验证。以高速铁路列控系统典型的行车许可运营场景为例,建立区间闭塞分区行车许可场景的HCSP模型;根据转换规则将行车许可场景的HCSP模型转换成HA模型;用PHAVer验证了所建立的区间闭塞分区行车许可场景模型的正确性,从而证明了基于HCSP的高速铁路列控系统建模及验证方法的有效性。 展开更多
关键词 高速铁路列控系统 混合通信顺序进程 混合自动机 行车许可场景
在线阅读 下载PDF
高速铁路列控系统运营场景实时性的建模与验证 被引量:10
2
作者 吕继东 唐涛 《铁道学报》 EI CAS CSCD 北大核心 2011年第6期54-61,共8页
高速铁路列控系统是一个典型的分布式实时系统,其时间约束主要反映在运营场景中子系统之间的交互过程中。时序逻辑的扩展方法并不能完全满足描述分布式实时系统性质的需要,并且随着系统的复杂性提高,列控系统运营场景中诸如超时、期限... 高速铁路列控系统是一个典型的分布式实时系统,其时间约束主要反映在运营场景中子系统之间的交互过程中。时序逻辑的扩展方法并不能完全满足描述分布式实时系统性质的需要,并且随着系统的复杂性提高,列控系统运营场景中诸如超时、期限、直到…才等形式化描述与验证上存在不足。本文提出一种适合于列控系统场景建模与验证的方法,其核心思想是使用混合通信顺序进程HCSP(Hybrid Communicating Sequential Process)形式化描述分布式实时系统模型,提出转换规则,转换成时间自动机网络模型并进行自动验证。最后通过对典型场景无线闭塞中心RBC(Radio Block Center)切换的相关属性进行建模与验证,分析证明方法的有效性。 展开更多
关键词 列控系统 时间约束 混合通信顺序进程 时间自动机 RBC切换
在线阅读 下载PDF
基于HCSP的列控系统安全性建模与验证分析 被引量:1
3
作者 吕继东 唐涛 +1 位作者 李开成 王海峰 《铁路计算机应用》 2017年第1期11-17,共7页
高速铁路列车运行控制系统是保证列车安全、高效运行的核心设备,如何验证系统功能的正确性从而提高系统的安全性是至关重要的。引入了一种基于进程演算的方法—混合通信顺序进程(HCSP,Hybrid Communication Sequential Process),利用该... 高速铁路列车运行控制系统是保证列车安全、高效运行的核心设备,如何验证系统功能的正确性从而提高系统的安全性是至关重要的。引入了一种基于进程演算的方法—混合通信顺序进程(HCSP,Hybrid Communication Sequential Process),利用该方法对列控系统进行了形式化描述,并针对典型的场景—注册与启动场景进行了HCSP建模,通过引入转换规则,进行了相应模型转换,应用模型检验工具UPPAAL进行了仿真和功能验证,验证结论表明了场景模型功能的正确性以及方法的可行性。 展开更多
关键词 列车运行控制系统 安全性 混合通信顺序进程 注册与启动 模型转换 验证
在线阅读 下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部