Finite Abstractions of Network Calculus Elements for Formal Verification of Network Bounds

This thesis presents a method to semi-automate the reasoning about network bounds, namely the backlog and delay. Network Calculus offers a rich theory for modeling network elements. Using the modeling techniques of network calculus, network elements are represented by discrete-time systems whose dynamics are linear in min-plus algebra. From the...