Contact: Hossein Tabatabaee
Background:
Several networks, such as airplanes and cars, require guaranteed delays. For instance, it is necessary to provide delay certifications for Airbus’s networks. Network calculus [1] is a theory providing bounds on such delays. This mathematical theory currently relies on, human-made, pen and paper proofs. However, we can formalize such proofs in Coq [2], an automated proof checker. Then, Coq can give delay certifications for such networks.
By automating the proofreading process, the confidence in mathematical proofs can be increased. We can use Coq to formally define mathematical objects, enunciate theorems, and finally describe proofs of these theorems. A computer is then able to automatically check these proofs.
As a state-of-the-art, authors in [3] have formalized a subset of the theory large enough to handle a complete proof of network calculus bounds on a simple case study.
In this project:
We will understand how to work with Coq. Specifically, how to define theorems and prove them by Coq. We will analyze the work done in [3]. Lastly, we will formally prove scheduler properties such as Static-priority.
Student Profile:
Interested in formal proofs and mathematics (needed).
Interested in networks, communications, or real-time systems (plus).
Referrences:
[1] Network Calculus Wikipedia Page
[3] Formal Verification of Real-time Networks Lucien Rakotomalala, Marc Boyer, Pierre Roux