Transform Dual Transition Timed Petri Net into Timed Automaton for Model Checking with UPPAAL

This paper presents the transformation of dual transition timed Petri Net (DTTPN) into timed automaton for model checking embedded system described in DTTPN which can model real-time embedded system in both control and data domain on different design phases. This paper proposes to transform a DTTPN model subnet into automaton, and then combine these concurrent subnets into whole one. For each DTTPN subnet, a time transition system is defined as active set net, which is bisimulated with this DTTPN subnet. Again by bisimulating this active set net, active set timed automaton is defined. Based on this active set timed automaton, model checking with UPPAAL can be carried out on events collision, resource constraints and so on. This paper gives the details of the transformation method, and model checking examples.