在CSP中对Turtle Python库建模
机器人学
2022-07-21 v1
摘要
软件验证是确立关键系统可靠性的重要工具。一个潜在的应用领域是机器人学,因为机器人在日常领域和高度专业化领域承担的任务越来越多。机器人通常被赋予待执行的计划,若该计划存在错误,机器人将无法可靠执行。提前检查计划中的错误可避免此问题。Python凭借机器人操作系统(ROS)及各种库而成为机器人领域流行的编程语言。Python的Turtle包提供了一个移动智能体,我们在此使用通信顺序进程(CSP)对其进行形式化建模。我们的交互式工具链CSP2Turtle包含CSP模型与Python组件,能够在Python中执行Turtle计划之前于CSP中对其验证。这意味着某些类别的错误可被避免,并为更详细地验证Turtle程序及更复杂的机器人系统提供了起点。我们以2D网格世界中机器人导航与避障为例说明了我们的方法。
引用
@article{arxiv.2207.09706,
title = {Modelling the Turtle Python library in CSP},
author = {Dara MacConville and Marie Farrell and Matt Luckcuck and Rosemary Monahan},
journal= {arXiv preprint arXiv:2207.09706},
year = {2022}
}
备注
In Proceedings AREA 2022, arXiv:2207.09058