Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Research highlights
Research results
Research highlight : PROVING FAIRNESS AND IMPLEMENTATION CORRECTNESS OF A MICROKERNEL SCHEDULER
PROVING FAIRNESS AND IMPLEMENTATION CORRECTNESS OF A MICROKERNEL SCHEDULER
5 May 2009

Matthias Daum , Jan Dörrenbächer and Burkhart Wolff.Journal of Automated Reasoning (JAR), 2009.
We report on the formal proof of a microkernel’s key property, namely that its multi-priority process scheduler guarantees progress, i.e., strong fairness. The proof architecture links a layer of behavioral reasoning over system-trace sets with a concrete, fairly realistic implementation written in C. Our microkernel provides an infrastructure for memory virtualization, for communication with hardware devices, for processes (represented as a sequence of assembly instructions, which are executed concurrently over an underlying, formally defined processor), and for inter-process communication (IPC) via synchronous message passing. The kernel establishes process switches according to IPCs and timer-events; the scheduling of process switches, however, follows a hierarchy of priorities, favoring, e.g., system processes over application processes over maintenance processes. Besides the quite substantial models developed in Isabelle/HOL and the formal clarification of their relationship, we provide a detailed analysis what formal requirements a microkernel imposes on the key ingredients (hardware, timers, machine-dependent code) in order to establish the correct operation of the overall system. On the methodological side, we show how early modeling with foresight to the later verification has substantially helped our project.

In: Journal of Automated Reasoning (JAR), DOI: 10.1007/s10817-009-9119-8, published electronically, print version to appear. Springer, 2009.

Keyword
  [none]

Group
  ° Formal Testing and System Exploration

Contact
  ° WOLFF Burkhart
Research highlights
MODEL TRANSFORMATION AS CONSERVATIVE THEORY-TRANSFORMATION
30 October 2020
We present a new technique to construct tool support for domain-specific languages (DSLs) inside the

BEST STUDENT PAPER AWARD (ML) AT ECML 2019
20 September 2019
Guillaume Doquet (A&O) received the Best Student Paper Award (category Machine Learning) at ECML 201

BEST PAPER AWARD - HPCS 2019 - ON SERVER-SIDE FILE ACCESS PATTERN MATCHING
17 July 2019
Francieli Zanon Boito¹ , Ramon Nou², Laércio Lima Pilla³, Jean Luca Bez⁴, Jean-François Méhaut¹, T

BEST FULL PAPER AWARD EDM 2019 - EDUCATIONAL DATA MINING
5 July 2019
DAS3H: Modeling Student Learning and Forgetting for Optimally Scheduling Distributed Practice of Ski

BEST PAPER AWARD - CODIT2019 - STOCHASTIC DUAL DYNAMIC INTEGER PROGRAMMING FOR A MULTI-ECHELON LOT-SIZING PROBLEM WITH REMANUFACTURING AND LOST SALES
14 May 2019
Franco Quezada, Céline Gicquel and Safia Kedad-Sidhoum