<< On the Semantics of Software Adaptation | ホーム | Model-Checking Real-Time Control Programs - Verifying LEGO Mindstorms Systems Using UPPAAL >>

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"

タグ : ,
コメント追加 RSS feed for responses to this blog entry
投稿者 kw : 2006/12/02 13:11:58 JST #



コメント追加 トラックバック送信