Testing Robots Using CSP

TY - GEN

T1 - Testing Robots Using CSP

AU - Cavalcanti, Ana

AU - Baxter, James

AU - Hierons, Robert M.

AU - Lefticaru, Raluca

N1 - Funding Information: Acknowledgements. This work is funded by the EPSRC grants EP/M025756/1 and EP/R025479/1, and by the Royal Academy of Engineering. We have benefited from discussions with Pablo Gómez-Abajo and Mercedes Merayo with regards to Wodel implementation, and Sharar Ahmadi, Alvaro Miyazawa, and Augusto Sampaio with regards to our example and its simulation. Publisher Copyright: © 2019, Springer Nature Switzerland AG. Copyright: Copyright 2019 Elsevier B.V., All rights reserved.

PY - 2019/9/23

Y1 - 2019/9/23

N2 - This paper presents a technique for automatic generation of tests for robotic systems based on a domain-specific notation called RoboChart. This is a UML-like diagrammatic notation that embeds a component model suitable for robotic systems, and supports the definition of behavioural models using enriched state machines that can feature time properties. The formal semantics of RoboChart is given using tock-CSP, a discrete-time variant of the process algebra CSP. In this paper, we use the example of a simple drone to illustrate an approach to generate tests from RoboChart models using a mutation tool called Wodel. From mutated models, tests are generated using the CSP model checker FDR. The testing theory of CSP justifies the soundness of the tests.

AB - This paper presents a technique for automatic generation of tests for robotic systems based on a domain-specific notation called RoboChart. This is a UML-like diagrammatic notation that embeds a component model suitable for robotic systems, and supports the definition of behavioural models using enriched state machines that can feature time properties. The formal semantics of RoboChart is given using tock-CSP, a discrete-time variant of the process algebra CSP. In this paper, we use the example of a simple drone to illustrate an approach to generate tests from RoboChart models using a mutation tool called Wodel. From mutated models, tests are generated using the CSP model checker FDR. The testing theory of CSP justifies the soundness of the tests.

UR - http://www.scopus.com/inward/record.url?scp=85076089634&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-31157-5_2

DO - 10.1007/978-3-030-31157-5_2

M3 - Conference contribution

AN - SCOPUS:85076089634

SN - 9783030311568

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 21

EP - 38

BT - Tests and Proofs - 13th International Conference, TAP 2019, held as part of the 3rd World Congress on Formal Methods 2019, Proceedings

A2 - Beyer, Dirk

A2 - Keller, Chantal

PB - Springer

T2 - 13th International Conference on Tests and Proofs, TAP 2019, held as part of the 3rd World Congress on Formal Methods, FM 2019

Y2 - 9 October 2019 through 11 October 2019

ER -