中国铁道科学2011，Vol.32Issue(3)：93-99,7.
基于UML的CTCS-3级列控系统需求规范形式化验证方法
Formal Verification of CTCS-3 System Requirements Specification Based UML Model
摘要
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 counterexample was proposed for tracking, locating and correcting errors.Taking the mode switch in the requirement specification for example, the proposed formal verification method was adopted for the verification of mode switch.The result of verification shows that mode switch can satisfy the requirements of liveness, transition, non-deadlock, determinacy and safety.The process of verification shows that the method which integrates UML with symbolic model checking is suitable for the verification of CTCS-3 level system requirement specification.关键词
列车控制系统/需求规范/形式化方法/UML/符号模型检验Key words
Train control system/ Requirement specification/ Formal method/ UML/ Symbolic model checking分类
交通工程引用本文复制引用
刘金涛,唐涛,徐田华,赵林..基于UML的CTCS-3级列控系统需求规范形式化验证方法[J].中国铁道科学,2011,32(3):93-99,7.基金项目
国家自然基金重点资助项目(60634010) （60634010）
轨道交通控制与安全国家重点实验室自主研究课题(RCS2008ZZ005) （RCS2008ZZ005）
