Abstract: By integrating the features of colored Petri net and timed Petri net, this paper proposes a formal modeling method for embedded systems. In the proposed method, the data, control information and timestamp are represented in places, and the timedelay, control function and transition function are introduced in the transitions. Moreover, inhibitor arcs are used to simplify the model. The proposed method can model complex embedded systems and analyze properties of the system by using the existing Petri nets techniques. A case study shows the applicability and feasibility of the method.