Certifying Network Calculus in a Proof Assistant

Abstract : Ensuring correct behaviour of a distributed real-time function requires bounds on the network traversal time. The network calculus is a theory designed to compute such bounds, used to certify the A380 AFDX backbone. In the PEGASE project, some enhancements have been done to the theory, and a software implementation has been developed. To ensure correctness of the software, instead of a process based on tests and code coverage, the "proof by instance" approach is used. The tool generates a proof of correctness of the result, that can be checked by a proof assistant.
Type de document :
Communication dans un congrès
EUCASS - 5th European Conference for Aeronautics and Space Sciences, Jul 2013, Munich, Germany. 2013
Liste complète des métadonnées

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

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

Fichier

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

Identifiants

  • HAL Id : hal-00904817, version 1

Collections

Citation

Etienne Mabille, Marc Boyer, Loic Féjoz, Stephan Merz. Certifying Network Calculus in a Proof Assistant. EUCASS - 5th European Conference for Aeronautics and Space Sciences, Jul 2013, Munich, Germany. 2013. 〈hal-00904817〉

Partager

Métriques

Consultations de la notice

275

Téléchargements de fichiers

212