October 31 - November 1 - Co-Located Events
October 28-30 - Conference
Lyon Convention Centre - Lyon, France
More information for Open Source Summit + Embedded Linux Conference Europe 2019
Back To Schedule
Wednesday, October 30 • 16:15 - 16:50
Formal Verification Made Easy (and fast!) - Daniel Bristot de Oliveira, Red Hat

Sign up or log in to save this to your schedule, view media, leave feedback and see who's attending!

Feedback form is now closed.
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!

avatar for Daniel Oliveira

Daniel Oliveira

Principal Software Engineer, Red Hat
Daniel is a Principal Software Engineer at Red Hat, working in the real-time kernel team, and has a Ph.D. in Automation Engineering (UFSC)/Computer Engineering (Scuola Superiore Sant'Anna). He works in the research and development of real-time features and runtime formal verification... Read More →

elce 2 pdf

Wednesday October 30, 2019 16:15 - 16:50 CET
Forum 2
  Embedded Linux Conference, Verification
  • Session Slides Included Yes