Towards Certifying Network Calculus

Etienne Mabille, Marc Boyer, Loïc Fejoz, and Stephan Merz

Abstract

Network Calculus (NC) is an established theory for determining bounds on message delays and for dimensioning buffers in the design of networks for embedded systems. It is supported by academic and industrial tool sets and has been widely used, including for the design and certification of the Airbus A380 AFDX backbone. However, while the theory of NC is generally well understood, results produced by existing tools have to be trusted. We report here on work towards using the interactive proof assistant Isabelle/HOL for certifying the results of NC computations. In a nutshell, the NC tool outputs a trace of the calculations it performs, as well as their results. The validity of the trace is then established offline by a trusted checker.

© Springer 2013

Available as: PDF

Reference

@InProceedings{mabille:nc-itp2013,
  author    = {Etienne Mabille and Marc Boyer and Lo\"{\i}c Fejoz and Stephan Merz},
  title     = {Towards Certifying Network Calculus},
  booktitle = {4th Intl. Conf. Interactive Theorem Proving (ITP 2013)},
  year      = {2013},
  pages     = {484-489},
  editor    = {Sandrine Blazy and Christine Paulin-Mohring and David Pichardie},
  series    = {LNCS},
  volume    = {7998},
  publisher = {Springer},
}