TY - GEN
T1 - AllSynth: Transiently Correct Network Update Synthesis Accounting for Operator Preferences
AU - Larsen, Kim Guldstrand
AU - Mariegaard, Anders
AU - Schmid, Stefan
AU - Srba, Jiri
PY - 2022
Y1 - 2022
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 in the LTL logic), also during the reconfiguration process. In particular, in contrast to existing approaches, AllSynth symbolically computes and compactly represents all feasible solutions. At its heart, AllSynth relies on a novel, two-level and parameterized use of 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 often 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 in the LTL logic), also during the reconfiguration process. In particular, in contrast to existing approaches, AllSynth symbolically computes and compactly represents all feasible solutions. At its heart, AllSynth relies on a novel, two-level and parameterized use of 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 often also in terms of runtime as documented by experiments on a benchmark of real-world network topologies.
UR - http://www.scopus.com/inward/record.url?scp=85135018352&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-10363-6_23
DO - 10.1007/978-3-031-10363-6_23
M3 - Article in proceeding
SN - 9783031103629
T3 - Lecture Notes in Computer Science
SP - 344
EP - 362
BT - Theoretical Aspects of Software Engineering - 16th International Symposium, TASE 2022, Proceedings
A2 - Aït-Ameur, Yamine
A2 - Crăciun, Florin
PB - Springer
ER -