Certifying Network Calculus in a Proof Assistant

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

Cited literature [9 references]  Display  Hide  Download

https://hal.inria.fr/hal-00904817
Contributor : Stephan Merz <>
Submitted on : Friday, November 15, 2013 - 11:56:20 AM
Last modification on : Tuesday, March 26, 2019 - 2:28:03 PM
Document(s) archivé(s) le : Sunday, February 16, 2014 - 4:30:51 AM

File

submission.pdf
Files produced by the author(s)

Identifiers

  • 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, Astrium and Technische Universität München, Jul 2013, Munich, Germany. ⟨hal-00904817⟩

Share

Metrics

Record views

407

Files downloads

228