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
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 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

Senior Software Engineer, Red Hat
Daniel Bristot de Oliveira is a Senior Software Maintenance Engineer at Red Hat, working in the support and development of real-time related products. He is also a Ph.D. student in Automation Engineering at UFSC in Brazil, researching about real-time Linu

Wednesday October 30, 2019 16:15 - 16:50
Forum 2