Automata Wiki

Related publications: [AJU10]

The Mapper

The parameters From, To, and Contact must be pre-configured in a session with ns-2, so they are set to constant values throughout the experiment. The Via parameter is a pair, consisting of a default address and a variable branch. The parameters Via, CallId, and CSeq are potentially interesting parameters. Monitoring of membership queries reveals that for each of these parameters, the ns-2 SIP implementation remembers the value which is received in the first Invite message (presumably, it is interpreted as parameters of the connection that is being established). The implementation also remembers the value received in the most recent input message when producing the corresponding reply, but thereafter forgets it. We therefore equip the mapper with six state variables. The state variable firstId stores the CallId parameter of the first Invite message, and lastId stores the CallId parameter value of the most recently received message. The state variables firstCSeq and lastCSeq store the analogous values for the CSeq parameter, and the state variables firstVia and lastVia for the Via parameter.

The abstraction mapping for input symbols is shown in Table 1. Intuitively, the input parameter CallId is compared with the variable firstId (assigned at the occurrence of the first Invite message) to check if it should be mapped to FIRST or LAST. For the input parameters Via and Cseq, we merged the abstract values FIRST and LAST into the single value ANY, since we found that these input parameters are not tested by ns-2. In output messages, for which the mapping is shown in Table 2, these three parameters can take the value received in the first Invite message, or the value in the just received message, corresponding to the two abstract values FIRST and LAST.

Table 1. Mapping table for input messages of SIP Server

Table 2. Mapping table for output messages of SIP Server

The Learned Model

Fig. 1: Pruned SIP model with 9 locations and 48 transitions. For presentation purposes, we have pruned the model as follows: (1) removing transitions triggered by abstract symbols that have no corresponding concrete symbol: the Mapper will immediately reject these, and react with a distinguished error symbol, (2) removing transitions with empty input and output symbol, i.e., with labels nil/timeout, (3) removing locations which have become unreachable after the previous steps. For readability, some transitions with same source location, output symbol and next location (but with different input symbols) are merged: the original input method types are listed, separated by a bar (|). Due to space limitations, we have suppressed the (abstract) parameter values. However, the CallId parameter of the input messages with abstract value FIRST, is depicted in the model with solid transition lines, the remaining transitions have a dashed line pattern. We suppressed all other parameters in the figure.

Fig. 2: Complete SIP model with 10 locations and 70 transitions.