AllSynth: A BDD-based approach for network update synthesis

The increasingly stringent dependability requirements on communication networks as well as the need to render these networks more adaptive to improve performance, demand for more automated approaches to operate networks. We present AllSynth, a symbolic synthesis tool for updating communication netwo...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2023-08, Vol.230, p.102992, Article 102992
Main Authors: Larsen, Kim G., Mariegaard, Anders, Schmid, Stefan, Srba, Jiří
Format: Article
Language:English
Subjects:
Binary decision diagrams
Computer networks
Software defined networking
Update synthesis
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The increasingly stringent dependability requirements on communication networks as well as the need to render these networks more adaptive to improve performance, demand for more automated approaches to operate networks. We present AllSynth, a symbolic synthesis tool for updating communication networks in a provably correct and efficient manner. AllSynth automatically synthesizes network update schedules which transiently ensure a wide range of policy properties expressed using linear temporal logic (LTL). In particular, in contrast to existing approaches, AllSynth symbolically computes and compactly represents all feasible and cost-optimal solutions. At its heart, AllSynth relies on a novel parameterized use of binary decision diagrams (BDDs) which greatly improves performance. Indeed, AllSynth not only provides formal correctness guarantees and outperforms existing state-of-the-art tools in terms of generality, but also in terms of runtime as documented by experiments on a benchmark of real-world network topologies.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2023.102992