Skip to Main content Skip to Navigation
New interface
Conference papers

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
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Friday, November 15, 2013 - 11:56:20 AM
Last modification on : Saturday, June 25, 2022 - 7:40:26 PM
Long-term archiving on: : Sunday, February 16, 2014 - 4:30:51 AM


Files produced by the author(s)


  • HAL Id : hal-00904817, version 1



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⟩



Record views


Files downloads