Towards Certifying Network Calculus

Etienne Mabille 1 Marc Boyer 2 Loic Féjoz 1 Stephan Merz 3
3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Liste complète des métadonnées

Cited literature [5 references]  Display  Hide  Download
Contributor : Stephan Merz <>
Submitted on : Friday, November 15, 2013 - 11:27:37 AM
Last modification on : Tuesday, March 26, 2019 - 2:28:03 PM
Document(s) archivé(s) le : Sunday, February 16, 2014 - 4:30:41 AM


Files produced by the author(s)




Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz. Towards Certifying Network Calculus. ITP - 4th International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.484-489, ⟨10.1007/978-3-642-39634-2_37⟩. ⟨hal-00904796⟩



Record views


Files downloads