English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

We present a model checking approach for the verification of data flowcorrectness in networks during concurrent updates of the network configuration.This verification problem is of great importance for software-definednetworking (SDN), where errors can lead to packet loss, black holes, andsecurity violations. Our approach is based on a specification of temporalproperties of individual data flows, such as the requirement that the flow isfree of cycles. We check whether these properties are simultaneously satisfiedfor all active data flows while the network configuration is updated. Torepresent the behavior of the concurrent network controllers and the resultingevolutions of the configurations, we introduce an extension of Petri nets witha transit relation, which characterizes the data flow caused by each transitionof the Petri net. For safe Petri nets with transits, we reduce the verificationof temporal flow properties to a circuit model checking problem that can besolved with effective verification techniques like IC3, interpolation, andbounded model checking. We report on encouraging experiments with a prototypeimplementation based on the hardware model checker ABC.

Model Checking Data Flows in Concurrent Network Updates (Full Version)