Towards Certifying Network Calculus

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.
Type de document :
Communication dans un congrès
Sandrine Blazy and Christine Paulin-Mohring and David Pichardie. ITP - 4th International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.484-489, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39634-2_37〉
Liste complète des métadonnées

Littérature citée [5 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00904796
Contributeur : Stephan Merz <>
Soumis le : vendredi 15 novembre 2013 - 11:27:37
Dernière modification le : mercredi 28 mars 2018 - 14:16:10
Document(s) archivé(s) le : dimanche 16 février 2014 - 04:30:41

Fichier

final.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz. Towards Certifying Network Calculus. Sandrine Blazy and Christine Paulin-Mohring and David Pichardie. ITP - 4th International Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.484-489, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-39634-2_37〉. 〈hal-00904796〉

Partager

Métriques

Consultations de la notice

442

Téléchargements de fichiers

118