Formal Verification and Analysis of Time-Sensitive Software-Defined Network Architecture

Safety-critical traffic in Industrial Internet of Things (IIoT) requires real-time communications with high fault tolerance, bounded latency and low jitter. Time-Sensitive Software-Defined Network (TSSDN), which combines the deterministic transmission of Time-Sensitive Networking (TSN) with the centralized management of Software-Defined Networking (SDN), was recently proposed to support the real-time requirement in IIoT. The research on TSSDN has been receiving increasing interests, however, the existing work has limitations including 1) the functional safety of TSSDN cannot be guaranteed; and 2) the effect of the separation of data plane and control plane on the time-sensitivity of TSSDN has not been evaluated. Therefore, in this paper, we employ the timed model checker UPPAAL to formalize the TSSDN architecture. Firstly, we use the build-in checker in UPPAAL to verify deadlock-free property, functional safety property and starvation-free property of our model. Then, the total latency of frames forwarding and scheduling within a single switch is measured based on the model. We focus on the latency overhead of frames requesting processing rules from the controller, which is on average an additioanl 180µs latency in the worst case, but the impact of this delay on the time-sensitivity of TSSDN is tolerable. As far as we know, this is the first paper providing a formal verification and analysis approach for TSSDN architecture, which could benefit for both TSSDN designers as well as the researchers.