Model-Checking Real-Time Control Programs - Verifying LEGO Mindstorms Systems Using UPPAAL
LEGO Mindstroms 上で動くプログラムを UPPAAL で検証したという論文。スケジューラのモデル化と、NQC 用の API のモデル化を行ってプログラムを全部時間オートマトンに変換して UPPAAL でモデル検査する。
author="Torsten K. Iversen and K{\aa}re J. Kristoffersen and Kim G. Larsen and Rune G. Madsen and Steffen K. Mortensen and Paul Pettersson and Chris B. Thomasen",
title = "{Model-Checking Real-Time Control Programs -- Verifying LEGO Mindstorms System Using UPPAAL}",
booktitle = "Proc. of 12th Euromicro Conference on Real-Time Systems",
publisher = "IEEE Computing Science Press",
pages = "147--155",
year = "2000"
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"