PAIS Lab seminar: On the application of timed automata and UPAAL toolset to the verification of Software Defined Networks // U. Popesko

On the application of timed automata and UPAAL toolset to the verification of Software Defined Networks

Software Defined Networks (SDNs) emerge quite recentlyas a new line of development of computer networks.A distinguished feature of SDNs is that a single controller manages allswitching devices by uploading and modifying their flowtables. A SDN maybe viewed as a real-time asynchronous system of communicating processes- controller and switches. It would be shown that networks of real-timeautomata is a suitable formal model to capture adequately the mostessential features of SDNs. To analyze the behaviour of such models onemay use UPPAAL, a well known toolset for verification of real timedistributed systems. In her talk the speaker presents SDN paradigm,gives a brief overview of real-time automata and UPPAAL, shows how tobuild a formal model of SDN and check it by means of UPPALL, and finallydemonstrates the results of some experiments of SDN verification.

Slides: SDN.pptx