NCCoq is a formalization of the network calculus

Related publication:

• Formal Verification of Real-time Networks

Dependencies

Coq (tested with version 8.20.1) MathComp (tested with version 2.3.0) MathComp Analysis (tested with version 1.8.0) Hierarchy Builder (tested with version 1.8.0) MathComp Dioid (tested with master branch)

Most dependencies can be installed using OPAM (version >= 2) by just typing

% opam repo add coq-released https://coq.inria.fr/opam/released
% opam update
% opam install coq.8.20.1 coq-mathcomp-algebra.2.3.0 coq-mathcomp-analysis.1.8.0

See https://github.com/math-comp/dioid for instructions to compile MathComp Dioid.

Compilation

When above dependencies are installed, just type

% make

to compile everything and

% make install

to install if needed.

Subdirectories

• examples: a simple case study

Documentation

% make doc

will generate a documentation, then open html/toc.html with any browser.