|
文摘
|
由于CTCS-2级列控系统设计复杂,因此提出一种将统一建模语言(UML)与符号模型检验相结合的形式化建模与验证方法。分析CTCS-2级列控车载设备的模式转换场景,对其进行UML 建模得到UML 类图和状态图,制定转换规则对UML 模型进行扩展和抽象,使其转化为NuSMV 模型。将待验证的系统性质和转化后的检验程序输入符号模型检验系统进行验证,验证结果都为true,表明CTCS-2级列控车载设备的模式转化场景具有活性、可达性和安全性。 |
|
其他语种文摘
|
For the designing complexity of CTCS-2 system, this paper proposes the method combining Unified Modeling Language(UML) and Symbolic Model Checking(SMC) for modeling and formal verification. It analyzes the mode conversion scene of CTCS-2 on-board equipment. The mode conversion scene of CTCS-2 on-board equipment is modeled by using the UML, and UML class diagrams and UML state diagrams are gotten as well, through formulating some exchanging rules to extend and abstract UML model and exchanging it to the NuSMV model. The property of to be verified system and system Symbolic Model Verifier(SMV) model are inputted to symbolic model verifier to check. The verified results are true, and it shows that mode conversion scene of CTCS-2 on-board equipment has activity, accessibility and security. |
|
来源
|
计算机工程
,2013,39(3):12-15 【核心库】
|
|
关键词
|
列控系统
;
符号模型检验
;
形式化方法
;
车载设备
;
模式转换
|
|
地址
|
兰州交通大学自动化与电气工程学院, 兰州, 730070
|
|
语种
|
中文 |
|
文献类型
|
研究性论文 |
|
ISSN
|
1000-3428 |
|
学科
|
系统科学 |
|
基金
|
国家自然科学基金资助项目
;
甘肃省教育厅硕导基金资助项目
|
|
文献收藏号
|
CSCD:4775571
|
|
|
1.
古天龙.
软件开发的形式化方法,2005
|
被引
20
次
|
|
|
|
|
2.
屈喜龙. UML及面向对象的分析与设计的研究.
计算机应用研究,2005,22(9):74-76
|
被引
3
次
|
|
|
|
|
3.
王璐珍. UML顺序图的自动验证.
计算机工程与应用,2003,39(29):81-83
|
被引
1
次
|
|
|
|
|
4.
唐涛.
列车运行控制系统规范建模与验证,2010
|
被引
5
次
|
|
|
|
|
5.
刘金涛. 基于UML的CTCS-3级列控系统需求规范形式化验证方法.
中国铁道科学,2011,32(3):93-99
|
被引
6
次
|
|
|
|
|
6.
董昱.
区间信号与列车运行控制系统,2008
|
被引
7
次
|
|
|
|
|
7.
Beato M E. UML Automatic Verification Tool with Formal Method.
Electronic Notes in Theoretical Computer Science,2005,127(4):3-16
|
被引
1
次
|
|
|
|
|
8.
吴晓丹.
CTCS-3级列控系统的UML建模与模型检验研究,2010
|
被引
1
次
|
|
|
|
|
9.
刘中田. CTCS-3级列控系统车地交互流程形式化建模与验证.
北京交通大学学报,2011,35(2):76-81
|
被引
1
次
|
|
|
|
|
10.
徐啸明.
列控车载设备,2007
|
被引
1
次
|
|
|
|
|
11.
徐效宁.
基于UML的CTCS-2级列控车载设备的建模及实现,2008
|
被引
2
次
|
|
|
了解气象卫星更多信息，请访问