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.
Over the course of 2 weeks, Ana Cavalcanti delivered a module on RoboChart at UFPE, including practical sessions on the use of RoboTool/FDR for modelling and analysis. Students are now using RoboTool to support modelling and analysis of robotic systems as part of their degree projects.
RoboCalc was presented to a group of experts from the Federal University of Pernambuco (UFPE) in Brazil and the Center for Advanced Studies and Systems Cesar. UFPE has the largest research group on software reliability in Brazil. Cesar is a business incubator and innovation centre, the largest component of Porto Digital in Recife (where UFPE is located). We are discussing close collaboration with UFPE and Cesar on topics related to RoboCalc.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599