Department of Computer Science


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, Surrey, King’s College, and from Thales, as well as researchers from around the world: Brazil, China, 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 .

"Software Engineering is key to the design of trustworthy mobile and autonomous robots. RoboStar is developing technology to put Software Engineering on the same standing as traditional engineering disciplines, where models, supported by tools and mathematical foundations, drive the whole production process: simulation, testing, deployment, and provision of evidence of quality."
Ana Cavalcanti, Director of RoboStar

Recent news

More news...

Recent publications

  • 1. N. Feng, L. Marsso, S. G. Yaman, Y. Baatartogtokh, R. Ayad, V. O. D. Mello, B. Townsend, I. Standen, I. Stefanakos, C. Imrie, G. N. Rodrigues, A. L. C. Cavalcanti, R. Calinescu, M. Chechik: Analyzing and Debugging Normative Requirements via Satisfiability Checking. In: Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. Association for Computing Machinery, New York, NY, USA (2024).
  • 2. S. G. Yaman, P. Ribeiro, C. Burholt, M. Jones, A. L. C. Cavalcanti, R. Calinescu: Toolkit for specification, validation and verification of social, legal, ethical, empathetic and cultural requirements for autonomous agents. Science of Computer Programming. 236, 103118 (2024).
  • 3. K. Ye, S. Foster, J. Woodcock: Formally verified animation for RoboChart using interaction trees. Journal of Logical and Algebraic Methods in Programming. 137, 100940 (2024).
  • 4. A. Cavalcanti, M. C. Filho, P. Ribeiro, A. Sampaio: Laws of Timed State Machines. The Computer Journal. bxad124 (2023).
  • 5. J. Baxter, G. Carvalho, A. Cavalcanti, F. R. Júnior: RoboWorld: Verification of Robotic Systems with Environment in the Loop. Form. Asp. Comput. 35, (2023).
More publications...

Research Projects

Currently there are nine ongoing research projects. The group started its work as part of the RoboCalc agenda.

RoboSAPIENS: Robotic Safe Adaptation In Unprecedented Situations

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.

EPSRC Trustworthy Autonomous System - Verifiability Node

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.

RoboTest: Systematic Model-Based Testing and Simulation of Mobile Autonomous Robots

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.

EPSRC Trustworthy Autonomous System - Resilience Node

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.

RoboCalc: A Calculus for Software Engineering of Mobile and Autonomous Robots

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.

CyPhyAssure: Compositional Safety Assurance for Cyber-Physical Systems

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.

RoboTIC@ - Information and Communication Technology for Robotics and Applications

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.

Requirements Modelling for Cyber-Physical Systems

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.

Model Transformation from RoboSim to Networks of Timed Automata for UPPAAL

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