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
Complete list of metadatas

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/hal-00904796
Contributor : Stephan Merz <>
Submitted on : Friday, November 15, 2013 - 11:27:37 AM
Last modification on : Tuesday, March 26, 2019 - 2:28:03 PM
Long-term archiving on : Sunday, February 16, 2014 - 4:30:41 AM

File

final.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

723

Files downloads

204