DO-178C DAL Levels¶

DO-178C defines five Development Assurance Levels (DAL A–E) corresponding to the severity of failure conditions. adacovex assesses compliance against all five levels.

Level Definitions¶

DAL	Severity	Failure Condition	Example
A	Catastrophic	Prevents continued safe flight/landing	Flight controls, engine FADEC
B	Hazardous	Large reduction in safety margins	Autopilot, navigation
C	Major	Significant increase in crew workload	Flight management system
D	Minor	Slight increase in crew workload	Cabin pressure display
E	No effect	No impact on safety	In-flight entertainment

Assessment Criteria¶

adacovex evaluates four criteria for each DAL level:

1. HLR Traceability¶

DAL	Requirement
A–C	All high-level requirements (HLRs) traced to source code tags (`-- HLR-XXXX`)
D–E	Recommended but not enforced

2. Orphan Tags¶

DAL	Requirement
A–C	Every in-source HLR tag must correspond to a defined HLR in `compliance/HLR.md`
D–E	Recommended but not enforced

3. Test Pass/Fail¶

DAL	Requirement
A–B	100% tests passing with MC/DC coverage (structural coverage analysis)
C	100% tests passing (statement coverage)
D	100% tests passing
E	No requirement

4. Minimum SPARK Level¶

DAL	Minimum SPARK Level	Requirement
A	Gold	Core invariants proved, AoRTE achieved
B	Silver	Partial proofs, all VCs attempted
C	Bronze	Flow analysis passes
D	Stone	Valid SPARK subset
E	None	–

The minimum levels match Min_SPARK_For in src/compliance/adacovex-compliance-dal.adb. Gold is the minimum compliance baseline; Platinum (every functional contract proved) is a best-effort ideal reported when achieved, not a compliance gate. Justified VCs (GNATprove pragma Annotate) count neither as proved nor unproved and never downgrade the level.

DAL-C (default)¶

The default assessment level is DAL-C. To assess at a different level:

adacovex --target=../Ada_CRDT --dal=A
adacovex --target=../Ada_CRDT --dal=B
adacovex --target=../Ada_CRDT --dal=D
adacovex --target=../Ada_CRDT --dal=E

Assessment Output¶

The tool reports each criterion as met/unmet and provides a final Achieved/Unmet status:

Target DAL: C
Status: Achieved
HLR traced:  24 /  24
Orphan tags: No
Tests passing: Yes
Min SPARK level met: Yes