MacConville, D.; Farrell, M.; Matt Luckcuck; Monahan, R.

Modelling the Turtle Python library in CSP

Conference paper

MacConville, D., Farrell, M., Matt Luckcuck and Monahan, R. 2022. Modelling the Turtle Python library in CSP. Second Workshop on Agents and Robots for reliable Engineered Autonomy. Open Publishing Association, Australia. https://doi.org/10.4204/eptcs.362.4

Publication process dates
Authors	MacConville, D., Farrell, M., Matt Luckcuck and Monahan, R.
Type	Conference paper
Abstract	Software verification is an important tool in establishing the reliability of critical systems. One potential area of application is in the field of robotics, as robots take on more tasks in both day-to-day areas and highly specialised domains. Robots are usually given a plan to follow, if there are errors in this plan the robot will not perform reliably. The capability to check plans for errors in advance could prevent this. Python is a popular programming language in the robotics domain, through the use of the Robot Operating System (ROS) and various other libraries. Python's Turtle package provides a mobile agent, which we formally model here using Communicating Sequential Processes (CSP). Our interactive toolchain CSP2Turtle with CSP model and Python components, enables Turtle plans to be verified in CSP before being executed in Python. This means that certain classes of errors can be avoided, and provides a starting point for more detailed verification of Turtle programs and more complex robotic systems. We illustrate our approach with examples of robot navigation and obstacle avoidance in a 2D grid-world.
Keywords	Software verification; Robotics ; Python components
Year	2022
Conference	Second Workshop on Agents and Robots for reliable Engineered Autonomy
Journal	Electronic Proceedings in Theoretical Computer Science
Publisher	Open Publishing Association, Australia
ISSN	2075-2180
Digital Object Identifier (DOI)	https://doi.org/10.4204/eptcs.362.4
Web address (URL)	http://dx.doi.org/10.4204/eptcs.362.4
Output status	Submitted
Publication dates	20 Jul 2022
Deposited	31 Jan 2023

Permalink -

https://repository.derby.ac.uk/item/9w93y/modelling-the-turtle-python-library-in-csp

Log in to edit

25
total views
0
total downloads
1
views this month
0
downloads this month

Export as

Related outputs

CSP2Turtle: Verified Turtle Robot Plans

Dara MacConville, Marie Farrell, Luckcuck, M. and Rosemary Monahan 2023. CSP2Turtle: Verified Turtle Robot Plans. Robotics. 12 (62), pp. 1-22. https://doi.org/10.3390/robotics12020062

An Abstract Architecture for Explainable Autonomy in Hazardous Environments

Matt Luckcuck, Hazel M Taylor and Marie Farrell 2022. An Abstract Architecture for Explainable Autonomy in Hazardous Environments. 2022 IEEE 30th International Requirements Engineering Conference Workshops (REW). IEEE Xplore. https://doi.org/10.1109/rew56159.2022.00027

Bridging the gap between single- and multi-model predictive runtime verification

Angelo Ferrando, Rafael C. Cardoso, Marie Farrell, Matt Luckcuck, Fabio Papacchini, Michael Fisher and Viviana Mascardi 2022. Bridging the gap between single- and multi-model predictive runtime verification. Formal Methods in System Design. 59, p. 44–76. https://doi.org/10.1007/s10703-022-00395-7

Formal Verification of a Map Merging Protocol in the Multi-agent Programming Contest

Luckcuck, M. and Cardoso, R. C. 2022. Formal Verification of a Map Merging Protocol in the Multi-agent Programming Contest. in: Alechina, N., Baldoni, M. and Logan, B. (ed.) Engineering Multi-Agent Systems Switzerland Springer. pp. 198–217

Evolution of the IEEE P7009 Standard: Towards Fail-Safe Design of Autonomous Systems

Farrell, M., Luckcuck, M., Pullum, L., Fisher, M., Hessami, A., Danit, G., Murahwi, Z. and Wallace, K. 2022. Evolution of the IEEE P7009 Standard: Towards Fail-Safe Design of Autonomous Systems. 2021 IEEE International Symposium on Software Reliability Engineering Workshops (ISSREW). IEEE Xplore. https://doi.org/10.1109/issrew53611.2021.00109

Towards Refactoring FRETish Requirements

Farrell, M., Luckcuck, M., Sheridan, O. and Monahan, R. 2022. Towards Refactoring FRETish Requirements. in: Deshmukh, J. V., Havelund, K. and Perez, I. (ed.) NASA Formal Methods Switzerland Springer. pp. 272–279

FRETting About Requirements: Formalised Requirements for an Aircraft Engine Controller

Farrell, M., Luckcuck, M., Sheridan, O. and Monahan, R. 2022. FRETting About Requirements: Formalised Requirements for an Aircraft Engine Controller. in: Gervasi, V. and Vogelsang, A. (ed.) Requirements Engineering: Foundation for Software Quality Switzerland Springer. pp. 96-111

Using formal methods for autonomous systems: Five recipes for formal verification

Luckcuck, M. Using formal methods for autonomous systems: Five recipes for formal verification. Journal of Risk and Reliability. pp. 1-19. https://doi.org/10.1177/1748006x211034970

An Overview of Verification and Validation Challenges for Inspection Robots

Fisher, M., Cardoso, R. C., Collins, E. C., Dadswell, C., Denis, L. A., Dixon, C., Farrell, M., Ferrando, A., Huang, X., Jump, M., Kourtis, G., Lisista, A., Luckcuck, M., Luo, S., Page, V., Papacchini, F. and Webster, M. 2021. An Overview of Verification and Validation Challenges for Inspection Robots. Robotics. 10 (2), pp. 1-29. https://doi.org/10.3390/robotics10020067

MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest

Cardoso, R. C., Ferrando, A., Papacchini, F., Luckcuck, M., Linker, S. and Payne, T. R. 2021. MLFC: From 10 to 50 Planners in the Multi-Agent Programming Contest. in: Ahlbrecht, T., Dix, J., Fiekas, N. and Krausburg, T. (ed.) The Multi-Agent Programming Contest 2021 One-and-a-Half Decades of Exploring Multi-Agent Systems Switzerland Springer. pp. 82–107

Towards Compositional Verification for Modular Robotic Systems

Luckcuck, M., Cardoso, R., Dennis, L., Farrell, M. and Fisher, M. 2020. Towards Compositional Verification for Modular Robotic Systems. Second International Workshop on Formal Methods for Autonomous Systems. . https://doi.org/10.4204/eptcs.329.2

Heterogeneous Verification of an Autonomous Curiosity Rover

Cardoso, R. C., Farrell, M., Luckcuck, M., Ferrando, A. and Fisher, M. 2020. Heterogeneous Verification of an Autonomous Curiosity Rover. in: Lee, R., Jha, S., Mavridou, A. and Giannakopoulou, D. (ed.) NASA Formal Methods Switzerland Springer. pp. 353–360

Formal specification and verification of autonomous robotic systems: A survey

Luckcuck, M., Farrell, M., Dennis, L.A., Dixon, C. and Fisher, M. 2019. Formal specification and verification of autonomous robotic systems: A survey. ACM Computing Surveys. 52 (5), pp. 1-41. https://doi.org/10.1145/3342355

A Summary of Formal Specification and Verification of Autonomous Robotic Systems

Luckcuck, M., Farrell, M., Denis, L. A., Dixon, C. and Fisher, M. 2019. A Summary of Formal Specification and Verification of Autonomous Robotic Systems. in: Ahrendt, W. and Tarifa, S. L. T. (ed.) Integrated Formal Methods Switzerland Springer. pp. 538–541

Robotics and Integrated Formal Methods: Necessity Meets Opportunity

Luckcuck, M., Farrell, M. and Fisher, M. 2018. Robotics and Integrated Formal Methods: Necessity Meets Opportunity. in: Furia, C. A. and Winter, K. (ed.) Integrated Formal Methods Switzerland Springer. pp. 161–171

Verifiable Self-Certifying Autonomous Systems

Fisher, M., Collins, E., Dennis, L., Luckcuck, M., Webster, M., Jump, M., Page, V., Patchett, C., Dinmohammadi, F., Flynn, D., Robu, V. and Zhao, X. 2018. Verifiable Self-Certifying Autonomous Systems. 29th IEEE International Symposium on Software Reliability Engineering Workshops, ISSREW 2018. IEEE Xplore. https://doi.org/10.1109/issrew.2018.00028