Model-checking real-time control programs -: Verifying LEGO® MINDSTORMS™ systems using UPPAAL

被引：0

作者：

Iversen, TK ^{[1
]}

Kristoffersen, KJ ^{[1
]}

Larsen, KG ^{[1
]}

Laursen, M ^{[1
]}

Madsen, RG ^{[1
]}

Mortensen, SK ^{[1
]}

Petterson, P ^{[1
]}

Thomasen, CB ^{[1
]}

机构：

[1] Aalborg Univ, Dept Comp Sci, BRICS, DK-9220 Aalborg, Denmark

来源：

EUROMICRO RTS 2000: 12TH EUROMICRO CONFERENCE ON REAL-TIME SYSTEMS, PROCEEDINGS | 2000年

关键词：

D O I：

暂无

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

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.

引用

页码：147 / 155

页数：5

共 50 条

[1] MODEL-CHECKING FOR PROBABILISTIC REAL-TIME SYSTEMS
ALUR, R
COURCOUBETIS, C
DILL, D
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 510 : 115 - 126
[2] Model-checking real-time concurrent systems
Romanovsky, I
[J]. 16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 439 - 439
[3] Model-Checking Temporal Properties of Real-Time HTL Programs
Carvalho, Andre
Carvalho, Joel
Pinto, Jorge Sousa
de Sousa, Simao Melo
[J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION, AND VALIDATION, PT II, 2010, 6416 : 191 - +
[4] Real-time Control Teaching Using LEGO® MINDSTORMS® NXT Robot
Grega, Wojeiech
Pilat, Adam
[J]. 2008 INTERNATIONAL MULTICONFERENCE ON COMPUTER SCIENCE AND INFORMATION TECHNOLOGY (IMCSIT), VOLS 1 AND 2, 2008, : 579 - 582
[5] Kronos: A model-checking tool for real-time systems
Bozga, M
Daws, C
Maler, O
Olivero, A
Tripakis, S
Yovine, S
[J]. COMPUTER AIDED VERIFICATION, 1998, 1427 : 546 - 550
[6] MODEL-CHECKING IN DENSE REAL-TIME
ALUR, R
COURCOUBETIS, C
DILL, D
[J]. INFORMATION AND COMPUTATION, 1993, 104 (01) : 2 - 34
[7] Scheduling Real-Time Systems with Periodic Tasks using a Model-checking Approach
Olivera Salmon, Arianna Z.
Gonzalez del Foyo, Pedro M.
Silva, Jose R.
[J]. 2014 12TH IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 2014, : 73 - +
[8] Dense time-based model-checking of real-time systems
Zhang, GQ
Rong, M
[J]. PROCEEDINGS OF THE 11TH JOINT INTERNATIONAL COMPUTER CONFERENCE, 2005, : 785 - 788
[9] REAL-TIME MODEL-CHECKING: PARAMETERS EVERYWHERE
Bruyere, Veronique
Raskin, Jean-Francois
[J]. Logical Methods in Computer Science, 2007, 3 (01)
[10] Real-time model-checking:: Parameters everywhere
Bruyère, V
Raskin, JF
[J]. FST TCS 2003: FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, 2003, 2914 : 100 - 111

← 1 2 3 4 5 →