Publication Details

On Formal Reachability Analysis in Networks with Dynamic Behavior

DE Silva Gayan, RYŠAVÝ Ondřej, MATOUŠEK Petr and ŠVÉDA Miroslav. On formal reachability analysis in networks with dynamic behavior. Telecommunication Systems, vol. 52, no. 2, 2013, pp. 919-929. ISSN 1018-4864. Available from: http://link.springer.com/article/10.1007%2Fs11235-011-9585-2
Czech title
Formální analýza dosažitelnosti služeb v počítačových sítích
Type
journal article
Language
english
Authors
De Silva Gayan (FIT BUT)
Ryšavý Ondřej, doc. Ing., Ph.D. (DIFS FIT BUT)
Matoušek Petr, doc. Ing., Ph.D., M.A. (DIFS FIT BUT)
Švéda Miroslav, prof. Ing., CSc. (DIFS FIT BUT)
URL
Keywords

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

Abstract

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.

Published
2013
Pages
919-929
Journal
Telecommunication Systems, vol. 52, no. 2, ISSN 1018-4864
Publisher
Springer US
BibTeX
@ARTICLE{FITPUB9578,
   author = "Gayan Silva De and Ond\v{r}ej Ry\v{s}av\'{y} and Petr Matou\v{s}ek and Miroslav \v{S}v\'{e}da",
   title = "On Formal Reachability Analysis in Networks with Dynamic Behavior",
   pages = "919--929",
   journal = "Telecommunication Systems",
   volume = 52,
   number = 2,
   year = 2013,
   ISSN = "1018-4864",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/9578"
}
Back to top