Verification of the legOS Scheduler using Uppaal
legOS のスケジューラは固定優先度方式で優先度の高いタスクから処理するため、優先度の低いタスクにプロセッサが割り当てられない飢餓状態が発生する可能性がある。このことをUPPAALで確認して、解決策として長く実行されないタスクの優先度を徐々に高くするスケジューラを実装しましたという論文。
author="Lone Halkjaer and Karen Haervi and Anna Ingolfsdottir",
title="{Verification of the legOS Scheduler using Uppaal}",
journal="ENTCS",
volume="39",
number="3",
pages="273--292",
year="2000"