Attending this event?
December 5-6, 2022
Yokohama, Japan + Virtual
View More Details & Registration
Note: The schedule is subject to change.

The Sched app allows you to build your schedule but is not a substitute for your event registration. You must be registered for Open Source Summit Japan 2022 to participate in the sessions. If you have not registered but would like to join us, please go to the event registration page to purchase a registration.

This schedule is automatically displayed in Japan Standard Time (UTC +9). To see the schedule in your preferred timezone, please select from the drop-down menu to the right, above "Filter by Date."

IMPORTANT NOTE: The timing of sessions and room locations are subject to change.

Back To Schedule
Tuesday, December 6 • 2:50pm - 3:30pm
Formal Verification of Embedded Linux Systems Using Trace-Based Models - Benno Bielmeier & Wolfgang Mauerer, Technical University of Applied Sciences Regensburg

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

Software for safety-critical systems must meet strict functional and temporal requirements. Since it is impossible to exhaustively test the required qualities, formal verification techniques have been devised. However, these approaches are usually only applicable to small systems, and require software architecture and development to consider verification goals from the ground up. Safety-critical systems face an increasing demand for functionality, and need to handle the associated complexity. While the desired functionalities can be satisfied by embedded Linux, established verification techniques fail for code of such magnitude. We show a semi-formal, model-based approach to derive reliable statements about the run-time characteristic of embedded Linux. Using a-priori expert knowledge, we generate a finite automaton-based effective description of safety-relevant aspects. The real-world, system-dependent behaviour of the resulting automata, in particular timing statistics for state transitions, is empirically obtained via system instrumentation. We then show how to turn this into (statistical) guarantees on their behaviour. We show how this allows to draw conclusions that can be used in certifying systems in terms of reliability, latencies, and other real-time properties.

avatar for Wolfgang Mauerer

Wolfgang Mauerer

Professor/Senior Research Scientist, Technical University of Applied Sciences Regensburg
Wolfgang Mauerer is a professor of theoretical computer science at the Technical University Regensburg, and a senior key expert at Siemens Corporate Research, Competence Centre Embedded Linux. He serves on the technical steering committee of the Linux Foundation's Civil Infrastructure... Read More →

Benno Bielmeier

Research Master Student, Technical University of Applied Sciences Regensburg
Benno Bielmeier is a master student of applied research at the Technical University of Applied Sciences Regensburg. In his bachelor's degree, he studied cooperatively with intensive in-company training in the field of industrial development of embedded software for microcontrollers... Read More →

Tuesday December 6, 2022 2:50pm - 3:30pm JST
416 & 417
  Critical Software Summit
Feedback form isn't open yet.