×

Automatic synthesis of transiently correct network updates via Petri games. (English) Zbl 1489.68157

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 118-137 (2021).
Summary: As software-defined networking (SDN) is growing increasingly common within the networking industry, the lack of accessible and reliable automated methods for updating network configurations becomes more apparent. Any computer network is a complex distributed system and changes to its configuration may result in policy violations during the transient phase when the individual routers update their forwarding tables. We present an approach for automatic synthesis of update sequences that ensures correct network functionality throughout the entire update phase. Our approach is based on a novel translation of the update synthesis problem into a Petri game and it is implemented on top of the open-source model checker TAPAAL. On a large benchmark of synthetic and real-world network topologies, we document the efficiency of our approach and compare its performance with state-of-the-art tool NetSynth. Our experiments show that for several networks with up to thousands of nodes, we are able to outperform NetSynth’s update schedule generation.
For the entire collection see [Zbl 1482.68013].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68M10 Network design and communication in computer systems
68Q60 Specification and verification (program logics, model checking, etc.)
68R10 Graph theory (including graph drawing) in computer science
91A80 Applications of game theory
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Amiri S.A., Dudycz, S., Schmid, S., Wiederrecht, S.: Congestion-free rerouting of flows on DAGs. In: ICALP 2018), volume 107 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 143:1-143:13. Dagstuhl (2018) · Zbl 1499.68242
[2] Benzekki, K., El Fergougui, A., Elbelrhiti Elalaoui, A.: Software-defined networking (SDN): a survey. Secur. Comm. Netw. 9(18), 5803-5833 (2016)
[3] Brandt, S., Förster, K., Wattenhofer, R.: On consistent migration of flows in SDNs. In: INFOCOM 2016, pp. 1-9. IEEE (2016)
[4] Christesen, N., Glavind, M., Schmid, S., Srba, J.: Latte: improving the latency of transiently consistent network update schedules. In: IFIP PERFORMANCE 2020, vol. 48, no. 3 of Performance Evaluation Review, pp. 14-26. ACM (2020)
[5] Cimatti, A.; Brinksma, E.; Larsen, KG, NuSMV 2: an opensource tool for symbolic model checking, Computer Aided Verification, 359-364 (2002), Heidelberg: Springer, Heidelberg · Zbl 1010.68766 · doi:10.1007/3-540-45657-0_29
[6] David, A.; Jacobsen, L.; Jacobsen, M.; Jørgensen, KY; Møller, MH; Srba, J.; Flanagan, C.; König, B., TAPAAL 2.0: integrated development environment for timed-arc petri nets, Tools and Algorithms for the Construction and Analysis of Systems, 492-497 (2012), Heidelberg: Springer, Heidelberg · Zbl 1352.68181 · doi:10.1007/978-3-642-28756-5_36
[7] Didriksen, M., et al.: Artefact for: Automatic Synthesis of Transiently Correct Network Updates via Petri Games (2021). doi:10.5281/zenodo.4497000
[8] Finkbeiner, B.; Gieseking, M.; Hecking-Harbusch, J.; Olderog, E-R; Chen, Y-F; Cheng, C-H; Esparza, J., Model checking data flows in concurrent network updates, Automated Technology for Verification and Analysis, 515-533 (2019), Cham: Springer, Cham · Zbl 1437.68115 · doi:10.1007/978-3-030-31784-3_30
[9] Finkbeiner, B.; Gieseking, M.; Hecking-Harbusch, J.; Olderog, E-R; Lahiri, SK; Wang, C., AdamMC: a model checker for petri nets with transits against flow-LTL, Computer Aided Verification, 64-76 (2020), Cham: Springer, Cham · Zbl 1478.68156 · doi:10.1007/978-3-030-53291-8_5
[10] Foerster, K.; Schmid, S.; Vissicchio, S., Survey of consistent software-defined network updates, IEEE Commun. Surv. Tutorials, 21, 2, 1435-1461 (2019) · doi:10.1109/COMST.2018.2876749
[11] Hopps, C., et al.: Analysis of an equal-cost multi-path algorithm. Technical report, RFC 2992, November 2000
[12] Jensen, JF; Nielsen, T.; Oestergaard, LK; Srba, J., TAPAAL and reachability analysis of P/T nets, Trans. Petri Nets Other Mod. Concurrency (ToPNoC), 9930, 307-318 (2016)
[13] Jensen, PG; Larsen, KG; Srba, J.; Bošnački, D.; Wijs, A., Real-time strategy synthesis for timed-arc petri net games via discretization, Model Checking Software, 129-146 (2016), Cham: Springer, Cham · Zbl 1354.68196 · doi:10.1007/978-3-319-32582-8_9
[14] Jensen, P.G., Larsen, K.G., Srba, J.: Ptrie: data structure for compressing and storing sets via prefix sharing. In: ICTAC 2017, vol. 10580 of LNCS, pp. 248-265. Springer (2017) · Zbl 1444.68063
[15] Jensen, PG; Larsen, KG; Srba, J., Discrete and continuous strategies for timed-arc Petri net games, Int. J. Softw. Tools Technol. Transf., 20, 5, 529-546 (2017) · doi:10.1007/s10009-017-0473-2
[16] Knight, S.; Nguyen, HX; Falkner, N.; Bowden, R.; Roughan, M., The internet topology Zoo, IEEE J. Select. Areas Comm., 29, 9, 1765-1775 (2011) · doi:10.1109/JSAC.2011.111002
[17] Liu, HH; Wu, X.; Zhang, M.; Yuan, L.; Wattenhofer, R.; Maltz, D., Zupdate: updating data center networks with zero loss, SIGCOMM Comput. Commun. Rev., 43, 4, 411-422 (2013) · doi:10.1145/2534169.2486005
[18] Ludwig, A., Dudycz, S., Rost, M., Schmid, S.: Transiently secure network updates. In: ACM SIGMETRICS, pp. 273-284. ACM (2016)
[19] Ludwig, A., Marcinkowski, J., Schmid, S.: Scheduling loop-free network updates: it’s good to relax! In: PODC 2015, pp. 13-22. ACM (2015) · Zbl 1333.68215
[20] Mahajan, R., Wattenhofer, R.: On consistent updates in software defined networks. HotNets-XII, New York, NY, USA. ACM (2013)
[21] McClurg, J.; Hojjat, H.; Černy, P.; Foster, N., Efficient synthesis of network updates, ACM Sigplan Not., 50, 6, 196-207 (2015) · doi:10.1145/2813885.2737980
[22] Moy, J.: RFC2328: OSPF version 2 (1998). https://tools.ietf.org/html/rfc2328
[23] Murata, T., Petri nets: properties, analysis and applications, Proc. IEEE, 77, 4, 541-580 (1989) · doi:10.1109/5.24143
[24] Reitblatt, M., Foster, N., Rexford, J., Schlesinger, C., Walker, D.: Abstractions for network update. In: ACM SIGCOMM 2012, pp. 323-334. ACM (2012)
[25] Vissicchio, S., Cittadini, L.: FLIP the (flow) table: fast lightweight policy-preserving SDN updates. In: INFOCOM 2016, pp. 1-9. IEEE (2016)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.