文章基本信息

标题：Model-Checking Real-Time Control Programs. Verifying LEGO Mindstorms Systems Using UPPAAL
本地全文：下载
作者：Torsten K. Iversen ; Kåre J. Kristoffersen ; Kim G. Larsen 等
期刊名称：BRICS Report Series
印刷版ISSN：0909-0878
出版年度：1999
卷号：6
期号：53
出版社：Aarhus University
摘要：In this paper, we present a method for automatic verification of real-time control programs running on LEGO RCX bricks using the verification tool UPPAAL. The control programs, consisting of a number of tasks running concurrently, are automatically translated into the timed automata model of UPPAAL. The fixed scheduling algorithm used by the LEGO RCX processor is modeled in UPPAAL, and supply of similar (sufficient) timed automata models for the environment allows analysis of the overall real-time system using the tools of UPPAAL. To illustrate our techniques we have constructed, modeled and verified a machine for sorting LEGO bricks by color.