Formal Verification of CTCS-3 System Requirements Specification Based UML Model
Lin Zhao · Zhongguo tiedao kexue · 2011
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.