BERK-RTOS — a sovereign real-time operating system
An RTOS designed for the defense industry, medical systems and critical IoT. One kernel, six sector personas; a scheduler design model-checked with TLA+ and a deterministic interrupt path.
"One Kernel — Six Personas"
One kernel, shaped by sector-specific certification profiles. Each persona carries the feature set its standard demands.
| Profile | Sector | Certification Target | Features |
|---|---|---|---|
| Defense | Defense Industry | CC EAL5+ → EAL7 | MILS, time-partitioning, MIFC |
| Avionics | Aerospace | DO-178C DAL-A/B | ARINC 653, health monitoring |
| Automotive | Automotive | ISO 26262 ASIL-D | AUTOSAR OS, timing protection |
| Medical | Medical Devices | IEC 62304 Class C | Deterministic, safe state |
| Automation | Industrial | IEC 62443 SL3 | PLC cyclic, fieldbus |
| IoT | Consumer IoT | ETSI / PSA | Tickless, OTA, low-power |
A branch-free timer wheel — measured on the board
A DO-178C DAL-A-targeted deterministic tick function for the timer-wheel component
(DualBufferWheel): no atomics, no conditional branches (0 in the compiler output), no flag write in the interrupt
path. Measured on the component's real source on an STM32F746G-DISCO @ 216 MHz with the DWT cycle counter. The wheel is now
the kernel's primary timer: it is advanced on every tick in the SysTick path (scheduler.on_tick), and delays as well as
semaphore and message timeouts are armed there (desktop criterion tests ZS-1…ZS-7). The SysTick path has been measured end to end on the board (below).
21-cycle tick (on the board)
tick_atomic_free with code in ITCM and data in DTCM: net 21 cycles (~97 ns) in steady state, identical with
0 and 8 timers; 9,999 of 10,000 samples at the same value. Worst observed including the first call: net 30 cycles
(includes the measurement call's first-call share). Caches on and off give the same result. Record: berk-rtos
logs/kart_tick_20261029_123002.log. This is a measured worst case, not a static WCET analysis.
108-cycle context switch (on the board)
The kernel's own PendSV handler in ITCM: from a task's switch request to the first instruction of the target
task, 108 cycles (500.0 ns) between two tasks that carry FPU context and 68 cycles (~0.31 µs) between tasks that do
not use the FPU; identical in both directions, all 10,000 samples in each direction at the same value (both
directions pass through exactly the same measurement code). Between
tasks that use the FPU, s0-s31 and FPSCR are preserved; a PendSV with no pending request does not switch context
(verified on the board). Record: berk-rtos logs/kart_pendsv_20261029_202936.log.
This is a measured value, not a static WCET analysis.
SysTick path end to end (on the board)
Real kernel, real SysTick: in deterministic mode (Cortex-M7 branch target address cache off,
belirlenimci_kip) every tick type gives a single value — normal 192, time slice 309, task wake-up 883,
re-arming a far timer 461; with a single task waking, the worst class (re-arm + wake-up) is 1,058 cycles; entry
latency 37 cycles; caches on and off identical. When k tasks wake on the same tick the cost grows with k (default
mode, k = 1/4/8: 842/1,130/1,514 cycles). End-to-end worst case for a single-wake-up tick:
37 + 1,058 + PendSV 108 = 1,203 cycles (~5.6 µs). In the default mode the values are lower (normal 123, wake-up 816)
but vary with the preceding ticks; every observed value stayed below the deterministic-mode value —
an observation, not a guarantee. Record: berk-rtos logs/kart_systick_20261029_202251.log. This is a measured value,
not a static WCET analysis.
Safety layers
Watchdog, stack guards, the SafetyViolation framework, MILS cache-flush hardening, a syscall layer and priority inheritance.
Verified on hardware
The BerkRTOS kernel ran on the STM32F746G-DISCO with two preemptive BERK tasks; the same BERK program also ran on FreeRTOS, ThreadX and Zephyr. DWT measurements at 216 MHz with standalone bare-metal benchmark programs (2026-01-27): context save/restore sequence 279–301 cycles (SRAM, ~1.3–1.4 µs), interrupt latency 138–141 cycles (~640 ns, 3-cycle jitter); 37 on-board tests across 14 sectors, 37/37. The timer wheel's tick function, the kernel's PendSV context switch and the SysTick path have been measured on the board (see the cards alongside). For the i.MX RT1050 there is only a hardware suitability assessment.