On Formal Reachability Analysis in Networks with Dynamic Behavior

On Formal Reachability Analysis in Networks with Dynamic Behavior

Peer-reviewed article not indexed in WoS or Scopus

Recently, several researches have suggested an application of formal methods for identifying configuration errors, unveiling design problems and predicting network behavior. In this paper, we contribute to this research area by defining a method able to efficiently check reachability properties in dynamically routed networks. We define a notion of network state that captures different network conditions. Each network state represents a unique combination of link availability. The naive enumeration of network states leads quickly to intractability even for small networks as the number of possible combinations grows exponentially. Instead, we enumerate all available paths and, for each path, we search for state aggregation, in which this path is active.

Recently, several researches have suggested an application of formal methods for identifying configuration errors, unveiling design problems and predicting network behavior. In this paper, we contribute to this research area by defining a method able to efficiently check reachability properties in dynamically routed networks. We define a notion of network state that captures different network conditions. Each network state represents a unique combination of link availability. The naive enumeration of network states leads quickly to intractability even for small networks as the number of possible combinations grows exponentially. Instead, we enumerate all available paths and, for each path, we search for state aggregation, in which this path is active.

Formal modeling and analysis, Network service reachability, Dynamic routing, Configuration validation

Formal modeling and analysis, Network service reachability, Dynamic routing, Configuration validation

DE SILVA, G.; RYŠAVÝ, O.; MATOUŠEK, P.; ŠVÉDA, M.

2014

01.02.2013

1018-4864

TELECOMMUNICATION SYSTEMS

52

2

Kingdom of the Netherlands

919

929

10

http://link.springer.com/article/10.1007%2Fs11235-011-9585-2

On formal reachability analysis in networks with dynamic behavior