Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a Model-Based Testing (MBT) approach for the Zephyr Real-Time Operating System in this 44-minute conference talk from the Linux Foundation. Learn how to address the significant challenges of certifying Zephyr for safety-critical domains, where the absence of centralized requirement specifications makes validation and verification particularly difficult. Discover how formal modeling can solve the problem of manual test creation by automatically generating runnable test cases that verify software implementation alignment with system models. Examine a practical implementation of MBT applied to Zephyr's semaphore API using TLA+ formal specification language to generate executable ZTest test cases. Understand how integrating Model-Based Testing into Zephyr's development cycle can produce formal system specifications, enable automated conformance testing, and facilitate continuous certification processes. Gain insights into how this approach can benefit open-source projects where feature development typically lacks centralized requirement specifications, making traditional verification and validation methods more challenging to implement effectively.
