[e2e] Formal methods for simulation/analysis of network

[Craig Partridge]

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 
>