Model-Based Testing for the Zephyr RTOS
summary
Model-based approach creates a formal spec of the Zephyr semaphore API in PlusCal/TLA+ and TLC, produces counterexample traces (about 10 properties explored, one property yielding ~90 traces), and translates traces into ZTest runnable C tests run via Twister. Implementation assumes single-core no-interrupts so scheduling is deterministic; the test-generation script is promised on the GitHub repo but not yet included. This is a small feasibility case, not full-system continuous certification yet.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 1:25UL Solutions and safety-critical domains
- 2:54Zephyr RTOS certification challenges
- 5:23Formal requirement specification
- 7:10Model-based testing overview
- 11:12Semaphore API formal modeling
- 16:06PlusCal and TLA+ modeling
- 18:38Model checking and verification
- 20:51Runnable test case generation
- 25:04Automated conformance testing benefits
- 27:09Future work and challenges
- 30:24Q&A
- 30:44Validating model requirements
- 32:08Model bias from implementation
- 33:56Existing tests and coverage
- 38:17Case study properties and counterexamples
- 40:04Safety properties and scalability
- 43:20Alternative modeling languages
related talks
46mZephyr Application Development Using TDD: Getting Started
46mZephyr Application Development Using TDD: Getting Started
44mTest Strategy for Zephyr
57mZephyr RTOS Debugging and Performance Analysis
37mStreamlining Testing with Generic Tests and Emulators
32mUsing Customerized QEMU Co-simulation for Development and Test of Zephyr Applications
32mBoF: Quality and Testing Processes for Zephyr + Discussion
18mKeynote: From Zephyr’s Structured Data to Traceable and Testable Open Hardware