基于UML的CTCS-3级列控系统需求规范形式化验证方法

Formal Verification of CTCS-3 System Requirements Specification Based UML Model

采用UML与符号模型检验相结合的方法,对CTCS-3级列控系统需求规范进行形式化验证。使用引入事件、可见变量抽象的方法,对需求规范UML模型进行扩展和抽象。根据转换规则,建立需求规范的NuSMV模型,并对NuSMV模型进行领域无关特性和领域相关特性的验证,通过反例对错误进行追踪、定位和修改。以需求规范中的模式转换为例,采用给出的形式化验证方法对其进行验证,验证结果确认模式转换满足活性、转移性、无死锁性、确定性及安全性的要求;验证过程表明UML与符号模型检验相结合的方法适用于CTCS-3级列控系统需求规范的验证。

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 specifi- cation 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 do- main independent and domain dependent properties of NuSMV model was elaborated. Additionally, the ap- proach 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 re- quirements of liveness, transition, non-deadlock, determinacy and safety. The process of verification shows that the method which integrates UMI. with symbolic model checking is suitable for the verification of CTCS-3 level system requirement specification.