Formal Design, Verification and Implementation of Robotic Controller Software via RoboChart and RoboTool

TY - JOUR

T1 - Formal Design, Verification and Implementation of Robotic Controller Software via RoboChart and RoboTool

AU - Li, Wei

AU - Ribeiro, Pedro

AU - Miyazawa, Alvaro

AU - Redpath, Richard

AU - Cavalcanti, Ana Lucia Caneca

AU - Alden, Kieran James

AU - Woodcock, Jim

AU - Timmis, Jon

N1 - © The Author(s) 2024

PY - 2024/7/5

Y1 - 2024/7/5

N2 - Current practice in simulation and implementation of robot controllers is usually undertaken with guidance from high-level design diagrams and pseudocode. Thus, no rigorous connection between the design and the development of a robot controller is established. This paper presents a framework for designing robotic controllers with support for automatic generation of executable code and automatic property checking. A state-machine based notation, RoboChart, and a tool (RoboTool) that implements the automatic generation of code and mathematical models from the designed controllers are presented. We demonstrate the application of RoboChart and its related tool through a case study of a robot performing an exploration task. The automatically generated code is platform independent and is used in both simulation and two different physical robotic platforms. Properties are formally checked against the mathematical models generated by RoboTool, and further validated in the actual simulations and physical experiments. The tool not only provides engineers with a way of designing robotic controllers formally but also paves the way for correct implementation of robotic systems.

AB - Current practice in simulation and implementation of robot controllers is usually undertaken with guidance from high-level design diagrams and pseudocode. Thus, no rigorous connection between the design and the development of a robot controller is established. This paper presents a framework for designing robotic controllers with support for automatic generation of executable code and automatic property checking. A state-machine based notation, RoboChart, and a tool (RoboTool) that implements the automatic generation of code and mathematical models from the designed controllers are presented. We demonstrate the application of RoboChart and its related tool through a case study of a robot performing an exploration task. The automatically generated code is platform independent and is used in both simulation and two different physical robotic platforms. Properties are formally checked against the mathematical models generated by RoboTool, and further validated in the actual simulations and physical experiments. The tool not only provides engineers with a way of designing robotic controllers formally but also paves the way for correct implementation of robotic systems.

U2 - 10.1007/s10514-024-10163-7

DO - 10.1007/s10514-024-10163-7

M3 - Article

SN - 0929-5593

VL - 48

JO - Autonomous Robots

JF - Autonomous Robots

M1 - 14

ER -