AllSynth: Transiently Correct Network Update Synthesis Accounting for Operator Preferences
Theoretical Aspects of Software Engineering(2022)
摘要
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.
更多查看译文
关键词
network,synthesis
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要