Abstract: Most Real-time Embedded Systems have been used in safety-critical situation, which is necessary to ensure the correctness of systems. The growing complexity of real-time embedded systems makes it imperative to apply formal analysis techniques at early sta

Key words: Colored time petri net,Timed automata,CTPN-to-TA, Model checking