# [e2e] Formal methods for simulation/analysis of network

Amit Prakash prakash at ece.utexas.edu
Mon Aug 11 17:23:24 PDT 2003

```This is a research idea that has been gestating in my mind for some
time but never got defined enough to work on it. I am looking for
inputs from people on this idea.

What I have in my mind is to use formal methods, or just simple
math to write a network simulator/analyzer that can do a more
comprehensive job than NS simulations.

For example, earlier most circuit designers used to rely on
simulations to verify their circuits and left many undetected bugs.
Now increasingly they have been using more of formal verification
tools to get a mathematical proof of the correctness of the design, or
at least do a more comprehensive job at state space exploration by
simulating  a set of states instead of just one. Similarly few runs
of of NS simulation do not tell
much about a particular protocol or routing algorithm under test.

The problem is that even in case of circuits where state variables are
in few thousands of bits, the verification problem  becomes
computationally formidable. In case of networks, we have a lot more
state to take care of, exact analysis may be impossible. Thus we have
to look for tractable approximation models.

There are two questions that I want your help on.

1) what is desired of  a network simulation/analysis tool ?
2) what sort of simplification assumptions can be made to make the
problem tractable ?

As for question one, You could expect to get some of the following
answers from the tool
a) given a topology, fixed routing and dropping policy, congestion
control protocol in use,  and a set of source and a sinks,
what range of loads makes network unstable, or increase loss rate
to, say more than 90%.

b) For what range of values of RED parameters will a certain network
work well (where working well needs to be defined) ?

c) Given a probability distributions of rate of traffic between all pairs
of sources and sinks in a network, what would be the probability
distribution of load on a certain link or a router.

I have thought of different ideas that do not make a coherent picture
as yet but I will try to list them.

1) A simulator could be built that in stead of simulating one instance
of traffic, simulates a range of traffic. Let A=[a_{ij}] be the
matrix such that a_{ij} is arrival rate of packets at input i for
output j.  And we are given that b_{ij} < a_{ij} < c_{ij}, where
b_{ij} and c{ij}s are constants. Then we can compute bounds on the
range of load we can see at the output links of that router using
simple math (assuming tail drop and a suitable arrival process). If
we do this computation throughout the network we can get the range
of loads that can be seen on any link. Then we can have
instantaneous rates, drop rates computed and feedbacks sent to
sources and rates readjusted. This way we simulate a range of loads
rather than one.
2) Have a fluid flow model, where routers are non-linear devices and
use techniques used in analog circuit simulation tools such as
SPICE.
3) Model network as a hybrid automaton. This blows up pretty soon.
4) Many papers have approximate mathematical expressions for the bandwidth
achieved by a TCP flow given a set of users and fixed routes in
a network such as Frank kelly's paper on modeling Internet. I am
wondering if these expressions can be used by a tool to
answer some of the questions that we can never hope a simulation
tool to answer. For example, compute what values of RED parameters
will optimize utility in  a
given network for a given probability distribution on load.

I apologies for lack of clarity in these ideas, but I will be greatful
if you can help me in defining this by your suggestions, pointing to
an existing work, or otherwise.

-regards,

Amit

```

More information about the end2end-interest mailing list