Model-Checking Real-Time Control Programs: Verifying LEGO (R) MINDSTORMS (TM) systems using UPPAAL

T. K. Iversen; K. J. Kristoffersen; Kim Guldstrand Larsen; M. Laursen; R. G. Madsen; S. K. Mortensen; P. Pettersson; C. B. Thomasen

doi:10.1109/EMRTS.2000.854002

Model-Checking Real-Time Control Programs: Verifying LEGO (R) MINDSTORMS (TM) systems using UPPAAL

T. K. Iversen, K. J. Kristoffersen, Kim Guldstrand Larsen, M. Laursen, R. G. Madsen, S. K. Mortensen, P. Pettersson, C. B. Thomasen

Institut for Datalogi

Publikation: Bidrag til tidsskrift › Konferenceartikel i tidsskrift › Forskning

36 Citationer (Scopus)

Abstract

In this paper, we present a method for automatic verification of real-time control programs running on LEGO(R) RCX(TM) bricks using the verification tool UPPALL. The control programs, consisting of a number of tasks running concurrently, are automatically translated into the mixed automata model of UPPAAL. The fixed scheduling algorithm used by the LEGO(R) RCX(TM) processor is modeled in UPPALL, and supply of similar (sufficient) timed automata models for the environment allows analysis of the overall real-time system using the tools of UPPALL. To illustrate our technique for sorting LEGO(R) bricks by color.

Originalsprog	Engelsk
Tidsskrift	Euromicro Conference on Real-Time Systems. Proceedings
Sider (fra-til)	147-155
Antal sider	9
ISSN	1068-3070
DOI	https://doi.org/10.1109/EMRTS.2000.854002
Status	Udgivet - 2000
Begivenhed	Model-Checking Real-Time Control Programs - Varighed: 19 maj 2010 → …

Konference

Konference	Model-Checking Real-Time Control Programs
Periode	19/05/2010 → …

Bibliografisk note

Print ISBN: 0-7695-0734-4

Adgang til dokumentet

10.1109/EMRTS.2000.854002

AUB Link

Søg efter materialet i Aalborg Universitetsbiblioteks søgemaskine

Citationsformater

@inproceedings{0079ea808ac211dbbb3d000ea68e967b,

title = "Model-Checking Real-Time Control Programs: Verifying LEGO (R) MINDSTORMS (TM) systems using UPPAAL",

abstract = "In this paper, we present a method for automatic verification of real-time control programs running on LEGO(R) RCX(TM) bricks using the verification tool UPPALL. The control programs, consisting of a number of tasks running concurrently, are automatically translated into the mixed automata model of UPPAAL. The fixed scheduling algorithm used by the LEGO(R) RCX(TM) processor is modeled in UPPALL, and supply of similar (sufficient) timed automata models for the environment allows analysis of the overall real-time system using the tools of UPPALL. To illustrate our technique for sorting LEGO(R) bricks by color.",

author = "Iversen, {T. K.} and Kristoffersen, {K. J.} and Larsen, {Kim Guldstrand} and M. Laursen and Madsen, {R. G.} and Mortensen, {S. K.} and P. Pettersson and Thomasen, {C. B.}",

note = "Print ISBN: 0-7695-0734-4; Model-Checking Real-Time Control Programs ; Conference date: 19-05-2010",

year = "2000",

doi = "10.1109/EMRTS.2000.854002",

language = "English",

pages = "147--155",

journal = "Euromicro Conference on Real-Time Systems. Proceedings",

issn = "1068-3070",

publisher = "I E E E Computer Society",

}

TY - GEN

T1 - Model-Checking Real-Time Control Programs

T2 - Model-Checking Real-Time Control Programs

AU - Iversen, T. K.

AU - Kristoffersen, K. J.

AU - Larsen, Kim Guldstrand

AU - Laursen, M.

AU - Madsen, R. G.

AU - Mortensen, S. K.

AU - Pettersson, P.

AU - Thomasen, C. B.

N1 - Print ISBN: 0-7695-0734-4

PY - 2000

Y1 - 2000

N2 - In this paper, we present a method for automatic verification of real-time control programs running on LEGO(R) RCX(TM) bricks using the verification tool UPPALL. The control programs, consisting of a number of tasks running concurrently, are automatically translated into the mixed automata model of UPPAAL. The fixed scheduling algorithm used by the LEGO(R) RCX(TM) processor is modeled in UPPALL, and supply of similar (sufficient) timed automata models for the environment allows analysis of the overall real-time system using the tools of UPPALL. To illustrate our technique for sorting LEGO(R) bricks by color.

AB - In this paper, we present a method for automatic verification of real-time control programs running on LEGO(R) RCX(TM) bricks using the verification tool UPPALL. The control programs, consisting of a number of tasks running concurrently, are automatically translated into the mixed automata model of UPPAAL. The fixed scheduling algorithm used by the LEGO(R) RCX(TM) processor is modeled in UPPALL, and supply of similar (sufficient) timed automata models for the environment allows analysis of the overall real-time system using the tools of UPPALL. To illustrate our technique for sorting LEGO(R) bricks by color.

U2 - 10.1109/EMRTS.2000.854002

DO - 10.1109/EMRTS.2000.854002

M3 - Conference article in Journal

SN - 1068-3070

SP - 147

EP - 155

JO - Euromicro Conference on Real-Time Systems. Proceedings

JF - Euromicro Conference on Real-Time Systems. Proceedings

Y2 - 19 May 2010

ER -