Department of Computer Science

RoboCalc : a Calculus for Software Engineering of Mobile and Autonomous Robots

A government report from June 2014 indicates that “The UK Government has identified ‘eight great technologies’ which will propel the UK to future growth”; one of them is robotics and autonomous systems. A £13 billion global market is predicted for 2025. A limiting factor, however, is safety, which is imperative for autonomous vehicles and home automation, for example. The UK Technology Strategy Board reports that we are sitting on a “robotics goldmine”, but “Regulation and certification will also be a vital part of RAS deployment…”. Full verification is beyond the state of the art due to the complexity of models and properties for decision-making systems.

We will develop a framework for integrated modelling, simulation, and programming of mobile and autonomous robots, covering, therefore, the full life cycle of development. We will adopt notations akin to those already in widespread use, but enriched with facilities to specify the environment, and timed and probabilistic behaviours. For simulation, we will identify a language that captures facilities of major tools. Our framework will ensure that models and simulations are consistent, and properties established by analysis and simulation are preserved in the robotic platform. The purpose is not to change current practice, but to enrich it with sound validation and verification techniques. Our challenges are sound combination of notations and techniques, automation, and scalability.

Current practice is normally based on standard state machines, without formal semantics, to specify the robot controller only. In the design stage, the state machine guides the development of a simulation, but no rigorous connection between them is established. Also, for implementation in a robotic platform, ad hoc adjustments are normally required to cater for the reality gap between the simulation and the robot hardware and actual environment. There is no accepted paradigm for the development of either simulations or robots, and no portability. Numerous iterations of (re)development and testing, tool dependency, and low-level programming are prevalent, with impact on cost, maintainability, and reliability.

Our framework will enable a transformative change to this scenario. We will provide industry and academia with invaluable tools: (1) guidance to developers; (2) a pathway to consider certification, since there are no guidelines or standards for robotic software; and (3) a platform for tool developers to discuss soundness of their techniques.

Recent news

Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599