Takeshi NAGAOKA † , Akihiko ITO † , Kozo OKANO † , and Shinji KUSUMOTO † †Graduate School of Information Science and Technology, Osaka University Yamadaoka 1–5, Suita City, Osaka, 565-0871, Japan The Internet is a best-effort network shared by a number of users, so there is no guarantee on the QoS properties such as network bandwidth, delay and throughput.  Therefore, sys- tem developers preliminarily have to estimate the QoS by simulation techniques or mathematical analysis.  Probabilis- tic model checking can evaluate performance, dependability and stability of information processing systems with random behaviors. PRISM is one of probabilistic model checkers. It handles automata with probabilities (discrete and continuous time Markov chains) and time elapse.  This paper presents a discrete Markov chain for a real-time distributed system, and evaluates its QoS properties using the simulation function of PRISM. As the target real-time distributed system, we use an experimental system whose main subsystem is video data transmission which uses RTSP (Real Time Streaming Pro- tocol) for the streaming protocol.  The system has also ftp servers and clients which exploit tcp connections, as well as a packet generator that generates udp packets as background noise.  Thus, the system involves several simultaneous con- nections; it may occur congestion. To validate the correctness of our model, we also model it in a model for the well-known network simulator NS–2. The paper gives the comparison of their simulation results. The comparison shows that the result of PRISM simulation is very similar to that of NS–2. The re- sults show that the proposed method is useful to analyze the network performance. Keywords: Real-time Distributed System, Model Check- ing, PRISM, Formal Verification
Introduction
1
Nowadays real-time distributed systems like streaming me- dia systems are widely spreading. These systems require time based transmission such as QoS control to prevent interrup- tion of packet transmission caused by network delay, packet loss, and so on. Since the Internet is a best-effort network shared by a num- ber of users, there is no guarantee on the QoS properties such as network bandwidth, delay and throughput. Therefore, sys- tem developers preliminary have to estimate the QoS by sim- ulation techniques[2] or mathematical analysis[4]. Simulation techniques usually do not guarantee qualitative properties such as the maximum throughput and the mini- mum jitter, and so on, though they can calculate mean-values along typical traces. In general, these techniques use much resources to simulate accurately the target network systems. On the other hand, mathematical analysis is logically correct and needs fewer computation resources, but in many cases the based models are too simple and ideal; hence it is hard to apply the mathematical analysis to realistic applications. Formal verification techniques, especially model checking techniques[3] are considered as promising techniques for in- formation system developing due to their ability of exhaustive checking.  Among them, probabilistic model checking can evaluate performance, dependability and stability of informa- tion processing systems with random behaviors. PRISM[1] is one of probabilistic model checkers. It handles automata with probabilities (discrete and continuous time Markov chains) and time elapse.  Therefore, it is suitable for modelling the network systems. This paper presents a discrete Markov chain for a real- time distributed system, and evaluate its QoS properties us- ing the simulation function and the verification function of PRISM. As the target real-time distributed system, we use an experimental system shown in Fig.1.  The main subsystem of the system is video data transmission which uses RTSP (Real Time Streaming Protocol) for the streaming protocol. The system has also ftp servers and clients which exploit tcp connections, as well as a packet generator that generates udp packets as background noise. Thus, the system involves sev- eral simultaneous sessions; it may occur congestion. This paper analyzes newly throughput property. The anal- ysis is performed on two levels; one is detail models, and the other is abstract level.  On the detail level, several numeric analysis is performed, whereas on the abstract level, qualita- tive verification is performed. To validate the correctness of our model, we also model it in a model for the well-known network simulator NS–2[2], and give the comparison of their simulation results.  The comparison shows that the result of PRISM simulation is very similar to that of NS–2. As related works, several case-studies are performed using PRISM [8]–[10]. For example, Paper [9] deals with network protocol. The rest of the paper is organized as follows.  Sec.2 gives some backgrounds, especially overviews of PRISM and NS– 2, as preliminaries. Sec.3 describes the example real-time dis- tributed systems which uses streaming media.  Explanations on several famous protocols for real-time video systems are also given. Sec.4 and 5 provide concrete models of the exam- ple network described in Prism and NS–2, respectively. Sec.6 and 7 show the results of comparison and gives discussions. Finally Sec.8 concludes the paper.
Preliminaries
2
This section simply describes Prism and NS–2 as well as network protocols for net streaming.
2.1
Probabilistic Model Checking tool PRISM
Here, we simply describe overview of probabilistic Model Checking tool PRISM[1]. A model checking tool usually has two inputs, a model M and a logical expression p . The model is typically a transi- tion system which represents behavior of the system to check; while the logical expression is a temporal logic expression which represents a property to check. The typical output of the model checking tool is whether the logical expression is valid on the model ( M |= p ). Some model checker outputs a counter example when p is invalid. The inputs of PRISM include the following three kind of transition system as a model: ● Discrete-time Markov chains (DTMC); ● Continuous-time Markov chains (CTMC); and ● Markov decision processes (MDP). Each of three systems is a probabilistic transition system (Markov chain).  The inputs of PRISM also include Proba- bilistic Computation Tree Logic (PCTL)[11] for DTMC and MDP, and Continuous Stochastic Logic (CSL)[12] for CTMC. They are CTL based logics enchanted with probability. PRISM has several analysis modes: simulation mode, nu- merical analysis mode, and verification mode. Using the sim- ulation mode, we can observe the behavior of the given model system visually. This mode uses only a model as input. Nu- merical analysis mode can evaluate the value of uncertain variable specified with PCTL or CSL based on the model. Such numerical analysis is considered as a kind of parametric model checking[13].  PRISM can draw a graph with several trials of such numeric analysis. Verification mode is like typi- cal model checking except that PRISM cannot output counter examples. In this paper, we use DTMC's as the model of the network. Here, we describe more precisely on a DTMC. Formally, a DTMC D is a tuple ( S, s_init, P, L ), where ● S is a set of states ("state space") ; ● s_init ∈ S is the initial state; ● P : S × S → [0, 1] is the transition probability matrix where ∑ s ′ ∈ s P(s, s ′ ) = 1 for all s ∈ S ′ ; and ● L : S → 2 AP is function labelling states with atomic propositions. PRISM allows a transition to specify an action and updat- ing expressions on D , where D is a set of variables with finite domain. In other words, a DTMC of PRISM is a kind of ex- tended automaton with probabilities. Usually, one execution of a transition is translated into a unit time of time elapse (a tick event).  Such scheme is known as digital clock view of DTMC, however, using an integer variable (with the upper- bound) explicitly as a clock variable, we can also represent a system with discrete time in DTMC. In this paper, we use the latter scheme to avoid the state explosion problem.
Network Simulator NS–2
2.2
The Network Simulator (ns) is a network simulator devel- oped by Virtual InterNetwork Testbed (VINT) project. It has been widely used[16]. NS–2 is the successor version of ns. It is open source soft- ware. NS–2 uses two languages: C++ for core libraries; and OTcl (Object-oriented Tcl) for scenario description and net- work configuration. A new protocol which is not pre-defined in the core libraries has to be written by a user.
Protocols for Net-streaming
2.3
Here, we simply summarize typical protocols used in the Internet.  Typical protocols used in the Internet have a con- gestion control mechanism in order to avoid network con- gestion.  For example, TCP (Transmission Control Protocol) uses AIMD (Additive Increase Multiplicative Decrease) type window-flow control as such the mechanism.  It controls the data size of sending packets based on the current available bandwidth.  Such scheme has an advantage for the correct data transmission.  It, however, allows delays, which is not suitable for real-time data transmission.  Therefore, RTSP (Real Time Streaming Protocol) is used for real-time appli- cation. RTSP is a protocol for the Internet streaming of voice and movies, on TCP/IP network. Famous congestion control mechanisms for RTSP are RAP (Rate Adaptation Protocol)[5] and TEAR (TCP Emulate At Receivers)[6]. Recently, TFRC (TCP-Friendly Rate Control)[7] attracts attention. Hence, this paper models TFRC.
2.3.1 RTSP
RTSP is one of typical protocols working at end-to-end. RTSP has five states, called SETUP, PLAY, RECORD, PAUSE and TEARDOWN. RTP (Real-time Transport Protocol) is respon- sible for transmission of stream-data.  It determines the through- put of RTP based on rate control scheme of TFRC using the report message of RTCP (RTP Control Protocol).
2.3.2    TCP Friendly Rate Control TFRC
TFRC is a rate control scheme for fairness between RTP and TCP. It controls the rate in order to avoid bad effects on ex- isting TCP flows in the same network, which increases total effectiveness of the whole network. TFRC controls the rate using the report message of RTCP. The report message con- tains loss of packets and jitters, which can be estimated via the sequence number of received RTP packets and time stamps, respectively.  RFC3448 describes the following formula for determining the throughput: X = R* √ 2*b*p/3 + (t_RTO*(3* √ 3*b*p/8*p*(1+32*p²))) where the unit of X is byte/seconds.  The parameter of the formula is summarized in Table 1. The calculated throughput is a rate with which a RTSP server should send packets considering the network conges- tion at the time. Therefore weighted average values of the pa- rameters in a short period are applied into the equation. Paper [7] also defines the calculation methods for the parameters. When the value of X  is less than the bandwidth, TFRC lets RTSP set the value as throughput.
3
Example Network Configuration and
Protocols
In this section, we introduce an example of a real-time dis- tributed system.  As the example system, we select a video data transmission system[14] shown in Fig.1.  The system is composed of a pair of a video server and its client, three pairs of FTP servers and their clients, and a packet generator, which are connected to each other through routers located at the middle of Fig.1. The routers are connected through the 10Base–T Ethernet, which is considered as a bottleneck of packet transmission.  In the considering scenario, the video server sends 80MB of video data with throughput of 1Mbps using the rate control of TFRC. After 100 seconds from the start of the video streaming, FTP servers and clients start their data transmission through TCP sessions.  Also, the packet generator always sends UDP packets with the throughput of 8Mbps as background noise.
PRISM Model
4
We generate two PRISM models for the example of Fig.1. The first one is modelled in detail, and another one is based on the simulation results on the first model but is more simpli- fied model. First, we apply PRISM simulation to the detailed model to show the correctness of our model and to obtain the data to generate the simplified model. Next, the simpli- fied model is used to verify the qualitative properties of the throughput.

The Detailed Model
4.1
In the detailed model, we have to model packet loss rates and round trip time of the RTP packets as well as the buffer control of the routers, the congestion control of transmission protocols, and a time elapsing mechanism.
4.1.1
Time Elapsing
In order to manage time elapsing in the detailed model, we declare an integer variable to represent time.  Time elapsing is based on events such as packet transmission. In the model, each module registers time of occurrence of the next event, and when all modules register the time, the model perform time elapsing into the latest time of the registered event from the current time. After time elapsing, a corresponding module performs the registered event and registers time of the next event again. The module to manage time elapsing contains two vari- ables and is implemented as ten lines of code.
4.1.2
Buffer Control of the Routers
Buffer control of the routers is modelled as a queue which holds transferring packets.  In the model, the current queue length is managed with an integer variable.  Enqueue and dequeue behaviors are described in the model as operations. Also, regardless of the current queue length, enqueueing pack- ets are dropped with certain probability. In order to construct the module of buffer control, we have to specify maximum length of the queue, a packet transfer rate of the link between the routers, and constant probability to drop enqueueing pack- ets as parameters. In the enqueue operation, if the current queue length be- comes larger than the maximum one, the enqueueing packet is considered to be dropped (drop tail).  The dequeue opera- tion is abstracted; together with the time elapsing operation, a number of packets are output from the queue at a time ac- cording to the packet transfer rate of the link. The buffer control module shown in Fig.2 contains ten vari- ables and is implemented as about 80 lines of code, where the module also manages the history of packet loss intervals used for the congestion control.  In Fig.2, the ten variables are firstly declared. Several actions are defined in CCS like expressions with probabilities. For example, the expression [ENQFTP1] P1]  (q_len <= MAXQLEN - pnum_ftp1)
 = P_LOSS_RATE : (q_len' = q_len + pnum_ftp1); + P_LOSS_RATE : true; stands for that when an action ENQFTP1 occurs and (q_len < MAXQLEN – pnum_ftp1 ) holds, the variables q_len is updated to q_len+ pnum_ftp1 with probability 1 – P_LOSS_ RATE , or do nothing with probability P_LOSS_RATE .
4.1.3
Congestion Control
In the model, TCP and RTP sessions can handle congestion control. The slow-start and congestion avoidance behaviors of TCP are embedded to our TCP model. For each connection of the TCP, we declare two integer variables to manage the slow- start threshold and the window size. For each connection of
LOSS RATE : true MAXOLEN) : MAXQLEN) 20SS RATE [TIMER] andmodule (PACKETPERMSEC -PACKETPERMSEC2) Figure 2: The Module of Router Described with PRISM Lan- guage the TCP, we declare six variables and the behavior is imple- mented as about 30 lines of code. In the transmission of RTP, a packet transmission rate is calculated from the throughput equation defined in [7].  To use the equation, we also have to model a packet loss rate and round trip time of the RTP session (see Sec.4.1.4 and 4.1.5). The module related to RTP contains six variables and is de- scribe with about 40 lines of code. In our model, the packet transmission behaviors of TCP and RTP are abstracted as a number of packets are transmitted simultaneously.
4.1.4
Round Trip Time
In our model, round trip time is obtained using physical delay and delay in the router. The delay in the router is calculated as the time to transmit all packets currently buffered in the router. Therefore, we obtain the delay in the router using cur- rent queue length and a packet transmission rate of the link.
4.1.5
Packet Loss Rate
In the TFRC specification[7], a packet loss rate is calculated using intervals of packet loss. To avoid the loss rate varying rapidly, a history of the packet loss intervals is used to calcu- late it. Our model declares eight integer variables to manage the history. In the calculation of the loss rate, recent intervals in the history are weighted heavily.
4.2
The Simplified Model
The detailed model described in Sec.4.1 is too complicated to verify its qualitative properties using model checking. Here, we create a simplified model based on simulation results on the detailed model to perform model checking.  Using the sim- plified model, we verify the minimum and maximum through- put of the media server. The simplified model is based on the throughput equation defined in [7].  In order to create the simplified model, we have to measure distributions of round trip time and packet loss rates on the detailed model.  From the obtained distri- butions, we create discrete probability distributions of them. The simplified model decides its round trip time and a packet loss rate according to the probability distributions.  Finally, by verifying occurrence probability of the throughput on the simplified model, we can obtain the minimum and maximum throughput. The simplified model is implemented as 50 lines of code.
5
NS–2 Model
We use a simulation scenario shown in Fig.3. Values asso- ciated with each link represent transfer rates or physical delay of the link. TCP and UDP sessions in the scenario are derived from pre-defined protocol set in NS–2. In this example, we have to modify the pre-defined RTP protocol so that it can control network congestion because the pre-defined RTP pro- tocol cannot control it. According to TFRC3448[7], we have modified the behaviors of RTP senders and receivers as fol- lows; the receiver can return appropriate feedback packets to the sender, which include information of a packet loss rate, network delay and so on, and the sender can control a trans- fer rate due to the feedback packets.  In our implementation, we have added about 500 lines of code to eight files (twelve methods) of NS–2 sources.
6
Experiments
We have performed some experiments using our PRISM and NS–2 models described in Sec.4 and 5. The experiments were performed under an environment of Windows Vista 64 bit, Intel Core 2 Duo 2.33GHz, and 2.00GB of M.M. In the experiments, we assume packet transmission param- eters as follows: the packet size is 500 Byte, the number of packets acknowledged by a single TCP acknowledgment is one, and the TCP retransmission timeout value is 4 × RTT second. Also we consider three scenarios with respect to the buffer size of routers. In the scenarios, the buffer sizes are 32, 64, and 128 KB respectively. In the paper, we have performed two experiments.  In the first experiment, we performed one trial run for PRISM and NS–2 simulation, respectively, and compared the simulation results. In the second experiment, we performed about 400 trial runs for PRISM simulation, and created a more simpli- fied PRISM model based on the simulation results.  Using the simplified model, we verify the minimum and maximum throughput of the RTP session. To make the simulation results more reliable, we chose about 400 thousands as the number of trial runs, which is default number trial runs for PRISM simulation.
Comparison of the Simulation Results
6.1
Here, we present the simulation results of the buffer size of 64KB in Fig.4 and 5. Throughput in the graph means the average throughput within one second, and a packet loss rate means a calculated value at the time as defined in [7].  In the scenario of the example, file transmission starts after 100 seconds from the start of RTP session, and this causes the network congestion. Consequently, the throughput of the RTP session goes down and the packet loss rate of it comes up. The simulation results of Fig.4 and Fig.5 show that our PRISM model and NS–2 model behave similarly even if the network congestion occurs. To analyze the correctness of our PRISM model in detail, we compare the average, variance, minimum and maximum of throughput measured by PRISM and NS–2. Table 2 repre- sents the analyzed data. Though the maximum throughput of PRISM and NS–2 are similar in all scenarios, the average and minimum throughput are a little bit different in the scenarios of 32KB and 128KB. We think one of the reasons is that we abstract a packet sending mechanism in the PRISM model, that is, when the packet transmission rate is high, our model transmits a number of packets at a time.  We think this may cause the differences of behaviors between the PRISM model and NS–2 one. However, Table 2 shows that the behaviors of these models seem to be totally similar. For one trial run of the PRISM simulation, it takes about two or three seconds, while it takes about three minutes in the simulation of NS–2.
Verification results for the simplified
6.2
model
Here, we verify minimum and maximum throughput that the media server can provide in the worst case and best case. In the verification, we use a simplified model based on the
simulation results on the detailed PRISM model. The simu- lation results should contain discrete probability distributions of the round trip time and the packet loss rates. To obtain re- liable simulation results, we perform about 400 thousands of trial runs of PRISM simulation, which is default number of the PRISM simulation. When the buffer size is 64KB, the discrete probability dis- tributions of the round trip time and the packet loss rates are shown in Fig.6 and 7, respectively. The verification property to be checked is given as follows; P =?[Throughput < xUThroughput > x] . This property means the probability of Throughput being the value of x , where Throughput is a variable to manage the throughput of the RTP session. The verification is performed with varying x from 0 to 1000. Figure 8 represents occurrence probability of the throughput. The graph represents the probability that the throughput becomes greater than or equals to value of x-axis. In the Fig.8, when the throughput is less than 116Kbps, the probability keeps the value one, and until the through- put becomes 1000Kbps the probability is greater than zero. From the verification result, it is guaranteed that the through- put of the media server is greater than 116Kbps in the worst case. Also, the result shows that the media server can trans- mit packets with the rate of 1000Kbps in the best case.  The simulation results of PRISM and NS–2 do not contradict to this verification result. Although it takes about 10 hours to perform about 400 trial runs for PRISM simulation on the detailed model, in the ver- ification on the simplified model, it takes about 40 seconds.
7
Discussion
In our case study, we have verified throughput of the media server using the detailed model and simplified model.  The detailed model includes behaviors of the buffer control of the router and behaviors of the RTP, TCP and UDP protocols in detail. Although the detailed model is too complicated to ver- ify qualitative properties of the system, we can measure some network properties using the simulation function of PRISM. On the other hand, the simplified model focuses on the veri- fication of the minimum and maximum throughput, which is considered as one of important properties of the real-time sys- tems. The simplified model is based on the throughput equa- tion shown in Sec.2, where the dominant parameters such as a packet loss rate and round trip time are derived from the sim- ulation results on the detailed model. The verification on the simplified model has been performed in a few seconds. From the experiments, we can reconstruct our method as follows.  The method will be useful to verify the minimum and maximum throughput that a RTSP connection can pro- vide in an environment where some TCP and UDP connec- tions exist simultaneously.  In our method, first, we create a detailed model of the system which should have a buffer con- trol mechanism of a router considered to be a bottleneck, as well as network congestion control mechanisms of RTSP and TCP. Next, using the simulation function of PRISM, we mea- sure distributions of round trip time and a packet loss rate on the detailed model, and create discrete probability distribu- tions of them. Based on the probability distributions and the throughput equation shown in Sec.2, we create a simplified model. The simplified model decides its round trip time and packet loss rate according to the probability distributions of them. Finally, the minimum and maximum throughput can be verified on the simplified model by probabilistic model check- ing with PRISM. In our simplified model, we assume that packet loss rates and round trip time are decided independently. In fact, these parameters are not independent, i.e., when network conges- tion occurs, packet loss rates and round trip time tend to in- crease simultaneously. In the future work, we need to create a simplified model which represents their dependency. Though simulation with NS–2 or PRISM can evaluate the system's performance, the simulation results depend on paths evaluated in the simulation. Therefore, from the simulation results, we cannot prove qualitative properties of the system. If we obtain a occurrence probability of throughput from the results of Fig.4, we cannot say it is reliable. In the paper, we created the simplified model and we can verify the qualitative properties of the system using model checking.
8
Conclusion
This paper presents a discrete Markov chain for a real-time distributed system, and evaluate its QoS properties using the simulation function of PRISM. To validate the correctness of our model, we also model it in a model for the well-known network simulator NS–2, and give the comparison of their simulation results.  The comparison shows that the result of PRISM simulation is very similar to that of NS–2. It shows that the proposed method is useful to analyze the network per- formance. We think that such analysis is useful for other kind of network analysis. The future works include automatic derivation of simplified model suitable for model checking analysis. Many abstrac- tion techniques are proposed for model checking. We want to apply such techniques to the process.
Acknowledgments
This research is partially supported by the research grant of the Okawa Foundation, (ref. no.08–09) and Grant-in-Aid for Scientific Research (C)(21500036).  Also, this work is being conducted as a part of Stage Project, the Development of Next Generation IT Infrastructure, supported by Ministry of Edu- cation, Culture, Sports, Science and Technology.  We thank Dr. S. Hiromori for useful advices for NS–2.