Software Engineering for Robotics Research Group

The practical use of advanced and rigorous Software Engineering techniques in many specific areas is an open challenge. In RoboStar, we face this challenge in the exciting area of mobile and autonomous robots. Our focus is on modelling, simulation, testing, and verification techniques with applicability in industry.

RoboStar contributes, first, to the development of the foundations of Software Engineering.  We take into account the physical robots and the environment in which they operate.  We cope with timed and probabilistic behaviours.  We characterise design and verification techniques used for simulation, testing, programming, and proof, in an integrated and consistent way. RoboStar tools support the automated application of our novel techniques to ensure scalability and usability.

Our vision is a 21st-century toolbox for roboticists. In this toolbox, a developer finds diagrammatic and natural language notations to specify assumptions and models for the environment, the robotic platform, and the controller. A rich library includes commonly used artefacts. Because these artefacts are precise, there is no scope for misunderstanding and the toolbox includes techniques for verification of desirable properties.

In the 21st-century toolbox, there are also tools for automatic generation of simulations and tests, techniques highly favoured by practitioners.  The ingenuity of the developer is now focussed in the optimisation of the simulation and of the associated deployed code. Facilities to ensure that optimisations maintain compliance with the models are also in the toolbox.

With the 21st-century toolbox, 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. Mobile and autonomous robots are cheaper and trustworthy.

Our aim is to develop software engineering principles, notations, and techniques for mobile autonomous robots, and to promote the commercialisation of the results by embedding our ideas in practical tools for use in industry. We advance the state of the art by exploring sound mathematical principles and techniques that underlie the current practice, or can enrich the future practice, of Software Engineering for Robotics. In doing so, we have the following objectives:

1. Enable application of modern software verification technology;
   
2. Support consistent use of design, verification, and testing technology across modelling, simulation, and programming tasks;
   
3. Enable creation of artefacts (via model checking, abstraction, theorem proving, and testing) recognised by certification authorities;
   
4. Enthuse young and senior researchers inside and outside York to join our efforts;
   
5. Disseminate the work to industry, and support and encourage adoption and further development as appropriate;
   
6. Identify and support business opportunities created by the possibility of developing trustworthy robotic systems.

To achieve these objectives, we

• adopt modelling notations accepted by the robotics community, covering temporal, probabilistic, and physical properties;
• define a mathematical semantics for the languages;
• identify and propose techniques to analyse the individual artefacts, and propose techniques to relate the artefacts to ensure consistency and correctness;
• tackle case studies to ensure relevance to the state of practice and disseminate the results;
• pursue high levels of automation of all these techniques;
• pursue opportunities for collaborations with researchers inside and outside York and the UK.  

In particular, we aim to contribute actively to YorRobots and the Institute on Safe Autonomy. Our ambition, in the long term, is to enable the development of robot controller software that is trustworthy and cheaper.

The potential impact is far reaching, given the large number of prospective applications. Benefit to society will be realised via increased safety and lower cost of robotic systems. Surveys of industry indicate gains afforded by the kind of techniques we will pursue; some report an order-of-magnitude cost reduction after second or third use.

The multitude of applications that can become economically viable means that we will support cultural enrichment (with robots in museums, galleries and libraries), quality of life (with robots used in domestic activities), health (with robots for home-care), and environmental (with robots for pollution monitoring). Beneficiaries are:

• developers will have modern tools to tackle the difficult problem of designing and verifying robot controllers;
• certifiers will be able to reasonably request evidence of properties of the robotic systems, with traceability to link designs, simulations, tests, and deployments;
• the robotics and software and systems engineering communities will have support to explore novel and safe designs, a framework for the combined use of techniques based on state machines, time, probability, and physical modelling to experiment with integration of novel approaches, and automation approaches for verification techniques;
• the general public will have another tool to understand the abstract concepts of Computer Science and Systems Engineering.

The UK has expertise in safety-critical software in many domains.  RoboStar research further enhances this expertise, and helps the UK to maintain international leadership.

RoboStar work is highly innovative and can transform how the robotics industry uses modelling, simulation, testing, and proof. Together with our collaborators, in academia and industry in the UK and other countries, namely, Brazil, China, France, Germany, and Norway, we form the RoboStar centre of excellence in Software Engineering for Robotics.