TY - JOUR
T1 - AllSynth: A BDD-Based Approach for Network Update Synthesis
AU - Larsen, Kim Guldstrand
AU - Mariegaard, Anders
AU - Schmid, Stefan
AU - Srba, Jiri
PY - 2023/8
Y1 - 2023/8
N2 - 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.
AB - 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.
KW - Binary decision diagrams
KW - Computer networks
KW - Software defined networking
KW - Update synthesis
UR - http://www.scopus.com/inward/record.url?scp=85164249420&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2023.102992
DO - 10.1016/j.scico.2023.102992
M3 - Journal article
SN - 0167-6423
VL - 230
JO - Science of Computer Programming
JF - Science of Computer Programming
M1 - 102992
ER -