DO-178C — auto-formation Ada / SPARK
Support d'auto-formation d'un développeur C# à Ada / SPARK et à
l'impact de la DO-178C sur la façon de développer. Ce n'est pas un
produit : c'est un cours qu'on peut compiler, exécuter, prouver et mesurer.
Rien n'y est affirmé sans avoir été exécuté.
| |
|---|
| Modules | 13, du SECI au projet intégré |
| Campagnes de test | 106 cas, 222 vérifications, 0 échec |
| Preuve SPARK | 253 obligations déchargées, 1 justifiée |
| Couverture | 100 % instructions, décisions et MC/DC sur le code sous test |
| Traçabilité | 0 défaut, matrice reconstruite par outil |
| Avertissements de compilation | 0, traités en erreurs |
Le dépôt frère
geeooff/DO-178C-training traite la même démarche en
C++17. Les deux dépôts partagent le même cas d'étude — un système de
jaugeage carburant FQMS, DAL B — contre les mêmes exigences de haut
niveau, énoncé pour énoncé.
L'intérêt est là : le processus est la constante, le langage est la
variable. Voir le module 12, qui met les deux
implémentations en regard.
Ce dépôt-ci se lit néanmoins seul : il ne suppose connu ni le C++, ni le
dépôt frère.
Ce que la chaîne Ada permet et que le C++ ne permettait pas
| Dépôt C++ | Ce dépôt |
|---|
| Couverture | lignes et branches (gcovr) | instructions, décisions, MC/DC (gnatcov) |
| Absence d'erreur à l'exécution | argumentée, revue | prouvée (gnatprove, DO-333) |
| Couplage données/contrôle | tableau tenu à la main | Global / Depends, vérifiés par l'outil |
| Interdiction des exceptions | convention de codage | pragma Restrictions, vérifié à l'édition de liens |
| Absence d'allocation | revue | pragma Restrictions, vérifié |
| Qualification d'outil | clang-tidy, qualifié pour rien | kit DO-330 réel pour GNATcoverage |
Démarrer
Le protocole ne se lance pas sur le poste : il se lance dans le SECI.
C'est ce qui rend le résultat reproductible, donc opposable.
docker build -t do178c-ada:verif .devcontainer
docker run --rm -v "$PWD:/workspace" do178c-ada:verif ./scripts/verify.sh
docker run --rm -v "$PWD:/workspace" do178c-ada:verif ./scripts/coverage.sh
VS Code ouvre directement le dépôt dans ce conteneur (Reopen in Container).
verify.sh enchaîne compilation, exécution, preuve SPARK, traçabilité et
formatage. Il accepte une étape isolée : ./scripts/verify.sh prove.
Le parcours
Plan détaillé et parcours abrégés : docs/00-plan-de-formation.md.
Cinq chiffres que ce dépôt a mesurés
Aucun n'est une estimation, et chacun se rejoue d'une commande.
| Chiffre | Ce qu'il dit | Où |
|---|
| 13 % | surcoût en .text des vérifications à l'exécution | module 02 |
| 55 % | MC/DC d'une campagne, sur du code dont 28 obligations sur 28 étaient prouvées | module 05 |
| 33 % | MC/DC atteint par deux cas de test qui donnent 100 % de couverture de décisions | module 10 |
| 4 sur 10 | violations du standard de codage attrapées par le compilateur ; six restent à la revue | module 11 |
| 44 → 35 | instructions du FQMS après correction des écarts : le composant a maigri en gagnant en couverture | module 12 |
Chaîne d'outils
Ce que l'image contient est épinglé dans
.devcontainer/Dockerfile, qui tient lieu de
SECI exécutable (DO-178C §11.15) : l'image de base par son digest, les
paquets système par un instantané daté de l'archive Ubuntu, l'archive d'Alire
par son empreinte, la chaîne Ada par ses versions. Une réserve, dite dans
docs/03-outils.md : l'index communautaire d'Alire est
suivi en tête de branche.
This is the beginning of the README. Read the rest at the original. Read the full README ↗
