A Coloured Petri Net Based Formal Verification Methodology of MVB-TCN Device

This paper presents a formal verification methodology of the Coloured Petri Net model of MVB-TCN device using symbolic model checking technique. The methodology proposed addresses the model checking of critical properties of MVB-TCN device including safety, liveness and fairness properties which are expressed in computation tree logics. As a confirmation of its validity, the methodology described in this paper has been successfully applied to modeling and formal verification of Line Redundancy Control unit of MVB-TCN device.