A Calculus for Software Engineering of Mobile and Autonomous Robots

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.