 is proposed in Section 16.3. 16.2 General Formal Modeling Methodologies and Tools for SIP There are a lot of general formal methodologies and tools for SIP modeling and simulation. Different tools are suitable for specific research purposes of SIP. Although there are programming languages like C, JAVA is a programming language to define and develop SIP modules and implementation languages like XML to test compatibility and protocol stacks of SIP [20], it is always cost-inefficient to use these methods. In this section, we focus on some simple but useful graphical modeling methods and tools. As SIP is a control-plane protocol, SIP modeling is discussed from finite state machine (FSM), which is used in standard RFCs followed by unified modeling language (UML) for SIP application development to the Petri Net cluster for complex modeling and further simulation. 16.2.1 Finite State Machine (FSM) Seen from the standard RFCs of SIP, most models are represented by FSM. Even an FSM framework is established for SIP extensions [21]. FSM is a simple graphical tool that focuses on states and events and is useful to describe the control flow of a system. Protocol processes can often be modeled as a collection of communicating finite state machines [11]. For SIP modeling, it consists of four elements [21]. S: States that define behavior and can produce actions T: State transitions that are changing from one state to another R: Rules or conditions that are to be met to allow a state transition E: Events that are either externally or internally generated, which can possibly trigger rules and lead to state transitions For SIP modeling, transaction procedures can be represented as one or more state machines. The formal model of a communicating finite state machine plays an important role in the formal validation of protocol, protocol synthesis, and its conformance testing [11]. Figure 16.1 is an FSM model with the formal definition of the INVITE client transaction procedure defined in RFC 3261. As we know, SIP should be used in co