llows the modeler to construct a SIP model by using a number of small CPNs, which are related to each other in a well- defined way. Temporal Petri Net [28], just as its name implies, timed factors are added to Petri Net to consider time in modeling and simulation. Learned from RFC 3261, we know that timer is an important factor for SIP service, which deals with overtime and retransmission. So, timed modeling of SIP is necessary and important. In the chapter, we added a time factor to HCPN into timed HCPN and utilize a tool called CPN tools [29] for practical modeling and simulation. In next section, we focus on the formal definition of the timed HTPN by use of which to model and simulate SIP in order to solve concrete problems. 16.3 Modeling and Simulation of SIP through Timed Hierarchical CPN and CPN Tools 16.3.1 Formal Definition of Timed HCPN and CPN Tools In order to further understand timed HCPN and the modeling method of SIP, We give the formal definition of timed HCPN. As the base of timed HTCPN CPN, the following is the formal definition of CPN from [27]. Definition 16.1 A Colored Petri Net (CPN) is a nine-tuple CPN = (, P, T, A, N, C, G, E, IN), satisfying: is a finite set of non-empty types, called colored sets. P is a finite set of places. © 2009 by Taylor & Francis Group, LLC SIP Modeling and Simulation T is a finite set of transitions. A is a finite set of arcs that = PNA = TNA = 0 P TUTXP is a node function. is a color function denotes tokens in a place. G is a guard function, which is defined from T into expressions such that: At E T: [Type(G(t)) = Bool ^ Type(Var(G(t))) C ]. E is an arc expression function, which is defined from A into expressions such that: Va E A: [Type(E(a)) = C(p(s)) MS ^ Type(Var(E(a))) U . IN is an initialization function. It is defined from P into closed expressions such that: Ap E P: [Type(IN(p)) = C(p(s)) MS ^ Var(IN(p)) = 0] where Type(expr) denotes the type of an expression and Var(expr) denotes the set of variables in an expression. An HCPN consists of a set of subnets