Formal Verification Made Easy (and fast!)

Modeling parts of Linux has become a recurring topic. For instance, the memory model, the model for PREEMPT_RT synchronization, and so on. But the term formal model causes panic for most of the deve …

Modeling parts of Linux has become a recurring topic. For instance, the memory model, the model for PREEMPT_RT synchronization, and so on. But the term “formal model” causes panic for most of the developers. Mainly because of the complex notations and reasoning that involves formal languages. It seems to be a very theoretical thing, far from our day-by-day reality.Believe me. Modeling can be more practical than you might guess!This talk will discuss the challenges and benefits of the modeling and verification of the Linux kernel, based on the experience of developing the PREEMPT_RT model. It will present a methodology based on Finite-State Machines, using terms that are very known by kernel developers: tracing events! With the particular focus on how to use models for the formal verification, at runtime, with low overhead, and in many cases, without even modifying Linux kernel!