Formal Verification of Embedded Linux Systems Using Trace-Based Models

Explore a conference talk on formal verification techniques for embedded Linux systems using trace-based models. Learn about a semi-formal, model-based approach to derive reliable statements about run-time characteristics of embedded Linux in safety-critical systems. Discover how to generate finite automaton-based descriptions of safety-relevant aspects, obtain empirical data through system instrumentation, and transform this information into statistical guarantees on system behavior. Gain insights into drawing conclusions for certifying systems in terms of reliability, latencies, and real-time properties. Follow the presentation through topics such as motivation, approach, state machines, model properties, real-time properties, system instrumentation, model visualization, stochastic analysis, and IOQ handling.

Introduction
Motivation
Approach
Single Steps
State Machines
Model Properties
RealTime Properties
Instrumenting System
Execution Path Token
System Instrumentation
Log of Events
Model Visualization
Stochastic Analysis
RealTime Systems Analysis
IOQ Handling
IOQ Measuring
Conclusion
Project