[e2e] Formal methods for simulation/analysis of network

[Debojyoti Dutta]

Another related page is the STRESS project page at USC. 

http://netweb.usc.edu/stress/

Regards
Debo


On Tue, 12 Aug 2003, Craig Partridge wrote:

> Date: Tue, 12 Aug 2003 11:29:23 -0400
> From: Craig Partridge <craig at aland.bbn.com>
> To: Amit Prakash <prakash at ece.utexas.edu>
> Cc: end2end-interest at postel.org
> Subject: Re: [e2e] Formal methods for simulation/analysis of network 
> 
> 
> Have you seen Holzmann's work on SPIN (and nice book on protocol verification
> c. 1989).
> 
> Craig
> 
> In message <Pine.LNX.4.21.0308111921120.29776-100000 at linux01.ece.utexas.edu>, A
> mit Prakash writes:
> 
> >
> >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 
> >
>