Our research group is the hub of a centre of excellence, called RoboStar

In 2018, the Royal Academy of Engineering and the University of York agreed to establish a centre of excellence on Software Engineering for Robotics. 

In the five years since, we have carried out research to develop a rich framework of notations and techniques to model and verify control software for robotic systems. 

Through collaboration with academia and industry, across institutions in the UK and five other countries, we have defined and mechanised the RoboStar approach to Software Engineering for Robotics.  It is supported by a collection of tools and demonstrated by dozens of examples.

How can roboticists effectively and efficiently apply modern approaches to design and verification of software when developing their systems, especially those that are safety or mission-critical? This is the problem being solved by RoboStar.

We are interested in application areas such as assistive care, agriculture, emergency response, lab automation, and logistics.

Contact us

Professor Ana Cavalcanti

Professor Ana Cavalcanti

Software Engineering for Robotics Research Group lead

ana.cavalcanti@york.ac.uk

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. 

Stories

Group members

Photo Contact details
Academic staff

Professor Ana Cavalcanti

Academic staff - group lead

ana.cavalcanti@york.ac.uk

Dr Simon Foster

Dr Simon Foster

Academic staff

simon.foster@york.ac.uk

Dr Alvaro Miyazawa

Dr Alvaro Miyazawa

Academic staff

alvaro.miyazawa@york.ac.uk

Dr Pedro Ribeiro

Dr Pedro Ribeiro

Academic staff

pedro.ribeiro@york.ac.uk

 

Professor Jim Woodcock

Professor Jim Woodcock

Academic staff

jim.woodcock@york.ac.uk

Research staff
Arjun Badyal

Arjun Badyal

Research Staff

arjun.badyal@york.ac.uk

Dr James Baxter

Dr James Baxter

Research associate

james.baxter@york.ac.uk

 

Dr Sinem Getir Yaman

Research associate (shared with HISE)

sinem.getir.yaman@york.ac.uk

 

Dr Kangfeng Ye

Dr Kangfeng Ye

Research associate

kangfeng.ye@york.ac.uk

 

Postgraduate research students
Lex Bailey

Lex Bailey

Postgraduate research student

djab501@york.ac.uk

Tom Gebert

Tom Gebert

Postgraduate research student

tgg516@york.ac.uk

Holly Hendry

Holly Hendry

Postgraduate research student

hrh517@york.ac.uk

Christian Laursen 

Christian Laursen

Postgraduate research student

christian.laursen@york.ac.uk

Annabelle Partis

Annabelle Partis

Postgraduate research student

alp565@york.ac.uk

 

Other affiliates
Mark Chattington

Mark Chattington

Industry Fellow

mark.chattington@york.ac.uk

Professor Jon Timmis

Professor Jon Timmis

Visiting associate

 

Contact us

Professor Ana Cavalcanti

Professor Ana Cavalcanti

Software Engineering for Robotics Research Group lead

ana.cavalcanti@york.ac.uk