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 .
Registration is now open for the RoboStar Summer School, a four-day workshop running from the 29th of June to the 2nd of July. Participants will explore the full RoboStar technology stack from modelling, verification, and simulation to testing, deployment, and assurance. The programme is grounded in over 10 years of RoboStar research, applying rigorous software engineering techniques to autonomous robotics, including ethical and legal concerns, adaptation, human-in-the-loop assurance, and physical behaviour modelling.
The Summer School will feature a series of eight modules, covering various topics related to our notations and techniques. We are pleased to welcome leading RoboStar researchers and industry experts from Brazil, Denmark, France, Norway, the UK, and the RoboStar York team, who will present novel notations, techniques, and tools illustrated through rich research and industrial use cases.
See the event page for more details.
Here is a date for your diaries. From the 29th of June to the 2nd of July, there will be a Summer School presenting the range of technologies available in RoboStar, covering modelling, simulation, deployment, and assurance. The Summer School will feature a series of eight modules, over four days, covering various topics related to our notations and techniques.
This face-to-face event will take place in the UK, but we already have confirmed contributions and presence from the leaders of several RoboStar branches (Brazil (Augusto Sampaio ), Denmark (Peter Gorm Larsen ), France (Thierry Lecomte ), and Norway (Alireza David Anisi )). This is in addition to the contributions of their teams and several members of the UK RoboStar York team.
More details and registration instructions will be available in February.
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 an exciting new project starting in September 2026 in Autonomous Robots for Manipulating Hazardous Substances (jointly funded with UK Atomic Energy Authority/RACE).
Read more...Alvaro Miyazawa presented our SoSyM paper “Diagrammatic physical robot models” on the Journal First track at MODELS 2025. This work extends RoboSim by introducing a new diagrammatic notation for modelling physical robotic platforms using block diagrams, enabling automatic simulation and mathematical reasoning over complete robotic systems.
RoboStar was delighted to participate in a Soapbox Science event in York city centre, as part of York Festival of Ideas. Fang Yan took to the soapbox to showcase RoboStar’s work to the public, demonstrating how we use formal methods and software engineering to help ensure that robots behave safely and reliably. Fang reported that it was a fantastic opportunity to engage with a wide audience, from children to adults, and to discuss the exciting challenges in building trustworthy robotic systems.
Ana Cavalcanti led an expert panel on “Design and verification of safe and reliable lab robots” at the the London Lab Live event. The panel featured Ian Fairlamb (co-director of the Albert CDT), Radhika Gudipati (ARIA), and George Karageorgis (AstraZeneca), bringing together insights from academia, industry, and funders. Together, they tackled important topics around safety, reliability, security, and ethics in lab automation.
RoboStar is proud to have participated in FASE 2025 (part of the ETAPS joint conferences):
RoboStar members Ana Cavalcanti and Jim Woodcock attended the euRobotics Forum 2025 alongside PAL robotics to represent the RoboSAPIENS EU Project and discuss the next steps for the project.
The RoboStar teams from France (Thierry Lecomte , ClearSY), Brazil (Paulo Rolim , UFRN), and York (Ana Cavalcanti and Pedro Ribeiro ) presented a course at RoME 25. The team presented their joint work on the use of RoboStar technology to implement a safe firefighting UAV on top of ClearSY’s safety platform.
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.
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
