11–13 Dec 2025
Asia/Tokyo timezone

RV and the deadline scheduler: how to verify your subsystem at runtime

11 Dec 2025, 15:00
45m
Hall A1 (330) (Toranomon Hills Mori Tower)

Hall A1 (330)

Toranomon Hills Mori Tower

LPC Refereed Track LPC Refereed Track

Speakers

Gabriele Monaco (Red Hat Inc.) Juri Lelli (Red Hat)

Description

Runtime Verification (RV) was introduced in v6.0 of the Linux Kernel and
regained some traction recently with the integration upstream of the scheduler
and rtapp models.

RV was successfully employed to model and validate a subsystem like the
scheduler. With the ongoing work on timed automata, RV monitors get the ability
to verify timing requirements of a subsystem, let's use it to validate the
deadline scheduler.

Join us in this interactive session where we are going to dig into the
experience of supporting a new subsystem in RV from the peculiarities that only
a subsystem maintainer can unveil to new capabilities and paradigms from an RV
maintainer.

This work can highlight inconsistencies in the subsystem, improve its general
understanding and documentation as well as make the RV infrastructure more
robust.

Primary authors

Gabriele Monaco (Red Hat Inc.) Juri Lelli (Red Hat)

Presentation materials

There are no materials yet.