[e2e] Formal methods for simulation/analysis of network

[Amit Prakash]

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