Extended Petri Net Based Formal Modeling and Verification of WTB-TCN Device

摘要

This paper presents a formal methodology ofmodeling and verification about WTB-TCN device based onextended Petri net model. By translating the model into timedautomata, properties of WTB-TCN device can be completelyverified using symbolic model checking technique. Themethodology proposed addresses the model checking of criticalproperties of WTB-TCN device including safety, liveness andfairness properties which are expressed in computation treelogics. As a confirmation of its validity, the methodologydescribed in this paper has been successfully applied tomodeling and formal verification of WTB-TCN device.