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"