3rd International ICST Conference on Simulation Tools and Techniques

Research Article

Combination of simulation and formal methods to analyse network survivability

Download479 downloads
  • @INPROCEEDINGS{10.4108/ICST.SIMUTOOLS2010.8654,
        author={Petr  Matousek and Ondrej  Rysavy and Gayan  de Silva and Martin  Danko},
        title={Combination of simulation and formal methods to analyse network survivability},
        proceedings={3rd International ICST Conference on Simulation Tools and Techniques},
        publisher={ICST},
        proceedings_a={SIMUTOOLS},
        year={2010},
        month={5},
        keywords={formal analysis dynamic networks simulation reliability},
        doi={10.4108/ICST.SIMUTOOLS2010.8654}
    }
    
  • Petr Matousek
    Ondrej Rysavy
    Gayan de Silva
    Martin Danko
    Year: 2010
    Combination of simulation and formal methods to analyse network survivability
    SIMUTOOLS
    ICST
    DOI: 10.4108/ICST.SIMUTOOLS2010.8654
Petr Matousek1,*, Ondrej Rysavy1,*, Gayan de Silva1,*, Martin Danko1,*
  • 1: Brno University of Technology, Bozetechova 2, 612 66 Brno, Czech republic.
*Contact email: matousp@fit.vutbr.cz, rysavy@fit.vutbr.cz, xdesil00@stud.fit.vutbr.cz, xdank00@stud.fit.vutbr.cz

Abstract

Modern computer networks are complex and their topology can dynamically change when links go down. It is difficult to predict behaviour of a large network with dynamic routing protocols. To automatically prove survivability and reliabil- ity of an end-to-end connection, formal analysis combined with simulation can be exploited. In this paper, an approach based on detection of critical elements using formal analy- sis and subsequent simulation of time related properties is introduced. Our network model is automatically extracted from configurations of network devices. Then, critical net- work elements are detected using graph search algorithms. Then, several simulation scenarios are executed over a model in order to detect time dependencies. Modelling and sim- ulation is done in OMNeT++ simulator, formal analysis is computed using scripting. The first results of this combined analysis show feasibility of this approach and help to reveal both qualitative parameters (status of links and nodes), and quantitative parameters (timers, routing protocols) that in- fluence reliability and survivability of the network. The ap- proach is demonstrated on a simplified topology of Czech Academic Network (CESNET).