Loading…
Attending this event?
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!

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!

Speakers
avatar for Daniel Bristot de Oliveira

Daniel Bristot de Oliveira

Senior Software Engineer, Red Hat
Daniel is a kernel engineer at Red Hat, working in the real-time kernel team. He is also a researcher in the Retis Lab at the Scuola Superiore Sant'Anna (Pisa - Italy). He works in the research and development of new real-time features and runtime formal verification methods for the... Read More →


Wednesday October 30, 2019 16:15 - 16:50
Forum 2
Feedback form isn't open yet.