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.

We’re improving state of the art on modelling, simulation, testing, and proof of properties.

We have produced the only end-to-end approach to design and verification of robotic software that can provide evidence of key properties that may depend on behaviour of humans, software implementation, and aspects of the physical robot and environment.  

We’re automating the use of Software Engineering techniques that support and enrich current practice.

We have developed a collection of tools to automate application of RoboStar notations and techniques.  The tools are freely available for use, and include support for modelling, automatic generation of simulations and tests, and proof.  

We’re educating people with the new skills they need.

Together, we have given dozens of keynote talks, tutorials, and courses that showcase the RoboStar framework. We also offer courses to industry professionals to support them in applying modern practices of software design and verification, and the RoboStar framework in particular.