Formal Verification of Embedded Linux Systems Using Trace-Base...
summary
Proposes a semi‑formal pipeline that models safety‑relevant behavior as deterministic finite automata, instruments Linux (using tracepoints, ftrace, kprobes, uprobes, LTTng, eBPF) to record transition timestamps, and turns collected latencies into histograms, KDEs and statistical worst‑case bounds. Demonstrates a six‑state synthetic model and an IO queue interrupt handling case, runs 100–200 runs to show distributions converge and worst‑case shifts right, and reports that the approach yields usable, explainable timing guarantees for mid‑assurance certification.
AI-written summary · about
chapters (18)
- 0:00Introduction
- 5:40Motivation
- 8:15Approach
- 11:10Single Steps
- 11:30State Machines
- 11:45Model Properties
- 13:50RealTime Properties
- 17:55Instrumenting System
- 18:30Execution Path Token
- 22:30System Instrumentation
- 23:10Log of Events
- 23:35Model Visualization
- 25:20Stochastic Analysis
- 25:50RealTime Systems Analysis
- 27:50IOQ Handling
- 29:00IOQ Measuring
- 31:00Conclusion
- 32:00Project
related talks
46mTools and Techniques to Debug an Embedded Linux System
38mDebugging Embedded Linux
43mTools and Techniques to Debug an Embedded Linux System
39mHow to Investigate Issues on Linux Embedded System?
26mTuning Real-Time Linux for ARM SoCs
33mUsing Open Source Software to Build an Industrial-grade Embedded Linux Platform...
02h 00mAdvanced Debug and Trace Tools for RISC-V Architectures
59mGetting Started with Embedded Linux Security