Print Email Facebook Twitter Finite Abstractions of Network Calculus Elements for Formal Verification of Network Bounds Title Finite Abstractions of Network Calculus Elements for Formal Verification of Network Bounds Author Dahlan, B. Contributor Mazo, M. (mentor) Faculty Electrical Engineering, Mathematics and Computer Science Department Delft Center for Systems and Control Programme Embedded Systems Date 2013-09-20 Abstract 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 state-space representation of a min-plus linear (MiPL) system, a finite-state symbolic model or quotient system can be constructed. The construction of such quotient systems is done by first partitioning the state-space according to the MiPL dynamics and certain atomic propositions defined over the states. The transitions between the quotient states are then computed based on the dynamical system. The resulting finite abstraction simulates the infinite-state discrete-time model, which permits applying formal verification to reason about the properties of the discrete-time system. The work is finalized by transforming the backlog and virtual delay properties of the original model to equivalent specifications, given by Linear Temporal Logic (LTL) formulas, on the finite abstraction. Subject Networked Control SystemsNetwork CalculusLeaky BucketsLatency-Rate ServersVirtual DelayBacklogMin-Plus SystemsPiecewise-Affine SystemsSymbolic ModelsFinite AbstractionsFormal MethodsVerificationModel CheckingLinear Temporal Logic To reference this document use: http://resolver.tudelft.nl/uuid:c6a21f0e-8bac-440b-a360-eaf4212c8107 Embargo date 2013-10-07 Part of collection Student theses Document type master thesis Rights (c) 2013 Dahlan, B. Files PDF mscThesis _edited.pdf 1.12 MB Close viewer /islandora/object/uuid:c6a21f0e-8bac-440b-a360-eaf4212c8107/datastream/OBJ/view