Detail publikace

On formal reachability analysis in networks with dynamic behavior

Originální název

On formal reachability analysis in networks with dynamic behavior

Anglický název

On formal reachability analysis in networks with dynamic behavior

Jazyk

en

Originální abstrakt

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.

Anglický abstrakt

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.

BibTex


@article{BUT91437,
  author="Hidda Marakkala Gayan Ruchika {de Silva} and Ondřej {Ryšavý} and Petr {Matoušek} and Miroslav {Švéda}",
  title="On formal reachability analysis in networks with dynamic behavior",
  annote="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.",
  address="NEUVEDEN",
  chapter="91437",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="2",
  volume="52",
  year="2013",
  month="february",
  pages="919--929",
  publisher="NEUVEDEN",
  type="journal article - other"
}