Model-Based Testing for the Zephyr RTOS
summary
Model based tests derive executable checks from a formal specification of Zephyr kernel behavior rather than higher level handwavy examples The project models the semaphore API and scheduler in TLA+ and PlusCal uses TLC to generate counterexample traces and translates those traces into ZTest runnable C tests run with Twister The prototype assumes a single core no interrupts assumption explores about ten properties and sometimes yields dozens of test cases per property and targets automated conformance for continuous certification
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
41mTurning the Ignition on Safety: Zephyr RTOS in Automotive Compliance
27mZephyr and Trusted Execution Environments
32mFuzzing Zephyr Apps - Struggles of Dynamic Analysis on Embedded Applications
27mZephyr and Trusted Execution Environments
35mValidating Freedom From Interference in Automotive Linux
25mRISC-V System-level Certification from Verification Foundations
38mZephyr: Learnings From Working on Safety Certification in the Open
41mPreparing Zephyr for Safety Element out of Context Certification