| 基于UML的CTCS-3级列控系统需求规范形式化验证方法 |
| |
| 引用本文： | 刘金涛,唐涛,徐田华,赵林. 基于UML的CTCS-3级列控系统需求规范形式化验证方法[J]. 中国铁道科学, 2011, 32(3) |
| |
| 作者姓名： | 刘金涛 唐涛 徐田华 赵林 |
| |
| 作者单位： | 北京交通大学,轨道交通控制与安全国家重点实验室,北京,100044 |
| |
| 基金项目： | 国家自然基金重点资助项目，轨道交通控制与安全国家重点实验室自主研究课题 |
| |
| 摘 要： | 采用UML与符号模型检验相结合的方法,对CTCS-3级列控系统需求规范进行形式化验证.使用引入事件、可见变量抽象的方法,对需求规范UML模型进行扩展和抽象.根据转换规则,建立需求规范的NuSMV模型,并对NuSMV模型进行领域无关特性和领域相关特性的验证,通过反例对错误进行追踪、定位和修改.以需求规范中的模式转换为例,采用给出的形式化验证方法对其进行验证,验证结果确认模式转换满足活性、转移性、无死锁性、确定性及安全性的要求;验证过程表明UML与符号模型检验相结合的方法适用于CTCS-3级列控系统需求规范的验证.
|
| 关 键 词： | 列车控制系统 需求规范 形式化方法 符号模型检验 |
Formal Verification of CTCS-3 System Requirements Specification Based UML Model |
| |
| LIU Jintao,TANG Tao,XU Tianhua,ZHAO Lin. Formal Verification of CTCS-3 System Requirements Specification Based UML Model[J]. China Railway Science, 2011, 32(3) |
| |
| Authors: | LIU Jintao TANG Tao XU Tianhua ZHAO Lin |
| |
| Affiliation: | LIU Jintao,TANG Tao,XU Tianhua,ZHAO Lin(State Key Laboratory of Rail Traffic Control and Safety,Beijing Jiaotong University,Beijing 100044,China) |
| |
| Abstract: | With the method which integrated UML with symbolic model checking,the formal verification of CTCS-3 level system requirement specification was carried out.The UML model of requirement specification was extended and abstracted using event and visible-variable abstraction methods.According to the transformation rules,the NuSMV model of requirement specification was established.Verification for domain independent and domain dependent properties of NuSMV model was elaborated.Additionally,the approach of the cou... |
| |
| Keywords: | UML |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
