RoboStar is a centre of excellence in 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.
On the 23rd of March 2023, Pedro Ribeiro will be delivering a talk on “Co-verification: from simulation to verification” as part of the UKRI Trustworthy Autonomous Systems Hub Verfiability Node talk series.
Lex Bailey will be presenting a paper on “Checking Confidentiality in Isabelle/UTP” at the Formal Methods 2023 Doctoral Symposium in Lübeck, Germany.
Currently there are eight ongoing research projects. The group started its work as part of the RoboCalc agenda.
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
