A Calculus for Software Engineering of Mobile and Autonomous Robots

到目前为止，指导软件工程的基本数学原理是众所周知的。其符号和过程以这些原则为依据的技术被称为正式方法，直到最近，行业中的主要参与者，如微软，才开始使用正式方法来提高其产品质量。对于软件开发人员来说，在许多工程学科中司空见惯的事情现在才变得可行。形式方法在许多具体应用领域的实际使用仍然是世界各地的科学家和工程师正在解决的一项开放挑战。在RoboCalc，我们在为移动和自主机器人开发控制器软件这一令人兴奋的领域面临着这一挑战。我们的重点是开发在这个行业具有适用性的正式方法。这需要在两个方面突破最先进水平的界限。首先，我们必须为软件工程基础的进一步发展做出贡献。我们需要处理机器人运行所处的物理环境的模型；环境对控制器的行为有直接影响。我们还需要处理时间和概率行为，这些行为既表现在环境中，也表现在控制器本身。最后，我们需要描述和理解用于机器人控制器仿真和编程的语言和设计技术。所有这些都需要以综合和一致的方式加以考虑。要开展的工作的第二个重要方面是设计程序和工具，以支持新技术的自动化应用；这确保了可伸缩性和可用性。我们的愿景是为机器人控制器开发人员提供一个21世纪的工具箱。在这个工具箱中，开发人员可以找到明确的图示符号来指定环境、机器人平台和控制器的模型。对于常用的环境和机器人平台，工具箱包括一系列现成的模型。因为这些模型是精确的，所以没有误解的余地，最重要的是，工具箱包括允许分析模型的理想属性的技术：死锁自由、速度限制等。如今，机器人控制器开发人员青睐的一种验证技术是模拟。在21世纪的工具箱中，有一些工具可以自动生成这些模拟。开发人员的独创性现在集中在模拟和相关部署代码的优化上。通常需要这些优化，因此工具箱还包括确保更改与先前开发的模型保持一致的工具。此外，因为用于模拟和编程的语言是高级的，所以结果是与工具无关的，并且可以部署在各种机器人平台上。所有这些都与当前的做法形成了鲜明对比。如今，高级模型通常要么是非正式的，要么不是真正的高级模型，因为它们是用编程语言描述的。对于这些模型，用于分析的工具是有限的。模拟和部署是独立发展的，因此任何推理都必须在(工具和硬件相关)代码级别进行。有了21世纪的工具箱，设计和测试迭代的代价高昂的周期减少了，即使是在部署时也会很晚才发现问题。此外，开发人员可以证明所产生的控制器满足在建模期间建立的基本性质。用于移动和自主机器人的软件更便宜、更可靠。21世纪的工具箱之所以成为可能，是因为机器人控制器软件的工程学科的微积分被理解并付诸实践。这是我们在RoboCalc中的目标。

The basic mathematical principles that guide the engineering of software are, by far and large, known. The techniques whose notations and procedures are justified by these principles are called formal methods, and it is just relatively recently that main players in industry like Microsoft have started using formal methods to improve the quality of their products. What is routine in many engineering disciplines is just now becoming feasible for software developers. The practical use of formal methods in many specific areas of application is still an open challenge that is being tackled by scientists and engineers worldwide. In RoboCalc, we face this challenge in the exciting area of development of controller software for mobile and autonomous robots. Our focus is on the development of formal methods with applicability in this industry. This requires pushing the boundaries of the state of the art in two respects. Firstly, we have to contribute for the further development of the foundations of software engineering. We need to cope with models of the physical environment in which robots operate; the environment has a direct impact on the behaviour of the controller. We also need to cope with timed and probabilistic behaviours, which are exhibited both by the environment and the controllers themselves. Finally, we need to characterise and understand the languages and design techniques used for simulation and programming of robot controllers. All this needs to be considered in an integrated and consistent way. The second important aspect of the work to be carried out is the design of procedures and tools to support the automated application of the novel techniques; this ensures scalability and usability. Our vision is a 21st-century toolbox for robot-controller developers. In this toolbox, a developer can find unambiguous diagrammatic notations to specify models for the environment, the robotic platform, and the controller. For commonly used environments and robotic platforms, the toolbox includes a range of ready-made models. Because these models are precise, there is no scope for misunderstanding and, most importantly, the toolbox includes techniques that allow analysis of desirable properties of the models: deadlock freedom, speed limits, and so on. A technique for validation that robot controller developers favour nowadays is simulation. In the 21st-century toolbox, there are tools for automatic generation of these simulations. The ingenuity of the developer is now focussed in the optimisation of the simulation and of the associated deployed code. These optimisations are often needed, and so the toolbox also includes facilities to ensure that changes maintain compliance with the models previously developed. Moreover, because the languages used for simulation and programming are high-level, the results are tool independent, and can be deployed in a variety of robotic platforms. All this is in stark contrast with current practice. Nowadays, typically, high-level models are either informal or not really of a high level, as they are described in a programming language. With these models, facilities for analysis is limited. Simulations and deployments evolve independently, and so any reasoning has to be at the (tool and hardware dependent) code level. With the 21st-century toolbox, the costly cycles of iterations of design and testing, with problems found very late, even just at deployment time, are reduced. Moreover, the developer can demonstrate that the controller produced satisfies essential properties established during modelling. Software for mobile and autonomous robot is cheaper and more reliable. The 21st-century toolbox has been made possible because the calculus for the engineering discipline for robot-controller software is understood and put into practice. This is our goal in RoboCalc.