RoboStar is a centre of excellence dedicated to research and technology transfer in the area of Software Engineering for Robotics. Research and development covers various aspects of model-based software engineering: modelling, simulation, testing, and verification, covering control software, physical models of the platform and scenarios, environment assumptions, and human behaviour. It is one of the largest research groups in the world that brings a diverse membership of researchers working in robotics under a single umbrella. Its membership comprises UK researchers from the universities of York, Sheffield and King’s College, as well as researchers from around the world: Brazil, Denmark, France, Germany, and Norway.
We are always hiring at all levels (from undergraduate interns, to PhD students, and research assistants). If you’re interested in joining RoboStar, get in touch with Ana Cavalcanti .
In a recent interview for Scientific Computing World, Ana Cavalcanti discusses the work of RoboStar, including the challenges for developing robotic software and the techniques we use for verification.
RoboStar has received funding from the Royal Academy of Engineering, in partnership with Google Deep Mind and the Hg Foundation, to host undergraduate interns in Summer 2025 under the Google DeepMind Research Ready programme. Applications are open until Friday 21 March 2025, 11.59pm GMT. See here more information and to apply.
Kangfeng Ye has been interviewed for the Scholarly Communication podcast about writing the paper “Probabilistic modelling and verification using RoboChart and PRISM”, in an episode titled “Use Sequential Internal Review to Improve Your Next Submission”.
Are you a UK applicant looking for a fully-funded PhD opportunity in robotics?
RoboStar, a world-leading centre of excellence for software engineering for robotics, is seeking postgraduate researchers for three exciting new projects starting in September 2025:
Ana Cavalcanti and Ian Fairlamb will contribute to the London Lab Live event in May. They will discuss “Design and verification of safe and reliable lab robots” based on their plans and experience with the Albert CDT.
The UK Atomic Energy Authority’s centre for Remote Applications in Challenging Environments (RACE), in collaboration with RoboStar, is offering a studentship for a PhD researching Autonomous Robots for Gloveboxes. See here for more information and to apply.
The RoboStar teams from France (Thierry Lecomte , ClearSY), Brazil (Paulo Rolim , UFRN), and York (Ana Cavalcanti and Pedro Ribeiro ) will contribute a course to RoME 25. The team will present their joint work on the use of RoboStar technology to implement a safe firefighting UAV on top of ClearSY’s safety platform. Registrations are open, and the team is looking forward to meeting the students.
RoboStar has received funding from the Royal Academy of Engineering, in partnership with Google Deep Mind and the Hg Foundation, to host undergraduate interns next Summer under the Google DeepMind Research Ready scheme. RoboStar and SAINTS will collaborate to host 12 students in the Institute for Safe Autonomy. They will work together to push forward the state of the art on design, verification, assurance of AI systems. Applications open in early 2025.
RoboStar is proud to have participated in FM 2024:
Ana Cavalcanti is giving a keynote talk at the 50th Euromicro Conference Series on Software Engineering and Advanced Applications (SEAA) 2024 taking place at Sorbonne University, Paris, France, from 28th to 30th of August 2024.
Currently there are nine ongoing research projects. The group started its work as part of the RoboCalc agenda.
Investigators: Ana Cavalcanti and Jim Woodcock
Funding: EU Horizon Grant Agreement 101133807
This project focuses on how robots can adapt to unexpected changes in their environment in a way that remains safe and trustworthy. This will include the development of software architectures to enable adaptation, and the development of deep learning techniques to quantify and reduce uncertainty in analysing the environment and formulating an updated plan of action. This is an EU-funded project led by Peter Gorm Larsen at Aarhus University in Denmark. The contribution of RoboStar at the University of York will include using the RoboStar technologies to model and verify the RoboSapiens architecture and case studies.
Investigators: Ana Cavalcanti and Jim Woodcock
UKRI Trustworthy Autonomous Systems (TAS) programme, funded through the UKRI Strategic Priorities Fund brings together the research communities and key stakeholders to drive forward cross-disciplinary fundamental research to ensure that autonomous systems are safe, reliable, resilient, ethical and trusted. The Verifiability Node of this programme is a £3M project led by Prof. Mohammad Mousavi . Ana Cavalcanti and Jim Woodcock contributions to this project are related with the definition and formalisation of notations to support unified verification of a variety of properties using a variety of techniques.
Investigators: Ana Cavalcanti (PI), Brijesh Dongol , Rob Hierons (PI), Jim Woodcock and Jon Timmis
Funding: EPSRC (EP/R025479/1), EPSRC (EP/R025134/2)
This project will see the development of novel automated test-generation techniques for mobile and autonomous robots. A RoboTest tester will construct a model of a robot using a notation already employed in the design of simulations and implementations. With the push of a button, the tester generates and executes tests for simulations, choosing from a variety of simulators, and then produces deployment tests. The RoboTest tester is in a strong position to understand the reality gap between the simulation and the real world. The RoboTest tester knows that test verdicts are correct and that tests are guaranteed to find faults of an identified class, and so can answer the difficult question: have we tested enough? RoboTest is moving the testing of mobile and autonomous robots onto a sound footing, making testing more efficient and effective and reducing longer term costs.
Investigator: Ana Cavalcanti
UKRI Trustworthy Autonomous Systems (TAS) programme, funded through the UKRI Strategic Priorities Fund brings together the research communities and key stakeholders to drive forward cross-disciplinary fundamental research to ensure that autonomous systems are safe, reliable, resilient, ethical and trusted. The Resilience Node of this programme is a £3M project led by York’s Radu Calinescu . Ana Cavalcanti ‘s contribution to this project is related to the definition of usable and formal notations to capture resilience requirements.
Investigators: Ana Cavalcanti (PI), Jim Woodcock and Jon Timmis
Funding: EPSRC (EP/M025756/1)
This project involves developing a framework for integrated modelling, simulation, and programming of mobile and autonomous robots covering the full life cycle of development. The project adopts similar notations to those already in widespread use, but enriched with facilities to specify the environment and timed and probabilistic behaviours. For simulation, a language that captures facilities of major tools will be identified. The framework ensures 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. Challenges will be sound combination of notations and techniques, automation, and scalability.
Investigators: Simon Foster (PI)
Funding: EPSRC (EP/S001190/1)
The goal of the CyPhyAssure project is to develop a methodology for compositional assurance of autonomous robots. This will be supported by a mechanical safety case platform for robotic multi-models, and associated verification tools. The platform will be based in Isabelle, and will support both construction of arguments and production of supporting evidence from formal verification tools. We will validate it by application to assurance demonstrators from our industrial partners, and support our technology with an outreach programme. We will mechanise denotational semantics for a number of modelling languages using our Isabelle/UTP framework, which will facilitate the production of verification tools.
Investigators: Augusto Sampaio (PI)
Funding: INES
The main objective of this project is to create a systematic and rigorous methodology to specify, verify, design and implement robotic applications. It is closely connected with the RoboCalc project. The focus is on the design of a graphical simulation language, RoboSim, and mapping models in RoboSim to several target platforms: Arduino, B and Simulink/Stateflow, among others. Development of the final implementations from the simulations is also in scope. Finally, we will also consider probabilistic models, modelling of the environment and the development of real-world applications.
Investigators: Jim Woodcock (PI)
Funding: The Royal Society
Cyber-physical systems (CPSs) are characterised as systems that are controlled and monitored by software and are tightly integrated with the internet and its users. Physical and software components are intimately linked, operating in different time-bands and at different spatial scales. They exhibit emergent behaviours arising from their interactions and changing environments. Examples of CPSs include smart grids, self-driving cars, fly-by-wire avionics, personalised healthcare, process control systems, and autonomous robotics. CPSs are complex and raise significant challenges in dependability and trust. Correspondingly strong guarantees are needed in order to justify their deployment. This project addresses these issues by devising and supporting methods for modelling their requirements and providing precise contracts for what a CPS may and may not do.
Investigator: Dehui Du
We are developing a model-transformation method based on timed automata patterns and mapping rules. We are also implementing a tool for automatic transformation from a RoboSim model to an NTA model for UPPAAL. We are working on case studies, plan to investigate automatic generation of properties for robots, and a new domain-specific modelling language for describing specific environments.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500
University of York legal statements
