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 条

[21] Testing Real-Time Task Networks with Functional Extensions Using Model-Checking
Bueker, Matthias
Metzner, Alexander
Stierand, Ingo
[J]. 2009 IEEE CONFERENCE ON EMERGING TECHNOLOGIES & FACTORY AUTOMATION (EFTA 2009), 2009,
[22] Combining real-time model-checking and fault tree analysis
Schäfer, A
[J]. FME 2003: FORMAL METHODS, PROCEEDINGS, 2003, 2805 : 522 - 541
[23] A LEGO Mindstorms NXT approach for teaching at Data Acquisition, Control Systems Engineering and Real-Time Systems undergraduate courses
Cruz-Martin, A.
Fernandez-Madrigal, J. A.
Galindo, C.
Gonzalez-Jimenez, J.
Stockmans-Daou, C.
Blanco-Claraco, J. L.
[J]. COMPUTERS & EDUCATION, 2012, 59 (03) : 974 - 988
[24] Requirement specification and model-checking of a real-time scheduler implementation
Boukir, Khaoula
Bechennec, Jean-Luc
Deplanche, Anne-Marie
[J]. 28TH INTERNATIONAL CONFERENCE ON REAL TIME NETWORKS AND SYSTEMS, RTNS 2020, 2020, : 89 - 99
[25] Verifying commit-atomicity using model-checking
Flanagan, C
[J]. MODEL CHECKING SOFTWARE, 2004, 2989 : 252 - 266
[26] Model-checking distributed real-time systems with states, events, and multiple fairness assumptions
Wang, F
[J]. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS, 2004, 3116 : 553 - 567
[27] Online testing of real-time systems using UPPAAL
Larsen, KG
Mikucionis, M
Nielsen, B
[J]. FORMAL APPROACHES TO SOFTWARE TESTING, 2005, 3395 : 79 - 94
[28] Towards Model-Checking Security of Real-Time Java']Java Software
Spalazzi, Luca
Spegni, Francesco
Liva, Giovanni
Pinzger, Martin
[J]. PROCEEDINGS 2018 INTERNATIONAL CONFERENCE ON HIGH PERFORMANCE COMPUTING & SIMULATION (HPCS), 2018, : 642 - 649
[29] Real-time face detection and recognition on LEGO Mindstorms NXT robot
Lee, Tae-Hoon
[J]. Advances in Biometrics, Proceedings, 2007, 4642 : 1006 - 1015
[30] Compact data structures and state-space reduction for model-checking real-time systems
Larsen, KG
Larsson, F
Pettersson, P
Yi, W
[J]. REAL-TIME SYSTEMS, 2003, 25 (2-3) : 255 - 275

← 1 2 3 4 5 →