A CCSDS protocol suite for Ada 2022, built with SPARK formal verification.
All protocol encoders and decoders are 100% SPARK-proved at Level 2 -- mathematically guaranteed free of runtime errors (no buffer overflows, no range violations, no integer overflows, no uninitialized reads).
| Standard | Package | Scope |
|---|---|---|
| CCSDS 133.0-B-1 | CCSDS.Space_Packets |
Full primary header encode/decode/validate, full packet encode/decode |
| CCSDS 301.0-B-4 | CCSDS.Time_Codes |
CUC (unsegmented) and CDS (day segmented) encode/decode with P-field |
| CCSDS 732.0-B-4 | CCSDS.AOS_Frames |
AOS Transfer Frame primary header encode/decode/extract, plus FECF CRC |
| CCSDS 133.1-B-3 | CCSDS.Encap_Packets |
Encapsulation Packet header encode/decode |
| CCSDS 727.0-B-5 | CCSDS.CFDP |
CFDP PDU header with variable-length entity IDs / seq nums, plus optional CRC trailer |
| CCSDS 132.0-B-3 | CCSDS.SLE |
Service types, delivery modes, bind states, diagnostics (types only) |
| CRC-16-CCITT-FALSE | CCSDS.CRC16 |
Shared CRC primitive for AOS FECF, CFDP PDU CRC, and any wire checksum using the CCSDS polynomial (0x1021 / seed 0xFFFF) |
- Formally verified -- 440 proof obligations, 0 unproved (CVC5/Z3)
- Standards compliant -- reserved field values rejected, field-width overflow prevented by contract
- No heap allocation -- stack-only, suitable for embedded and safety-critical systems
- Stateless --
pragma Pure, no global state, no side effects - No exceptions -- all errors reported via status enums in result records
- Zero dependencies -- only the Ada standard library
alr with ccsds_adaOr add to your alire.toml:
[[depends-on]]
ccsds_ada = "~0.1.0"with CCSDS;
with CCSDS.Space_Packets;
procedure Example is
package SP renames CCSDS.Space_Packets;
Header : constant CCSDS.Space_Packet_Header :=
(Version => CCSDS.Current_Version,
Packet_Type => CCSDS.Telemetry,
Sec_Header => CCSDS.Absent,
App_Id => 42,
Seq_Flags => CCSDS.Standalone,
Seq_Count => 1,
Data_Length => 3); -- N-1 encoding: 4 bytes of payload
Payload : constant CCSDS.Byte_Array (0 .. 3) :=
[16#DE#, 16#AD#, 16#BE#, 16#EF#];
Packet : constant CCSDS.Byte_Array :=
SP.Encode_Packet (Header, Payload);
begin
-- Packet is now a 10-byte CCSDS Space Packet
null;
end Example;with CCSDS;
with CCSDS.Space_Packets;
procedure Example is
package SP renames CCSDS.Space_Packets;
Data : constant CCSDS.Byte_Array := ...; -- raw bytes
R : constant CCSDS.Packet_Decode_Result := SP.Decode_Packet (Data);
begin
if R.Status = CCSDS.OK then
-- R.Header contains the decoded primary header
-- R.Data_First .. R.Data_Last bounds the data field in Data
null;
end if;
end Example;with CCSDS.Time_Codes;
procedure Example is
package TC renames CCSDS.Time_Codes;
-- Encode a CUC timestamp (4-byte coarse, 2-byte fine)
T : constant TC.CUC_Time :=
(Preamble => (Coarse_Len => 4, Fine_Len => 2),
Coarse => 1_000_000,
Fine => 32768);
Encoded : constant CCSDS.Byte_Array := TC.Encode_CUC (T);
R : constant TC.CUC_Decode_Result := TC.Decode_CUC (Encoded);
begin
pragma Assert (R.Status = TC.OK);
pragma Assert (R.Time.Coarse = 1_000_000);
end Example;with CCSDS;
with CCSDS.AOS_Frames;
with CCSDS.CRC16;
procedure Example is
package AOS renames CCSDS.AOS_Frames;
package CRC renames CCSDS.CRC16;
Body_Bytes : constant CCSDS.Byte_Array := ...; -- header + data
Frame : CCSDS.Byte_Array (0 .. Body_Bytes'Length + 1) :=
[others => 0];
begin
Frame (0 .. Body_Bytes'Length - 1) := Body_Bytes;
CRC.Write_BE
(AOS.Compute_FECF (Body_Bytes),
Frame (Body_Bytes'Length),
Frame (Body_Bytes'Length + 1));
pragma Assert (AOS.Verify_FECF (Frame));
end Example;CCSDS.CRC16 is the shared CRC-16-CCITT-FALSE primitive (polynomial
0x1021, seed 0xFFFF, no reflection, no final XOR). Its canonical
check value is 0x29B1 for the ASCII string "123456789", which is
exercised in the test suite.
Each package has its own decode status enum and result record. No exceptions are raised -- callers check the .Status field:
type Decode_Status is (OK, Err_Truncated, Err_Invalid_Version, ...);
type Header_Decode_Result is record
Status : Decode_Status;
Header : Space_Packet_Header;
end record;All 440 verification conditions discharged cleanly at SPARK Level 2.
No pragma Assume, no justified checks, no warnings.
# Requires gnatprove >= 15.1
gnatprove -P ccsds_ada.gpr -j0 --level=2 --timeout=30 \
-u ccsds-space_packets.adb \
-u ccsds-time_codes.adb \
-u ccsds-aos_frames.adb \
-u ccsds-encap_packets.adb \
-u ccsds-cfdp.adb \
-u ccsds-crc16.adbalr build # build the library
alr exec -- gprbuild -P test_ccsds.gpr -p # build tests
bin/test_space_packets # 76 tests
bin/test_time_codes # 74 tests
bin/test_stretch # 91 tests (AOS, Encap, CFDP, SLE)
bin/test_crc16 # 19 tests (CRC-16 + AOS FECF + CFDP CRC)On macOS, add -XCCSDS_OS=macos when building the test project so the
linker picks up the SDK search path.
Runnable walk-throughs live under examples/:
| Example | Demonstrates |
|---|---|
space_packet_roundtrip.adb |
Build and parse a CCSDS 133.0-B-1 Space Packet |
cuc_time_roundtrip.adb |
CUC time code with and without an explicit P-field |
aos_fecf.adb |
AOS Transfer Frame with a computed FECF trailer and bit-flip detection |
cfdp_pdu_with_crc.adb |
CFDP PDU header with the optional 2-byte CRC trailer |
Build and run (same macOS caveat applies):
alr exec -- gprbuild -P examples.gpr -p # add -XCCSDS_OS=macos on macOS
bin/space_packet_roundtrip
bin/cuc_time_roundtrip
bin/aos_fecf
bin/cfdp_pdu_with_crc- GNAT >= 15.1 with Ada 2022 support
- gnatprove >= 15.1 (for running SPARK proofs only -- not a library dependency)
- Alire >= 2.0 (package manager)
Apache-2.0 -- see LICENSE.