Extended Petri net based formal modeling and verification of WTB-TCN device

This paper presents a formal methodology of modeling and verification about WTB-TCN device based on extended Petri net model. By translating the model into timed automata, properties of WTB-TCN device can be completely verified using symbolic model checking technique. The methodology proposed addresses the model checking of critical properties of WTB-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 WTB-TCN device.