A Calculus for Software Engineering of Mobile and Autonomous Robots

Lead Research Organisation: University of York
Department Name: Computer Science

Abstract

The basic mathematical principles that guide the engineering of software are, by far and large, known. The techniques whose notations and procedures are justified by these principles are called formal methods, and it is just relatively recently that main players in industry like Microsoft have started using formal methods to improve the quality of their products. What is routine in many engineering disciplines is just now becoming feasible for software developers.

The practical use of formal methods in many specific areas of application is still an open challenge that is being tackled by scientists and engineers worldwide. In RoboCalc, we face this challenge in the exciting area of development of controller software for mobile and autonomous robots. Our focus is on the development of formal methods with applicability in this industry.

This requires pushing the boundaries of the state of the art in two respects. Firstly, we have to contribute for the further development of the foundations of software engineering. We need to cope with models of the physical environment in which robots operate; the environment has a direct impact on the behaviour of the controller. We also need to cope with timed and probabilistic behaviours, which are exhibited both by the environment and the controllers themselves. Finally, we need to characterise and understand the languages and design techniques used for simulation and programming of robot controllers. All this needs to be considered in an integrated and consistent way. The second important aspect of the work to be carried out is the design of procedures and tools to support the automated application of the novel techniques; this ensures scalability and usability.

Our vision is a 21st-century toolbox for robot-controller developers. In this toolbox, a developer can find unambiguous diagrammatic notations to specify models for the environment, the robotic platform, and the controller. For commonly used environments and robotic platforms, the toolbox includes a range of ready-made models. Because these models are precise, there is no scope for misunderstanding and, most importantly, the toolbox includes techniques that allow analysis of desirable properties of the models: deadlock freedom, speed limits, and so on.

A technique for validation that robot controller developers favour nowadays is simulation. In the 21st-century toolbox, there are tools for automatic generation of these simulations. The ingenuity of the developer is now focussed in the optimisation of the simulation and of the associated deployed code. These optimisations are often needed, and so the toolbox also includes facilities to ensure that changes maintain compliance with the models previously developed. Moreover, because the languages used for simulation and programming are high-level, the results are tool independent, and can be deployed in a variety of robotic platforms.

All this is in stark contrast with current practice. Nowadays, typically, high-level models are either informal or not really of a high level, as they are described in a programming language. With these models, facilities for analysis is limited. Simulations and deployments evolve independently, and so any reasoning has to be at the (tool and hardware dependent) code level.

With the 21st-century toolbox, the 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. Software for mobile and autonomous robot is cheaper and more reliable.

The 21st-century toolbox has been made possible because the calculus for the engineering discipline for robot-controller software is understood and put into practice. This is our goal in RoboCalc.

Planned Impact

The potential impact of the work we propose is far reaching, given the large number of prospective and current applications of mobile and autonomous robots. Benefit to society is going to be realised, in the longer term, via the increased safety and lower cost of the robotic systems developed with the use of our techniques. For example, autonomous vehicles can become widespread, with uses for entertainment, surveillance, defense and so on, and industrial robots can become more interactive and cooperate with humans.

In more detail, we note the following non-academic beneficiaries:

* general public, who will have another tool to understand the abstract concepts of Computer Science and Software Engineering;
* developers, who will have modern tools to tackle the difficult problem of programming robot controllers;
* certifiers, who will have techniques for program verification, and can reasonably request from developers the artefacts that provide evidence of properties of the robot controllers, with traceability provided to link designs, simulations, and deployments;

We expect the impact on the general public to be achieved during the lifetime of the project and beyond, on developers at the end of the project, and on certifiers in the longer term.

We note that our approach is based on state machines, a notation well accepted by engineers. In addition, we eagerly pursue automation. This addresses scalability, but also accessibility of techniques and results. Impact is, in this way, improved, from the point of view of developers and certifiers.

The multitude of applications of robots that can become economically viable mean that, indirectly, our results can support cultural enrichment (with robots used in museums, galleries and libraries), quality of life (with robots used in domestic cleaning activities), health (with robots used in home-care setups), environmental protection (with robots used for pollution monitoring). On a more technical vein, our results can provide evidence that safety cases can be made for mobile autonomous robots. This can influence governmental and industrial guidelines both in the UK and internationally. In the case of businesses involved in robot development themselves, our results will generate the knowledge that they can use to significantly improve their design, validation, and verification skills. With the growth expected in the market, the impact will be significant, and attract and optimise investment.

While some of our research assistants will concentrate on the scientific foundations of the engineering of robot-controller software, some will have just the right skills to work in the modern robotics industry. Undergraduate and MSc students will also benefit from our results, since our demonstrators and examples can be incorporated in modules on software engineering and robotics.

According to market reports, the UK software industry is on the rise and is presently the second largest market by value in Europe. The UK has expertise in the development of safety-critical software in a wide number of domains. The state-of-the-art technology that we will developed will further enhance this expertise, and help us to maintain significant international leadership. The UK has clear international leadership in formal methods. This project will help us maintain our position. We will ensure our continued presence in a very important section of the society.
 
Description The goal of our work is the development of a 21st-century toolbox for robot-controller developers. The development of this toolbox and its scientific underpinnings are well under way. We already have a framework for with unambiguous diagrammatic notations to specify models for the robotic platform and the controller. Because these models are precise, there is no scope for misunderstanding and, most importantly, the toolbox includes techniques that allow analysis of desirable properties of the models: deadlock freedom, speed limits, and so on. We cater for both timed and probabilistic properties.

A technique for validation that robot controller developers favour nowadays is simulation. In the 21st-century toolbox, there are tools for automatic generation of these simulations. The ingenuity of the developer is now focussed in the optimisation of the simulation and of the associated deployed code. Since the languages used for simulation are high-level, the results are tool independent, and can be deployed in a variety of robotic platforms. Because of the automation, we have usability and scalability.
Exploitation Route The outcomes of this project are being taken forward in a variety of pathways to impact: additional funding attracted (from EPSRC and RAEng), and take up in industry is under way. Industrial interest nationally and internationally is leading to technology transfer activities funded by industry.
Sectors Aerospace

Defence and Marine

Agriculture

Food and Drink

Chemicals

Digital/Communication/Information Technologies (including Software)

Electronics

Environment

Healthcare

Leisure Activities

including Sports

Recreation and Tourism

Manufacturing

including Industrial Biotechology

Culture

Heritage

Museums and Collections

Retail

Transport

URL https://robostar.cs.york.ac.uk/
 
Description We have participated in public engagement activities to disseminate the work. We have reached out to schools, the York Festival of Ideas, and the Pint of Science, contribute to RAEng public engagement events, and recorded vidoes and podcasts. For an audience more focused on science and engineering, but still generalist, we have written popular articles, given webinars, and published podcasts. We have also developed new material for YorkTalks (https://www.york.ac.uk/research/events/yorktalks/). We have material ready and are developing more material to engage in this form of activity. As a result, we have also trained the Research Assistants in dealing with the public. We are engaging with industry nationally and internationally to train human resources and support the development of new tools. Colleagues in industry are also leading the effort. T. Lecomte, D. Déharbe, P. Fournier, M. Oliveira: The CLEARSY safety platform: 5 years of research, development and deployment. Sci. Comput. Program. 199, 102524 (2020). reports on efforts by industry to provide support for use of RoboTest technology in their safety platform. Another current effort is providing support for implementation of RoboTest results in a prized testing tool adopted by major players in the cyber-physical industry. An incoming Royal Academy of Engineering Fellowship is pursuing technology transfer by extending the result to deal with humans in the loop. Colleagues in academia are also building on our work to develop their own research independently. An example is reported in W. Lindoso, S. C. Nogueira, R. Domingues, L. Lima: Visual Specification of Properties for Robotic Designs. In: S. Campos and M. Minea (eds.) Formal Methods: Foundations and Applications - 24th Brazilian Symposium, SBMF 2021, Virtual Event, December 6-10, 2021, Proceedings. pp. 34-52. Springer (2021). We are working on a Prosperity Partnership, and establishing a industry-funded CDT.
First Year Of Impact 2024
Sector Digital/Communication/Information Technologies (including Software),Transport
Impact Types Cultural

Societal

Economic

 
Description 1000 Talents Programme
Amount ¥1,950,000 (CNY)
Organisation National Science Foundation China 
Sector Public
Country China
Start 11/2019 
End 11/2024
 
Description Aarhus University Centre for Digital Twins
Amount 970,392 kr. (DKK)
Funding ID 2018-019 
Organisation Aarhus University 
Sector Academic/University
Country Denmark
Start 11/2019 
End 11/2024
 
Description Chair in Emerging Technologies
Amount £1,300,000 (GBP)
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 03/2018 
End 02/2028
 
Description Chair in Emerging Technologies Top-Up Award 1
Amount £55,000 (GBP)
Funding ID CiET1819\TUA\11 
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 03/2019 
End 02/2020
 
Description Chair in Emerging Technologies Top-Up Award 2
Amount £55,000 (GBP)
Funding ID CiET1920\TUA\13 
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 03/2020 
End 02/2021
 
Description Chair in Emerging Technologies Top-Up Award 4
Amount £55,000 (GBP)
Funding ID CiET1920\TUA\2021\4 
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 03/2021 
End 02/2022
 
Description CyPhyAssure: Compositional Safety Assurance for Cyber-Physical Systems
Amount £562,549 (GBP)
Funding ID EP/S001190/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 05/2018 
End 07/2021
 
Description Distinguished Visiting Fellow DVF (Round 4)
Amount £2,865 (GBP)
Funding ID DVF1516\4\23 
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 05/2016 
End 07/2016
 
Description EPSRC Standard Grant
Amount £1,776,973 (GBP)
Funding ID EP/R025479/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 03/2018 
End 03/2023
 
Description EU Horizon 2020
Amount € 900,000 (EUR)
Organisation European Commission 
Sector Public
Country European Union (EU)
Start 01/2015 
End 12/2017
 
Description Hazardous Scene Assessment
Amount £78,500 (GBP)
Organisation Defence Science & Technology Laboratory (DSTL) 
Department Centre for Defence Enterprise
Sector Public
Country United Kingdom
Start 02/2017 
End 06/2017
 
Description Horizon 2020
Amount € 7,000,000 (EUR)
Organisation European Commission 
Sector Public
Country European Union (EU)
Start 01/2015 
End 12/2017
 
Description Human-Robot Collaboration in RoboStar
Amount £150,000 (GBP)
Organisation Thales Group 
Sector Private
Country France
Start 09/2021 
End 09/2025
 
Description Mini Centre for Doctoral Training. Albert: Autonomous Robotic Systems for Laboratory Experiments
Amount £1,000,000 (GBP)
Organisation University of York 
Sector Academic/University
Country United Kingdom
Start 03/2023 
End 12/2027
 
Description Newton Mobility Grant
Amount £12,000 (GBP)
Organisation The Royal Society 
Sector Charity/Non Profit
Country United Kingdom
Start 12/2015 
End 11/2017
 
Description Newton Research Collaboration Programme
Amount £23,374 (GBP)
Funding ID NRCP1617/6/164 
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 01/2017 
End 12/2017
 
Description Newton Research Collaboration Programme
Amount £23,105 (GBP)
Funding ID NRCP1617/5/68 
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 07/2016 
End 10/2017
 
Description RAEng Brazil 1
Amount £24,000 (GBP)
Funding ID NRCP1617/5/68 
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 05/2016 
End 07/2017
 
Description RAEng Brazil 2
Amount £24,000 (GBP)
Funding ID NRCP1617/6/164 
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 01/2017 
End 01/2018
 
Description Regional Engagement Awards
Amount £75,000 (GBP)
Funding ID REA1920\3\20 
Organisation Royal Academy of Engineering 
Sector Charity/Non Profit
Country United Kingdom
Start 01/2020 
End 12/2023
 
Description Robotic Safe Adaptation In unprecedented Situations
Amount € 6,883,233 (EUR)
Funding ID Grant agreement ID: 101133807 
Organisation European Commission H2020 
Sector Public
Country Belgium
Start 01/2024 
End 12/2027
 
Description TSB Open Call
Amount £22,000 (GBP)
Organisation Innovate UK 
Sector Public
Country United Kingdom
Start 03/2016 
End 03/2017
 
Description UKRI Trustworthy Autonomous Systems Node in Resilience
Amount £3,063,678 (GBP)
Funding ID EP/V026747/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 11/2020 
End 04/2024
 
Description UKRI Trustworthy Autonomous Systems Node in Verifiability
Amount £2,923,652 (GBP)
Funding ID EP/V026801/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 11/2020 
End 04/2021
 
Description Aarhus University Centre for Digital Twins 
Organisation Aarhus University
Department School of Engineering
Country Denmark 
Sector Academic/University 
PI Contribution Research collaboration with Professor Peter Gorm Larsen at Aarhus University's Centre for Digital Twins. Appointment as Adjunct Professor with support for activities, including regular visits. Appointment of Larsen as Visiting Professor at York.
Collaborator Contribution Collaboration on research papers and research proposals. Joint supervision of students at Aarhus.
Impact Collaboration with Cláudio Gomes on a paper: Uncertainty quantification and runtime monitoring using environment-aware digital twins. Paper accepted for ISoLA conference 2020, but delayed to 2021 because of pandemic.
Start Year 2019
 
Description Adjunct Professorship, Southwest University, Chongqing, China 
Organisation Southwest University
Country China 
Sector Academic/University 
PI Contribution Collaboration on a joint research project on human-cyber-physical systems. Appointment as Adjunct professor at Southwest University. Supervision of joint research students at Southwest University. Personal research fund for JCPW at Southwest University. Collaboration on the verification of neural networks.
Collaborator Contribution Joint research papers and research proposals. Proposed joint research laboratory. Joint direction of FM4AI research programme.
Impact Published a paper: Hengjun Zhao, Xia Zeng, Taolue Chen, Zhiming Liu, Jim Woodcock: Learning Safe Neural Network Controllers with Barrier Certificates. SETTA 2020: 177-185
Start Year 2019
 
Description Applicable Formal Methods 
Organisation Aarhus University
Country Denmark 
Sector Academic/University 
PI Contribution Expertise in theory and practice of formal methods.
Collaborator Contribution Expertise in theory and practice of formal methods.
Impact Publications: 1. Mario Gleirscher, Simon Foster, Jim Woodcock: New Opportunities for Integrated Formal Methods. ACM Comput. Surv. 52(6): 117:1-117:36 (2020) 2. Mario Gleirscher, Jaco van de Pol, Jim Woodcock: A Manifesto for Applicable Formal Methods. CoRR abs/2112.12758 (2021) 3. Mario Gleirscher, Jaco van de Pol, Jim Woodcock: Proceedings First Workshop on Applicable Formal Methods, AppFM@FM 2021, virtual, 23rd November 2021. EPTCS 349, 2021 Workshop: First Workshop on Applicable Formal Methods, AppFM@FM 2021
Start Year 2020
 
Description Applicable Formal Methods 
Organisation University of Bremen
Country Germany 
Sector Academic/University 
PI Contribution Expertise in theory and practice of formal methods.
Collaborator Contribution Expertise in theory and practice of formal methods.
Impact Publications: 1. Mario Gleirscher, Simon Foster, Jim Woodcock: New Opportunities for Integrated Formal Methods. ACM Comput. Surv. 52(6): 117:1-117:36 (2020) 2. Mario Gleirscher, Jaco van de Pol, Jim Woodcock: A Manifesto for Applicable Formal Methods. CoRR abs/2112.12758 (2021) 3. Mario Gleirscher, Jaco van de Pol, Jim Woodcock: Proceedings First Workshop on Applicable Formal Methods, AppFM@FM 2021, virtual, 23rd November 2021. EPTCS 349, 2021 Workshop: First Workshop on Applicable Formal Methods, AppFM@FM 2021
Start Year 2020
 
Description Butterfield TCD UTP 
Organisation Trinity College Dublin
Department School of Computer Science and Statistics
Country Ireland 
Sector Academic/University 
PI Contribution I have been collaborating with Andrew Butterfield since 2002 on Unifying Theories of Programming (UTP) and the formal semantics of of real-time, hybrid, and probabilistic systems. We meet regularly (at least twice a year) and have published 10 joint papers (five journal and five refereed conference papers). I have made contributions in foundations of UTP (including donating extensive course materials) and in applications to systems of systems and robotic and autonomous systems.
Collaborator Contribution Andrew Butterfield at TCD has made contributions to understanding hardware/software co-design and real-time and probabilistic systems. He contributed a strong background in functional programming.
Impact Outputs: DOIs: 10.1007/978-3-319-47166-2_26 10.1016/j.scico.2008.09.014 10.1109/TASE.2009.57 10.1109/ICECCS.2008.35 10.1109/ICECCS.2007.23 10.1007/978-3-540-73210-5_5 10.1016/j.entcs.2006.04.026 10.1007/s10009-004-0181-6 10.1016/S1571-0661(04)80821-1 10.1016/S1571-0661(04)80762-X The collaboration is multi-disciplinary, involving computer science and electronic engineering.
 
Description CSP-based testing 
Organisation University of Bremen
Country Germany 
Sector Academic/University 
PI Contribution Expertise in CSP and its semantics
Collaborator Contribution Expertise on testing and automation
Impact J. Peleska, W. l. Huang, and A. L. C. Cavalcanti. Finite complete suites for CSP refinement testing. Science of Computer Programming, 179:1 -- 23, 2019. A. L. C. Cavalcanti, W.-L. Huang, J. Peleska, and J. C. P. Woodcock. CSP and Kripke Structures. In M. Leucker, C. Rueda, and F. D. Valencia, editors, Theoretical Aspects of Computing, pages 505--523. Springer, 2015.
Start Year 2015
 
Description Chemical Agent Detection 
Organisation Ulster University
Department Faculty of Life and Health Sciences
Country United Kingdom 
Sector Academic/University 
PI Contribution Development of a hardware demonstrator of a neural network based control system for chemical agent detection. Using the tools developed in RoboCalc we will explore the limits of what is possible to model with respect to a complex controller based on neural networks.
Collaborator Contribution They are experts in the development of hardware based neural networks.
Impact Funded grant from the CDE (phase 1 development of prototype)
Start Year 2016
 
Description Circus foundations and Isabelle/UTP 
Organisation Galois, Inc.
Country United States 
Sector Private 
PI Contribution This is a collaboration that has just started. We are going to provide expertise on the techniques.
Collaborator Contribution They are taking a lead to mechanise the techniques and apply them on Rigorous Digital Engineering.
Impact Development of theories and techniques, and their application to industrial case studies.
Start Year 2022
 
Description Collaboration on RoboSim language: semantics, verification, examples, tools. 
Organisation Federal University of Pernambuco
Country Brazil 
Sector Academic/University 
PI Contribution Training on robotics
Collaborator Contribution Partnership in the design and implementation of RoboSim
Impact Joint papers.
Start Year 2017
 
Description Collaboration on RoboWorld language: syntax, semantics, examples, tools 
Organisation UFPE
Country Brazil 
Sector Academic/University 
PI Contribution Expertise on robotics, the RoboChart language, and CyPhyCircus semantics
Collaborator Contribution Expertise on controlled natural languages, partnership in the design and implementation of RoboWorld
Impact Development of the RoboWorld language and a prototype tool for it, journal paper under review
Start Year 2019
 
Description Collaboration on Social, Legal, Ethical, Empathetic and Cultural (SLEEC) aspects of autonomous agents with the TAS Resilience Node 
Organisation University of York
Department Department of Computer Science
Country United Kingdom 
Sector Academic/University 
PI Contribution Expertise on the formal semantics of RoboChart and definition of conformance relation for checking satisfaction of design models against SLEEC rules.
Collaborator Contribution Expertise on Social, Legal, Ethical, Empathetic and Cultural (SLEEC) aspects for Autonomous Agents.
Impact Joint work under way and contributing to the writing of joint journal paper.
Start Year 2022
 
Description Collaboration on Social, Legal, Ethical, Empathetic, and Cultural Requirements for Service Robots 
Organisation University of Toronto
Country Canada 
Sector Academic/University 
PI Contribution Expertise on modelling, formalisation, validation, and verification of these requirements.
Collaborator Contribution Alternative mathematical models, and validation approaches.
Impact We have published two papers together and given a tutorial.
Start Year 2023
 
Description Collaboration with Fudan University 
Organisation Fudan University
Country China 
Sector Academic/University 
PI Contribution We have begun very early work on the application of the tools developed in the project to case studies being undertaken by researchers at Fudan. We visited once in 2018 (Sept) and plan to visit again later this year and work with MSc and PhD students in more detail. We have provided insight into the use of the tools and suggested possible application areas.
Collaborator Contribution They have provided outline case studies for us to examine, so that we can focus work for 2019.
Impact At this stage, outcomes are limited, expect the development of a plan for 2019 work.
Start Year 2018
 
Description Collaboration with Univesity of Agder, NMBU, and ABB Robotics 
Organisation ABB Group
Country Switzerland 
Sector Private 
PI Contribution We have provided insight into the use of tools and techniques for modelling and verification of a High-Voltage Controller (HVC) robotic system.
Collaborator Contribution They have brought a case study of a High-Voltage Controller, which is at the core of a painting robot developed at ABB Robotics. They have used RoboChart and RoboTool to model the software controller and perform formal verification of safety properties. Work is ongoing towards verification including a model of the physical robotic platform.
Impact * A case study, including two models. * Improvements to the implementation of the semantics of RoboChart for model-checking. * A publication: Murray Y, Anisi D, Sirevåg M, Ribeiro P, Hagag R. (2020). Safety Assurance of a High Voltage Controller for an Industrial Robotic System. Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings. (pp. 45-63).
Start Year 2020
 
Description Collaboration with Univesity of Agder, NMBU, and ABB Robotics 
Organisation Norwegian University of Life Sciences (NMBU)
Country Norway 
Sector Academic/University 
PI Contribution We have provided insight into the use of tools and techniques for modelling and verification of a High-Voltage Controller (HVC) robotic system.
Collaborator Contribution They have brought a case study of a High-Voltage Controller, which is at the core of a painting robot developed at ABB Robotics. They have used RoboChart and RoboTool to model the software controller and perform formal verification of safety properties. Work is ongoing towards verification including a model of the physical robotic platform.
Impact * A case study, including two models. * Improvements to the implementation of the semantics of RoboChart for model-checking. * A publication: Murray Y, Anisi D, Sirevåg M, Ribeiro P, Hagag R. (2020). Safety Assurance of a High Voltage Controller for an Industrial Robotic System. Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings. (pp. 45-63).
Start Year 2020
 
Description Collaboration with Univesity of Agder, NMBU, and ABB Robotics 
Organisation University of Agder
Country Norway 
Sector Academic/University 
PI Contribution We have provided insight into the use of tools and techniques for modelling and verification of a High-Voltage Controller (HVC) robotic system.
Collaborator Contribution They have brought a case study of a High-Voltage Controller, which is at the core of a painting robot developed at ABB Robotics. They have used RoboChart and RoboTool to model the software controller and perform formal verification of safety properties. Work is ongoing towards verification including a model of the physical robotic platform.
Impact * A case study, including two models. * Improvements to the implementation of the semantics of RoboChart for model-checking. * A publication: Murray Y, Anisi D, Sirevåg M, Ribeiro P, Hagag R. (2020). Safety Assurance of a High Voltage Controller for an Industrial Robotic System. Formal Methods: Foundations and Applications - 23rd Brazilian Symposium, SBMF 2020, Ouro Preto, Brazil, November 25-27, 2020, Proceedings. (pp. 45-63).
Start Year 2020
 
Description D'Souza IISc Verification 
Organisation Indian Institute of Science Bangalore
Department Department of Computer Science and Automation
Country India 
Sector Academic/University 
PI Contribution My team contributed expertise in formal specification, refinement, and verification of software. We contributed to the verification of FreeRTOS, the popular open-source real-time operating system. We helped our Indian colleagues develop expertise in Z and Z/Eves and helped them apply it to verification problems.
Collaborator Contribution Colleagues at the Indian Institute of Science and General Motors India helped us to understand the FreeRTOS code and extract suitable abstract specifications of aspects of its behaviour.
Impact Three projects funded by the British Council, the Royal Academy of Engineering, and the Robert Bosch Centre for Cyber-Physical Systems (total value £175k). One conference paper (10.1007/978-3-319-25423-4_11). One journal paper (10.1007/s00165-014-0308-9). Two Phd theses: Sumesh Divakaran: A Refinement-Based Methodology for Verifying Abstract Data Type Implementations (IISc, 2015). Shu Cheng: Formally modelling and verifying the FreeRTOS real-time operating system (York, 2014).
Start Year 2010
 
Description D-RisQ 
Organisation D-RisQ
Country United Kingdom 
Sector Private 
PI Contribution Development of a case study, the alpha algorithm, using the techniques for modelling and simulation developed in the project. As a result of a our joint efforts, we have evolved both our reserch and their product.
Collaborator Contribution Development of a case study, the alpha algorithm, using the techniques for modelling and simulation used in their company. As a result of a our joint efforts, we evolved both our reserch and their product.
Impact * A case study, including two models, several simulations. * Improvements to D-RisQ's tools. * Improvements to our notation to deal with collections of robots. * Improvements to our simulation approach.
Start Year 2016
 
Description Distinguished Visiting Professor 
Organisation Fudan University
Country China 
Sector Academic/University 
PI Contribution New appointment for Prof Timmis to explore further applications of the technology in intelligent robotics.
Collaborator Contribution Initial discussions on case studies and possible research student supervision.
Impact None as yes.
Start Year 2021
 
Description ECNU - Shanghai UPPAL 
Organisation East China Normal University (ECNU)
Country China 
Sector Academic/University 
PI Contribution We bring in expertise in robotics, simulation, and model-based engineering, including the design and semantics of RoboSim.
Collaborator Contribution They bring in expertise in timed and probabilistic model checking, and verification using bisimulation.
Impact A tool under development and a paper in preparation.
Start Year 2020
 
Description FMI Step Negotiation 
Organisation Aarhus University
Department Department of Engineering
Country Denmark 
Sector Academic/University 
PI Contribution Meetings to discuss how to verify co-simulation algorithms with algebraic loops and adaptive steps. Our insight is to use angelic nondeterminism to specify backtracking. This requires new theories of state-rich, reactive, angelic nondeterminism.
Collaborator Contribution Aarhus are the problem owners. They contributed expertise in the functional mock-up interface (FMI) and the problems of adaptive co-simulaiton.
Impact Paper: Simon Thrane Hansen, Cláudio Gomes, Maurizio Palmieri, Casper Thule, Jaco van de Pol, Jim Woodcock: Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps. FMICS 2021: 3-20 DOI: 10.1007/978-3-030-85248-1_1
Start Year 2021
 
Description FitzLarsen CPS EU 
Organisation Aarhus University
Department School of Engineering
Country Denmark 
Sector Academic/University 
PI Contribution Our collaboration has involved two major EU projects. My research team brought expertise in modelling, formal semantics, mechanised proof, and model checking.
Collaborator Contribution Newcastle made contribution in modelling and methods. Aarhus made contributions in tool building.
Impact Also see http://www.compass-research.eu/. Outputs: Funding for two large EU projects. Publications: 8 conference papers, 4 journal papers, 2 book chapters. Citations: > 600 in total. Multi-disciplinary collaboration covering systems, software, hardware, control theory, and electronics.
Start Year 2009
 
Description Formal methods in security 
Organisation Aarhus University
Department Department of Engineering
Country Denmark 
Sector Academic/University 
PI Contribution Expertise in formal methods in security
Collaborator Contribution Expertise in formal methods in security
Impact Technical report: Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter Würtz Vinther Tran-Jørgensen, Jim Woodcock: A Survey of Practical Formal Methods for Security. CoRR abs/2109.01362 (2021) Accepted for publication in ACM Formal Aspects of Computing.
Start Year 2020
 
Description Formal methods in security 
Organisation University of Surrey
Department Department of Computing
Country United Kingdom 
Sector Academic/University 
PI Contribution Expertise in formal methods in security
Collaborator Contribution Expertise in formal methods in security
Impact Technical report: Tomas Kulik, Brijesh Dongol, Peter Gorm Larsen, Hugo Daniel Macedo, Steve Schneider, Peter Würtz Vinther Tran-Jørgensen, Jim Woodcock: A Survey of Practical Formal Methods for Security. CoRR abs/2109.01362 (2021) Accepted for publication in ACM Formal Aspects of Computing.
Start Year 2020
 
Description Hybrid Model Checking - CORA 
Organisation Technical University of Munich
Country Germany 
Sector Academic/University 
PI Contribution We bring expertise in robotics, the design and semantics of the RoboWorld language, and the CyPhyCircus hybrid process algebra.
Collaborator Contribution They bring expertise in hybrid model checking, and development on the CORA hybrid model checker to support our models.
Impact Models in CORA based on the semantics of RoboWorld, testing and enhancement of the CORA hybrid model checker.
Start Year 2022
 
Description INTO-CPS collaboration 
Organisation Aarhus University
Country Denmark 
Sector Academic/University 
PI Contribution Collaboration between EU Horizon 2020 project and RoboCalc. RoboCalc contributed to a new work item in INTO-CPS on adding new languages and tools to the INTO-CPS toolchain. Specifically, the probabilistic version of RoboChart and its translation to the PRISM model checker.
Collaborator Contribution Work carried out by investigator funded by INTO-CPS project.
Impact Draft publications.
Start Year 2017
 
Description INTO-CPS collaboration 
Organisation Newcastle University
Country United Kingdom 
Sector Academic/University 
PI Contribution Collaboration between EU Horizon 2020 project and RoboCalc. RoboCalc contributed to a new work item in INTO-CPS on adding new languages and tools to the INTO-CPS toolchain. Specifically, the probabilistic version of RoboChart and its translation to the PRISM model checker.
Collaborator Contribution Work carried out by investigator funded by INTO-CPS project.
Impact Draft publications.
Start Year 2017
 
Description Interaction trees 
Organisation Seoul National University
Country Korea, Republic of 
Sector Academic/University 
PI Contribution Expertise in UTP semantics and Isabelle.
Collaborator Contribution Expertise in interaction trees.
Impact Technical report: Simon Foster, Chung-Kil Hur, Jim Woodcock: Formally Verified Simulations of State-Rich Processes using Interaction Trees in Isabelle/HOL. CoRR abs/2105.05133 (2021) Implementation in Isabelle/UTP. Contributions to undergraduate and postgraduate teaching: PROF module.
Start Year 2021
 
Description Lectures on Probabilistic Robotics 
Organisation Aarhus University
Department Department of Engineering
Country Denmark 
Sector Academic/University 
PI Contribution Outreach and dissemination through research-based teaching.
Collaborator Contribution Providing an audience of engineering students.
Impact Lecture not4s, slides, and videos.
Start Year 2022
 
Description Lectures on Programming and Modelling 
Organisation Aarhus University
Department Department of Engineering
Country Denmark 
Sector Academic/University 
PI Contribution Research-based teaching.
Collaborator Contribution Provision of engineering student audience.
Impact Lecture notes, slides, and videos.
Start Year 2022
 
Description Mota UFPE 
Organisation Federal University of Pernambuco
Country Brazil 
Sector Academic/University 
PI Contribution Collaboration on probabilistic aspects of RoboChart language: semantics, examples, tools.
Collaborator Contribution Collaborative work on probabilistic RoboChart.
Impact Draft publications.
Start Year 2017
 
Description Partnership in the application of RoboChart 
Organisation Fudan University
Country China 
Sector Academic/University 
PI Contribution Training for use of RoboChart
Collaborator Contribution Explaining the potential collaborative research area of RoboChart
Impact No.
Start Year 2019
 
Description Reducing the Cyber Attack Surface 
Organisation Aarhus University
Department Department of Engineering
Country Denmark 
Sector Academic/University 
PI Contribution Survey of verifiable computation techniques. Experiments. Proposal for future work.
Collaborator Contribution Contributions to report.
Impact Reports. Draft publications.
Start Year 2022
 
Description Reducing the Cyber Attack Surface 
Organisation D-RisQ
Country United Kingdom 
Sector Private 
PI Contribution Survey of verifiable computation techniques. Experiments. Proposal for future work.
Collaborator Contribution Contributions to report.
Impact Reports. Draft publications.
Start Year 2022
 
Description Reducing the Cyber Attack Surface 
Organisation Defence Science & Technology Laboratory (DSTL)
Country United Kingdom 
Sector Public 
PI Contribution Survey of verifiable computation techniques. Experiments. Proposal for future work.
Collaborator Contribution Contributions to report.
Impact Reports. Draft publications.
Start Year 2022
 
Description Royal Academy of Engineering Industry Fellowship 
Organisation Thales Group
Department Thales UK Limited
Country United Kingdom 
Sector Private 
PI Contribution Co-supervision of student and industry fellows.
Collaborator Contribution We are developing a technique to model and verify mobile and autonomous robots with humans in the loop.
Impact Multi-disciplinary: Engineering and Psychology.
Start Year 2021
 
Description Simomics Robotics 
Organisation Simomics Ltd
Country United Kingdom 
Sector Private 
PI Contribution Expertise on modelling and verification of robotics systems.
Collaborator Contribution Tools for modelling auditing and assurance cases.
Impact A tool is under development.
Start Year 2020
 
Description Sound simulation of robotic applications 
Organisation Federal University of Pernambuco
Country Brazil 
Sector Academic/University 
PI Contribution We have brought to them expertise on the results and approaches to modelling and verifying robotic applications, and developing simulations.
Collaborator Contribution They have brought in experience in model-based software engineering, compositional verification, testing, and probabilistic model checking. They have employed a research assistant to to work on the project and collaborate with our group. Together, we are developing a domain-specific language for modelling simulations. The language has a formal semantics under development. They are in charge of developing tool support for this language, and developing tool support for probabilistic reasoning.
Impact Tools are under development and papers are submitted.
Start Year 2017
 
Description Testing from Circus with Mealy Machines 
Organisation Universidade de São Paulo
Department Institute of Mathematical and Computer Sciences (ICMC)
Country Brazil 
Sector Academic/University 
PI Contribution Expertise on model-based testing based on process algebras and resfinement.
Collaborator Contribution Expertise on testing based on Mealy machines.
Impact Joint papers
Start Year 2015
 
Description Transport Systems Catapult - Autonomous Vehicle 
Organisation Transport Systems Catapult
Country United Kingdom 
Sector Private 
PI Contribution Modelling, analysis and simulation of the control system of an autonomous vehicle. Using the tools and techniques developed in RoboCalc, we will explore the limits of what is possible to model, analyse and simulate with respect to a complex realistic controller where safety concerns are of utmost importance.
Collaborator Contribution They are experts in the development of transport systems. As well as their expertise, they will provides us with documentation and source code regarding the specific case study.
Impact *A case study, the largest RoboChart model to date. *Preliminary analysis results based on model checking technology. *The model and results will be published in a book, which is currently at the final stages of publication.
Start Year 2017
 
Description Uncertainty 
Organisation King's College London
Country United Kingdom 
Sector Academic/University 
PI Contribution Discussions between the University of York and King's College London on a future research proposal.
Collaborator Contribution Discussions between the University of York and King's College London on a future research proposal.
Impact Draft research proposal.
Start Year 2022
 
Description Uncertainty in autonomous systems 
Organisation King's College London
Country United Kingdom 
Sector Academic/University 
PI Contribution Definition of probabilistic semantics in UTP and implementation in Isabelle/UTP.
Collaborator Contribution Problems, examples, case studies.
Impact No outputs yet.
Start Year 2021
 
Description Uncertainty in autonomous systems 
Organisation University of York
Country United Kingdom 
Sector Academic/University 
PI Contribution Definition of probabilistic semantics in UTP and implementation in Isabelle/UTP.
Collaborator Contribution Problems, examples, case studies.
Impact No outputs yet.
Start Year 2021
 
Description VSR collaborations 
Organisation Microsoft Research
Department Microsoft Research Cambridge
Country United Kingdom 
Sector Private 
PI Contribution Organising the UK's contribution to the Verified Software Initiative.
Collaborator Contribution Suppliers of case studies, verification technology, challenge project prizes, organisers of workshops.
Impact Collection of verification case studies for experimentation by the verification community.
Start Year 2006
 
Description VSR collaborations 
Organisation Praxis Systems Ltd
Country United Kingdom 
Sector Private 
PI Contribution Organising the UK's contribution to the Verified Software Initiative.
Collaborator Contribution Suppliers of case studies, verification technology, challenge project prizes, organisers of workshops.
Impact Collection of verification case studies for experimentation by the verification community.
Start Year 2006
 
Description Verification and uncertainties in self-integrating systems 
Organisation Aarhus University
Department Department of Engineering
Country Denmark 
Sector Academic/University 
PI Contribution Expertise in unification of semantics and verification techniques.
Collaborator Contribution Expertise in self-integrating systems and uncertainty.
Impact Publication: Lukas Esterle, Barry Porter, Jim Woodcock: Verification and Uncertainties in Self-integrating System. ACSOS-C 2021: 220-225 DOI: 10.1109/ACSOS-C52956.2021.00050
Start Year 2021
 
Description Verification and uncertainties in self-integrating systems 
Organisation Lancaster University
Department School of Computing and Communications
Country United Kingdom 
Sector Academic/University 
PI Contribution Expertise in unification of semantics and verification techniques.
Collaborator Contribution Expertise in self-integrating systems and uncertainty.
Impact Publication: Lukas Esterle, Barry Porter, Jim Woodcock: Verification and Uncertainties in Self-integrating System. ACSOS-C 2021: 220-225 DOI: 10.1109/ACSOS-C52956.2021.00050
Start Year 2021
 
Description Verification grand challenge history 
Organisation Altran
Country United Kingdom 
Sector Private 
PI Contribution History of the Verified Software Initiative
Collaborator Contribution Personal accounts of contributions to the Verified Software Initiative.
Impact Publication: Jim Woodcock, Janet Barnes, Rod Chapman, Simon Foster, Thomas Santen: Verification in the Grand Challenge. Theories of Programming 2021: 125-156 DOI: 10.1145/3477355.3477363
Start Year 2021
 
Description Verification grand challenge history 
Organisation Technical University Berlin
Country Germany 
Sector Academic/University 
PI Contribution History of the Verified Software Initiative
Collaborator Contribution Personal accounts of contributions to the Verified Software Initiative.
Impact Publication: Jim Woodcock, Janet Barnes, Rod Chapman, Simon Foster, Thomas Santen: Verification in the Grand Challenge. Theories of Programming 2021: 125-156 DOI: 10.1145/3477355.3477363
Start Year 2021
 
Description bangalore-2018 
Organisation Indian Institute of Science Bangalore
Country India 
Sector Academic/University 
PI Contribution Newton grant from RAEng held by IIIT-B. Contributions on refinement of simulink models.
Collaborator Contribution Research in refinement of simulink models.
Impact Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. RAMiCS 2018: 205-224 Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. CoRR abs/1806.02101 (2018)
Start Year 2018
 
Description butterfield-tcd-march-2018 
Organisation Trinity College Dublin
Department Trinity Biomedical Sciences Institute
Country Ireland 
Sector Hospitals 
PI Contribution Research discussions at TCD.
Collaborator Contribution Research discussions.
Impact Discussions on future research collaborations.
Start Year 2018
 
Description chongqing-2-2018 
Organisation Southwest University
Country China 
Sector Academic/University 
PI Contribution Royal Society China Cost Share Programme
Collaborator Contribution Research contributions.
Impact None yet.
Start Year 2018
 
Description chongqing2018 
Organisation Southwest University
Country China 
Sector Academic/University 
PI Contribution Royal Society China Cost Share Programme.
Collaborator Contribution Rsearch contributions.
Impact No outputs yet.
Start Year 2018
 
Description digit-2018 
Organisation Aarhus University
Department Aarhus Institute of Advanced Studies
Country Denmark 
Sector Academic/University 
PI Contribution Planning for future collaboration.
Collaborator Contribution Research exchanges.
Impact Proposal to Grundfos Foundation.
Start Year 2018
 
Description peleska-testing-2018 
Organisation University of Bremen
Country Germany 
Sector Academic/University 
PI Contribution Rsearch discussions.
Collaborator Contribution Rsearch discussions.
Impact Research proposals.
Start Year 2018
 
Title Automated Verification of Reactive and Concurrent Programs by Calculation, supporting material 
Description Abstract Event-driven reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber physical systems and autonomous robots, and so verification support for them is highly desirable. We present a verification strategy for concurrent and reactive programs, with a large or infinite state space, utilising algebraic laws for reactive relations. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, which is supported by Kleene algebra, and parallel composition, which allows flexible specification of various concurrency schemes. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He's Unifying Theories of Programming (UTP) semantic framework, which provides soundness guarantees, and practical verification support. Isabelle Formalisation This archive accompanies the JLAMP journal submission, "Automated Verification of Reactive and Concurrent Programs by Calculation". All of the Isabelle/HOL theories needed to support the theorems developed in this paper are included, and also the dependencies from the Archive of Formal Proofs (AFP). This development depends on Isabelle/2019 (from https://isabelle.in.tum.de/). In order to view the theories, you first need to make Isabelle aware of the Isabelle/UTP directly. You can either do this by adding a reference to its absolute path in the ROOTS file of your Isabelle installation, or else by invoking Isabelle on the command line with a command such as:
isabelle jedit -d /path/to/isabelle/utp -l UTP-Circus
The main heap images of interest are UTP, UTP-Reactive-Designs, and UTP-Circus. The first time you invoke the command, you may need to wait for a while to allow Isabelle to build the heap image. You can find the reactive buffer example under tutorial/utp_csp_buffer.thy and further reactive program examples in tutorial/utp_csp_ex.thy. The theories for reactive designs and stateful failure reactive designs may be found under theories/{rea_designs, sf_rdes}. 
Type Of Technology Software 
Year Produced 2019 
Open Source License? Yes  
URL https://zenodo.org/record/3541079
 
Title Isabelle/UTP 
Description Hoare and He's Unifying Theories of Programming is a framework for construction of denotational semantic meta-models for a variety of programming languages based on an alphabetised relational calculus. Isabelle/UTP is an implementation of their framework based in Isabelle/HOL. It can be used to formalise semantic building blocks for programming language paradigms (based on UTP theories), prove algebraic laws of programming, and then use these laws to construct program verification tools. 
Type Of Technology Software 
Year Produced 2023 
Open Source License? Yes  
Impact The software was applied to verification of a fan control unit controller, and a railway signalling system as part of the previous INTO-CPS EU project. It is currently being applied to model autonomous robots. 
URL https://isabelle-utp.york.ac.uk/
 
Title RoboToool 
Description RoboTool provides a graphical editor for models written in a domain-specific language for robotics, RoboChart. RoboTool also generates automatically mathematical definitions that capture the behaviour of the RoboChart model, and is integrated with a model checker. This is a tool that is able to use the mathematical definitions to prove properties like freedom of deadlock and livelock. Instead of testing the system or the model, a model checker explores exhaustively all the states of the model to ensure that the property of interest is satisfied in all states. Using the definition generated by RoboTool, we can also prove specific properties of a robotic system, like impossibility of ignoring a particular event in given circumstances, for example. If, however, the property does not hold, a model checker provides a counterexample. RoboTool is provided as a set of Eclipse plugins implemented using the Xtext 1 and Sirius 2 frameworks. Xtext automatically generates plugins that implement a parser, and provides mechanisms for the implementation of validators, type checkers, and code generators, for instance. Sirius supports the definition of graphical representations, and produces a plugin for construction and visualisation of models. The model checker used by RoboTool is FDR4. 
Type Of Technology Software 
Year Produced 2016 
Open Source License? Yes  
Impact General interest in academia and industry in using the results of our project. 
URL https://www.cs.york.ac.uk/circus/RoboCalc/robotool/
 
Title SLEECVAL: Specification and Validation of Normative Rules for Autonomous Agents 
Description Growing range of applications use autonomous agents such as AI and robotic systems to perform tasks deemed dangerous, tedious or costly for humans. To truly succeed with these tasks, the autonomous agents must perform them without violating the social, legal, ethical, empathetic, and cultural (SLEEC) norms of their users and operators. We introduce SLEECVAL, a tool for specification and validation of rules that reflect these SLEEC norms. Our tool supports the specification of SLEEC rules in a DSL. we co-defined with the help of ethicists, lawyers and stakeholders from health and social care, and uses the CSP refinement checker FDR4 to identify redundant and conflicting rules in a SLEEC specification. We illustrate the use of SLEECVAL for two case studies: an assistive dressing robot, and a firefighting drone. 
Type Of Technology New/Improved Technique/Technology 
Year Produced 2023 
Impact SLEECVAL enables specification and validation of non-functional rules with the focus on SLEEC (social, legal, ethical, empathetic, and cultural) principles for autonomous agents. To best of our knowledge, our language and tool are novel in their support to formalise and validate normative rules that address SLEEC concerns. Our vision is to provide an automated framework to specify, validate, and verify that agents follow rules, reporting redundancy and conflicts. 
URL https://sleec.github.io
 
Description 18th International Summer School on Trustworthy Software 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Ana Cavalcanti and Jim Woodcock led courses on Software Engineering for Robotics and Isabelle/HOL as part of the 18th International Summer School on Trustworthy Software organised by the School of Software Engineering of East China Normal University. RoboStar colleagues James Baxter , Gustavo Carvalho , Alvaro Miyazawa , Pedro Ribeiro and Matt Windsor delivered practicals and seminars.
Year(s) Of Engagement Activity 2022
 
Description 18th International Summer School on Trustworthy Software 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact In August 2022, we delivered a series of lectures via video link to graduate students at East China Normal University (ECNU) in Shanghai, China as part of the 18th International Summer School on Trustworthy Software organised by the Software Engineering Institute at the ECNU.
Year(s) Of Engagement Activity 2022
URL https://seisummerschool.github.io/2022/
 
Description 1st Belt & Road Conference on Science and Engineering Exchange, Chongqing 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Keynote presentation. National and regional TV interviews. Discussions with international, national, and regional science China policymakers. Interview on national TV (CCTV) and local TV (Congqing CQTV).
Year(s) Of Engagement Activity 2023
 
Description A demonstration of probabilistic modelling and verification in RoboTool to researcher in University of Agder 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Demonstrated the probabilistic modelling and verification in RoboTool through PRISM to colleagues in the University of Agder on February 26th 2020 via Skype. Audiences include researcher and master students. At the same time, Pedro demonstrated RoboTool in general.

To prepare for this demo, an online resource (see https://robostar.cs.york.ac.uk/prob_case_studies/probabilistic_verification_tutorial/index.html) was created.
Year(s) Of Engagement Activity 2020
 
Description ASE 2023 - Tutorial on Social, Legal, Ethical, Empathetic and Cultural Requirements: from Elicitation to Verification 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact On the 15 of September, colleagues Sinem Getir Yaman, Ana Cavalcanti, Radu Calinescu, and Beverly Townsend, from the UKRI TAS Node on Resilience, will be holding a tutorial on "Social, Legal, Ethical, Empathetic and Cultural Requirements: from Elicitation to Verification" at the 38th IEEE/ACM International Conference on Automated Software Engineering (ASE 2023).
Year(s) Of Engagement Activity 2023
 
Description ASEP professional development course. 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Professional development course on assurance and proof.
Year(s) Of Engagement Activity 2023
URL https://www.cs.york.ac.uk/professional/assured-software-engineering-proof/
 
Description Aarhus Lectures on probabilistic robotics 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Undergraduate students
Results and Impact I delivered a series of six lectures on probabilistic robotic control to undergraduates in engineering at Aarhus University. The lectures were prepared as curated videos with lecture notes.
Year(s) Of Engagement Activity 2021
 
Description Are you Talking to your Autonomous Car? (Maybe you should!) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Public/other audiences
Results and Impact Ana Cavalcanti featured as a speaker in the latest Living with AI Podcast of the TAS Hub.
Year(s) Of Engagement Activity 2022
URL https://www.buzzsprout.com/1447474/11041372
 
Description BCS FACS Evening Seminar 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact The BCS Specialist Group for practitioners in Formal Aspects of Computing Science has members drawn from both industry and academia. It acts as a bridge between the two communities, helping British industry to stay in the forefront of formal computer techniques, and British academics to maintain the applicability of their research.

It arranges informal seminars to encourage technology transfer throughout the year: about four a year.
Year(s) Of Engagement Activity 2016
URL http://www.bcs.org/content/ConWebDoc/56123
 
Description Bristol BAME STEM seminar on Software Engineering for Robotics 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact Webinar on my career journey and research interests to a wide range of scientists and Science Administrators for wider dissemination.
Year(s) Of Engagement Activity 2023
 
Description CUP journal. Research Directions: Cyber-Physical Systems 
Form Of Engagement Activity A magazine, newsletter or online publication
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Development and launch of a new journal.
Year(s) Of Engagement Activity 2022,2023
URL https://www.cambridge.org/core/journals/research-directions-cyber-physical-systems
 
Description China Lectures on probabilistic robotics 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Undergraduate students
Results and Impact I delivered a series of six lectures on probabilistic robotic control.
Year(s) Of Engagement Activity 2021
 
Description Course at School of Software, Northwest Polytechnical University, Xi'an, China 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact I contributed to a tutorial on the use of the RoboChart notation for formal verification of robotic applications.
Year(s) Of Engagement Activity 2021
 
Description CyPhyAssure Spring School 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Participation in Spring School on the assurance of cyber-physical systems.
Year(s) Of Engagement Activity 2019
URL https://www.cs.york.ac.uk/circus/CyPhyAssure/school/
 
Description DIGIT Advisory Board 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Participation in the advisory board of the center for digital twins at Aarhus University,
Year(s) Of Engagement Activity 2018
 
Description Dagstuhl seminar on Integrated Rigorous Analysis in Cyber-Physical Systems Engineering 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Week-long seminar of world experts on cyber-physical systems. Seminar report. Publication.
Year(s) Of Engagement Activity 2023
URL https://www.dagstuhl.de/en/seminars/seminar-calendar/seminar-details/23041
 
Description ECNU summer school 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact In August 2022, we delivered a series of lectures via video link to graduate students at East China Normal University (ECNU) in Shanghai, China as part of a summer school on Trustworthy Systems.
Year(s) Of Engagement Activity 2022
URL https://seisummerschool.github.io/2022/
 
Description FM 2019 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Talks and discussions with international colleagues.
Year(s) Of Engagement Activity 2019
 
Description Formal Methods Symposium 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Papers were presented, talks were given, and specialist group meetings were organised.
Year(s) Of Engagement Activity 2023
URL https://www.fmeurope.org/symposia/
 
Description Formally Verified Animation for RoboChart using Interaction Trees at ICFEM2022 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact A talk about "Formally Verified Animation for RoboChart using Interaction Trees" given at the conference ICFEM2022
Year(s) Of Engagement Activity 2022
URL http://maude.ucm.es/ICFEM22/index.html
 
Description Guest lecture on model-based software engineering for robotics 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Undergraduate students
Results and Impact I delivered a two-part guest lecture on "Model-based software engineering for robotics", as part of the undegratuate module "Model-Driven Engineering" (Computer Science, University of York), based on outputs of my research on sound model-transformation from RoboChart to RoboSim.
Year(s) Of Engagement Activity 2022
 
Description Huawei Research Forum 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Presentation on formal methods for assurance of security-related software in Huawei 5G products.
Year(s) Of Engagement Activity 2019
 
Description Huawei Research Symposium 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Presentation of my research agenda to Huawei engineers. I gave advice on future research policy for their company.
Year(s) Of Engagement Activity 2019
 
Description ICTAC: International Colloquium on Theoretical Aspects of Computing, Lima, Peru 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Presented research to internatiomnal audience.
Year(s) Of Engagement Activity 2023
URL https://ictac2023.compsust.utec.edu.pe/
 
Description IFIP WG 2.3 Programming Methodology 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Hosted meeting of IFIP WG 2.3 on Programming Methodology. Organised scientific and social agenda, chaired the meeting, and gave an extended scientific talk. I involved my doctoral students and research assistants in the meeting.
Year(s) Of Engagement Activity 2019
URL https://ifip-tc2-wg23.paluno.uni-due.de/?page_id=455
 
Description Integrated Rigorous Analysis in Cyber-Physical Systems Engineering (Dagstuhl Seminar 23041) 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact International seminar (one week) on the integrated rigorous analysis of cyber-physical systems. Presentations, discussions, published summary.
Year(s) Of Engagement Activity 2023
URL https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.1.155
 
Description Invited Lecture at University of Sheffield 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Postgraduate students
Results and Impact the research at a level accessible to young researchers.
Year(s) Of Engagement Activity 2021
 
Description Invited course at the School of Software, Northwest Polytechnical University, Xi'an, China 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact This is a school organised by a consortium of Chinese universities that provides younger researchers with the background on the state of the art in the area of software engineering. The course sparked questions and discussion afterwards.
Year(s) Of Engagement Activity 2021
 
Description Invited course at the School of the International Colloquium on Theoretical Aspects of Computing 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact This is a school associated with an international conference that provides younger researchers with the background on the state of the art in the area of theoretical aspects of computing. The course sparked questions and discussion afterwards, and led to a publication.
Year(s) Of Engagement Activity 2021
URL https://ictac2021.github.io/school.html
 
Description Invited lecture University of Leicester 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Postgraduate students
Results and Impact Present the research at a level accessible to young researchers.
Year(s) Of Engagement Activity 2018
URL https://www2.le.ac.uk/departments/informatics/news/researchevents/external
 
Description Invited lecture at the International School on Formal Methods and Theoretical Informatics (ETMF) 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Undergraduate students
Results and Impact This is a school associated with an international conference that provides younger students with the background to follow the paper presentations in the conference. The course sparked questions and discussion afterwards and during the main event.
Year(s) Of Engagement Activity 2021
URL https://sites.google.com/computacao.ufcg.edu.br/sbmf2021/program
 
Description Invited talk at BCS on How can we define operational requirements in robotics? 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact On the 9th of May, Ana Cavalcanti lead a seminar on "How can we define operational requirements in robotics?" together with colleagues James Baxter and Gustavo Carvalho . The event was organised by BCS London Central Branch and BCS North London branch, for IT professionals.
Year(s) Of Engagement Activity 2022
 
Description Invited talk at HIS (High- Integrity Software) 2019 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Industry/Business
Results and Impact Now in its sixth year, the mission of the High Integrity Software conference is to share challenges, best practice and experience between software engineering practitioners. The conference features talks from industrial and academic specialists which disseminate experience and knowledge of important techniques and methods that are applicable across industry sectors. I have presented the technology developed in our researcher. It sparked questions and discussion, afterwards, and later contacts with a view to exchange ideas and collaborate.
Year(s) Of Engagement Activity 2019
URL https://www.his-2017.co.uk/
 
Description Invited talk at the IROS2021 Workshop on Standardised Software Frameworks for Robotics in Nuclear 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact This was a workshop organised by colleagues in industry. It gave us the opportunity to present our results and spark discussion with practitioners who are themselves interested in technological developments in the area.
Year(s) Of Engagement Activity 2021
URL https://ukaeaevents.com/2021-ieee-rsj/
 
Description Invited talk at the York & North Yorkshire LEP Skills Conference 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Professional Practitioners
Results and Impact Ana Cavalcanti delivered an invited talk at the York & North Yorkshire LEP Skills Conference on "Software Engineering for Robotics in Industry 4.0". The talk can be watched on YouTube
Year(s) Of Engagement Activity 2022
URL https://www.ynylep.com/news/festival-of-engagement/event/id/2220
 
Description Invited talk on probabilistic robotics 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Undergraduate students
Results and Impact I delivered an invited talk at a summer school in Shanghai.
Year(s) Of Engagement Activity 2021
 
Description Isabelle/UTP Tutorials in Southwest University, Chongqing, China 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact This tutorial lasted for two afternoons, covers three main topics: functional programming with Isabelle/HOL, imperative programming with Isabelle/UTP, and reactive programming with Isabelle/UTP. The material of the tutorial is very much based on the tutorial that Dr. Simon Foster gave during CyphyAssure Spring School.
Year(s) Of Engagement Activity 2019
URL http://computer.swu.edu.cn/s/computer/kxyj2xsky/20190509/3706486.html
 
Description LMS Computer Science Colloquium talk - Verification of control software for robots that learn 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact On the 1st of December, Professor Ana Cavalcanti gave a talk at the LMS Computer Science Colloquium titled "Verification of control software for robots that learn", explaining the approach adopted in RoboStar to verify intelligent systems.
Year(s) Of Engagement Activity 2023
URL https://www.lms.ac.uk/events/lms-computer-science-colloquium-2023
 
Description Newton Institue Workshop 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact I gave a talk about the impact of verification technology on practical application.
Year(s) Of Engagement Activity 2019
 
Description Open Day 
Form Of Engagement Activity Participation in an open day or visit at my research institution
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Schools
Results and Impact Presentation of robotic applications developed using our techniques.
Year(s) Of Engagement Activity 2016
 
Description Opening of Aarhus Centre for Digital Twins 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Keynote talk on research direction at the opening of the Centre for Digital Twins at Aarhus University.
Year(s) Of Engagement Activity 2019
URL https://digit.au.dk/research-projects/centre-for-digital-twins/
 
Description Organisation of RoboStar and YorRobots Industry Exhibition 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact On 11-12 October YorRobots and RoboStar hosted an Industry Exhibition. There were talks and demonstrations by RoboStar colleagues and from YorRobots, The Institute for Safe Autonomy, Adelard, AgroIntelli, BAE, Bristol Robotics Lab, ClearSy, Chemspeed Technologies, Connected Places, LabMan, LDRA, DRis-Q, Dyson, RobotCenter, ShadowRobot, Thales and VSI.
Year(s) Of Engagement Activity 2022
URL https://robostar.cs.york.ac.uk/events/yrie2022/
 
Description Organised and Participated in Computer Science Postgraduate welcome Research Showcase and Panel 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Postgraduate students
Results and Impact Organised a postgraduate welcome week event to showcase existing Computer Science research within the University of York, alongside chairing a panel of existing students sharing research experiences. The research showcase was a series of short presentations. This has sparked interest from new postgraduate researchers in my own research.
Year(s) Of Engagement Activity 2022
 
Description Present "Engineering Robotic Swarms" in the Pint of Science at York 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Public/other audiences
Results and Impact Presented at Pivni of York from 7:30 PM - 9:30 PM on May 22, 2019, with James Baxter and Richard Redpath (Jon Timmis).

Abstract
Robots are becoming part of our everyday lives, from making cars and cleaning the house to assisting with surgery and exploring areas too dangerous for humans to enter. But can we trust them to be safe? In this talk, we look at ways that Mathematics, Computer Science, and Software Engineering can play a part to ensure that robots behave in the way we expect them to. We discuss groups of robots working together and the problems and solutions related to working with them. We show the power of these techniques lives in action. Using frogs. And the audience. What could possibly go wrong?
Year(s) Of Engagement Activity 2019
URL https://pintofscience.co.uk/event/-blurred-lines-boundaries-between-man-and-machine
 
Description Presentation at IFIP WG 2.3 Meeting 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Our work on modelling for robotics was presented to the members of the Working Group on Programming Methodology, as well as to the invited observers. The goal of the presentation was to disseminate our work and receive feedback on current research.
Year(s) Of Engagement Activity 2019
 
Description Presentation at IFIP WG 2.3 Meeting 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Recent work on priorities, related to the formal semantics of RoboChart and RoboSim, was presented to the Working Group on Programming Methodology, as well as to the invited speakers. The goal of the presentation was to disseminate our work and receive feedback on ongoing research.
Year(s) Of Engagement Activity 2019
 
Description Presentation at Pint of Science Festival 2018 in York 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Public/other audiences
Results and Impact The Pint of Science festival is run every year bringing researchers to local pubs to present their work to the general public. In this talk, we motivated our work using robotic demonstrators and presented our main results. The talk was followed by a number of interesting questions from the public.
Year(s) Of Engagement Activity 2018
URL https://pintofscience.co.uk/event/are-you-sure-you-are-safe
 
Description Presentation at Pint of Science Festival 2019 in York 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Public/other audiences
Results and Impact The Pint of Science festival is run every year bringing researchers to local pubs to present their work to the general public. In this talk, we presented our work on modelling and verifying the robot software, with particular focus on application of our approach to robot swarms. The talk was followed by a number of interesting questions from the public.
Year(s) Of Engagement Activity 2019
URL https://pintofscience.co.uk/event/-blurred-lines-boundaries-between-man-and-machine
 
Description Presentation at RoboStar and YorRobots Industry Exhibition 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact On 11th October 2022, I gave a talk and presented a poster on the semantics of the RoboWorld language and the use of hybrid model checking to check the semantics.
Year(s) Of Engagement Activity 2022
URL https://robostar.cs.york.ac.uk/events/yrie2022/
 
Description Presentation at meeting with BSI 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact I presented an overview of the RoboCalc and RoboTest projects at a meeting with British Standards Institution and the Assuring Autonomy International Programme at York, which discussed standards in AI, robotics and autonomy.
Year(s) Of Engagement Activity 2018
 
Description Presentation of project to Thales 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Industry/Business
Results and Impact Presentation of the project to consider possible collaboration. Six colleagues from Thales attended.
Year(s) Of Engagement Activity 2019
 
Description Presentations at RoboStar and YorRobots Industry Exhibition 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact On 11-12 October, I gave three talks on the work developed in the RoboCalc and RoboTest projects at an Industry Exhibition.
Year(s) Of Engagement Activity 2022
URL https://robostar.cs.york.ac.uk/events/yrie2022/
 
Description Presented "Modelling and verification of probabilistic behaviour of robotic applications" during a two-day workshop to communicate with our visitors (Prof. Zhiming Liu and his team) from Southwest University 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Agenda:
1. Overview of RoboChart;
2. Background of reactive modules, PRISM and MDP;
3. How to transform models from RoboChart to PRISM;
4. Verification support through PRISM and the assertion language in RoboTool;
5. Example and performance.

Date: Jul 23, 2019 9:30 AM - 11:00 AM
Location: University of York

This talk was presented during a two-day workshop to communicate with our visitors (Prof. Zhiming Liu and his team) from Southwest University, Chongqing, China.
Year(s) Of Engagement Activity 2019
 
Description Probabilistic modelling and verification using RoboChart and PRISM at MODELS2022 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Invited as a Journal-first paper by International Journal on Software and Systems Modeling (SoSyM) to present our work at MODELS 2022 on 27th October 2022
Year(s) Of Engagement Activity 2022
URL https://conf.researchr.org/home/models-2022
 
Description Public lecture 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Public/other audiences
Results and Impact Short lecture on the interaction between biology and robotics and the need to develop safe robotic systems that can interact with humans and the environment.
Year(s) Of Engagement Activity 2017
 
Description Public talk as part of YorkTalks 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Public/other audiences
Results and Impact About 300 people attended an event in the university The talks sparked questions and discussion afterwards, with the public, and with other colleagues involved in the event. The aim of the overall event is to showcase the very best of the University's research across seven research themes in order to exemplify our commitment to research excellence which forms a key component of the University Strategy and the Research Strategy.
Year(s) Of Engagement Activity 2020
URL https://www.york.ac.uk/research/events/yorktalks/
 
Description RAMiCS 2021 conference 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact A talk about "Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving" in the conference RAMiCS 2021 on November 4, 2021.
Year(s) Of Engagement Activity 2021
URL https://ramics19.lis-lab.fr/
 
Description REF 2021 Subpanel 11 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Policymakers/politicians
Results and Impact Computer Science subpanel member for Research Evaluation Framework 2021.
Year(s) Of Engagement Activity 2021,2022
 
Description Research visit to Aarhus University 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Discussion on current research collaboration.
Year(s) Of Engagement Activity 2023
 
Description RoboCheck 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact About 40 research students attended a school organised in York. Afterwards, several students showed interest in our project and our interests. We have discussed ideas for further work.
Year(s) Of Engagement Activity 2015
URL https://www.cs.york.ac.uk/circus/RoboCalc-event/
 
Description RoboSoft: software engineering for robotics 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Professional Practitioners
Results and Impact RoboSoft was a two-day event that will brought together researchers working on software engineering for robotics, developers working on the next generation of robotic systems in various areas of application, and regulation authorities interested in safety of robotic systems. RoboSoft provides a platform to establish software engineering for robotics as an important discipline in computer science and electronic engineering. The objective was to establish a common understanding of the challenges that need to be addressed to ensure that results are relevant to industrial practice and regulation. The group organised the whole event and gave three presentations.
Year(s) Of Engagement Activity 2019
URL https://www.raeng.org.uk/events/events-programme/2019/november/robosoft-software-engineering-for-rob...
 
Description RoboStar and YorRobots Industry Exhibition 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact On 11th October 2022, I was a speaker in two talks on "RoboSim: software models for sound simulation" and "Trustworthy Autonomous Systems Node on Verifiability", and co-presented (as well as co-authored) three posters during the exhibition: (1) "RoboSim: software models for sound simulation"; (2) "Autonomous Fire-Fighting UAV" ; (3) "Safety Assurance of an Industrial Robotic Control System Using Hardware/Software Co-Verification" related to my on-going collaboration with the University of Agder (Norwary), Norwegian University of Life Sciences and ABB Robotics.
Year(s) Of Engagement Activity 2022
URL https://robostar.cs.york.ac.uk/events/yrie2022/
 
Description RoboStar test generation presented at Huawei Grenoble 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Ana Cavalcanti presented an invited lecture to Huawei Grenoble on 25 October, 2023. The invitation came from the Huawei Fermat Lab, and the audience included colleagues online from China and Hong Kong. Ana presented RoboStar work on automatic test generation.
Year(s) Of Engagement Activity 2023
 
Description Robotics and Software Engineering Conference (RSE'23), KCL 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Presented research work on robotics and uncertainty.
Year(s) Of Engagement Activity 2023
URL https://rsemeeting.github.io/rse2023/
 
Description Royal Academy of Engineering GEEP (Graduate Engineering Engagement Programmme) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact On the 29th of January, 2024, Ana Cavalcanti met with a group of more than 60 students in a webinar session, where they discussed the RoboStar views for Software Engineering of AI-enabled systems. GEEP is an award-winning programmme run in partnership with employers to increase the transition of engineering graduates from diverse backgrounds into engineering employment.
Year(s) Of Engagement Activity 2024
URL https://raeng.org.uk/programmes-and-prizes/programmes/uk-grants-and-prizes/support-for-education/gra...
 
Description Royal Academy of Engineering Research Forum 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Other audiences
Results and Impact The Research Forum is a highlight of the Academy's activities. It showcases the world-class engineering research funded through the Academy's wide range of programmes. The event consists of a mix of keynote talks from current awardees and alumni. Awardees from across the portfolio of Academy's research schemes will also exhibit posters and demos throughout the day. The project was presented in a keynote talk.
Year(s) Of Engagement Activity 2019
URL https://www.raeng.org.uk/events/events-programme/2019/november/research-forum
 
Description School visit (London) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Schools
Results and Impact Prof Timmis gave a series of talks to years 10 and 12 students at St, Michael's College, Burmonsea, London. The talks were around the use of robotics and their limitations and issues around safety. In addition, he talked about careers in the subject area.
Year(s) Of Engagement Activity 2019
 
Description Spring School on Engineering Trustworthy Software Systems 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Spring School on Engineering Trustworthy Software Systems (SETSS), held in April, 2016, at Southwest University in Chongqing, China. The school was aimed at post-graduate students, researchers, academics, and industrial engineers who are interested in the theory and practice of methods and tools for the design and programming of
trustworthy software systems.
Year(s) Of Engagement Activity 2016
 
Description Summer School 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Second Summer School in 2023 at ECNU.
Year(s) Of Engagement Activity 2023
 
Description Summer School lecturess 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Lectures delivered at a Summer School at ECNU in Shanghai.
Year(s) Of Engagement Activity 2022
 
Description Symposium for Marie-Claude Gaudel 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact I gave a talk on software engineering for robotic control.
Year(s) Of Engagement Activity 2019
 
Description Talk at Huawei engineering conference 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact A talk was given at Huawei's engineering conference on advance software engineering practice.
Year(s) Of Engagement Activity 2022
 
Description Talk at Verification Future Meeting 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Industry/Business
Results and Impact I gave an invited talk at this industry meeting.
Year(s) Of Engagement Activity 2019
URL https://www.testandverification.com/conferences/verification-futures/vf2019
 
Description Tutorial at 25th Brazilian Symposium on Formal Methods 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact On 8 December 2022, Alvaro Miyazawa lead a tutorial on "RoboStar and RoboTool: Software Engineering for Robotics using Formal Methods". The tutorial was part of the 25th Brazilian Symposium on Formal Methods.
Year(s) Of Engagement Activity 2022
URL https://sites.google.com/dcomp.ufs.br/sbmf2022/keynotes-tutorials?authuser=0
 
Description UK-RAS Network RoboTalk Podcast 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Public/other audiences
Results and Impact Podcast organised by the UK-RAS network to describe research and projects of my group.
Year(s) Of Engagement Activity 2022
URL https://www.ukras.org.uk/news/robot-talk-episode-thirty-out-now
 
Description UTP and BDI agents 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Study participants or study members
Results and Impact Preliminary work to establish future research collaborations.
Year(s) Of Engagement Activity 2023
 
Description Verifiability Talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Study participants or study members
Results and Impact Presentation on A Unifying Framework for Verifiability as part of the seminar series for the EPSRC Trusted Autonomous Systems Verifiability Node.
Year(s) Of Engagement Activity 2021
URL https://www.youtube.com/watch?v=iUv5i9NYgNU
 
Description Verifiability Talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Study participants or study members
Results and Impact Presentation of the RoboStar approach to Software Engineering for Robotics, including modelling and testing
Year(s) Of Engagement Activity 2021
 
Description Video on cyber-physical systems 
Form Of Engagement Activity A broadcast e.g. TV/radio/film/podcast (other than news/press)
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Video promoting research in cyber-physical systems.
Year(s) Of Engagement Activity 2023
URL https://www.cambridge.org/core/journals/research-directions-cyber-physical-systems
 
Description Visit by Jan Pekeska 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Discussions on research collaboration.
Year(s) Of Engagement Activity 2018
 
Description Visit by Ziming Liiu 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Visit to discuss long-term research collaboration.
Year(s) Of Engagement Activity 2018
 
Description Visit from Southwest University 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Visit from a delegation from Southwest University, Chongqing, China.
Year(s) Of Engagement Activity 2019
 
Description Visit from TCD Ireland 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Visit from colleagues from Trinity College Dublin. Contributions on probabilistic semantic for robotics.
Year(s) Of Engagement Activity 2018,2019
 
Description Visit ti Aarhus University 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Visit to exchange research ideas.
Year(s) Of Engagement Activity 2018
 
Description Visit to Aarhus University 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Research visit to AArhus University for continuing collaboration
Year(s) Of Engagement Activity 2023
 
Description Visit to Chongqing 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Workshop on formal methods for human-cyber-=physical systems. I gave talks on software engineering for robotics.
Year(s) Of Engagement Activity 2019
 
Description Visit to Chongqing 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Visit Southwest University to give lectures and direct doctoral students.
Year(s) Of Engagement Activity 2019
 
Description Visit to IISc 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Presentation of research work. Exchange of research ideas for future research proposals.
Year(s) Of Engagement Activity 2018
 
Description Visit to IISc Bangalore 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Workshop at IISc funded by Royal Academy of Engineering. Discussed work on formal verification of operating system real-time kernels.
Year(s) Of Engagement Activity 2019
 
Description Visit to Malardalen University 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact External examining of a doctoral student. Interaction with academic colleagues on research directions. Interaction with industry colleagues on research directions.
Year(s) Of Engagement Activity 2019
 
Description Visit to Southwest University 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Study participants or study members
Results and Impact Visit to exchange ideas.
Year(s) Of Engagement Activity 2018
 
Description Visit to Southwest University, Chongqing, China. Visit to Tong Ji University, Shanghai. 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Other audiences
Results and Impact Presentation of research and planning for future funding of international research programme.
Year(s) Of Engagement Activity 2023
 
Description Visit to VSI Bremen 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Visit to VSI in Bremen to discuss future research collaboration, especially in verification of learning-enabled systems.
Year(s) Of Engagement Activity 2023
 
Description White Rose Retreat on Robotics 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Study participants or study members
Results and Impact Discussed future collaborative in robotics.
Year(s) Of Engagement Activity 2019
 
Description Workshop for Advisory Board and additional representatives from academia and industry 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Industry/Business
Results and Impact Meeting of the Advisory Board to report on our results from RoboCalc and kick-off RoboTest. The joint meeting of the projects was very positive. There was a lot of discussion and good feedback. Further colleagues from industry asked to join the Advisory Board afterwards.
Year(s) Of Engagement Activity 2018
 
Description Workshop for academics and industrialists in Pernambuco, Brazil 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact A workshop organised by the Federal University of Pernambuco, Brazil, to present our project and their own experiences in robotics, ranging from support technology development, participation in competitions, to actual deployment of systems. In attendance were academics and students from the local Centre of Informatics, other departments interested in applications, and the local industry. RoboCalc, its results and its goals, were extensively discussed.
Year(s) Of Engagement Activity 2017
 
Description Workshop for industry 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Industry/Business
Results and Impact Workshop involving key industry players in robotics. Discussions influenced our work and created opportunities for further collaboration.
Year(s) Of Engagement Activity 2015
URL https://www.cs.york.ac.uk/circus/RoboCalc/2015/11/Kick-off-meeting
 
Description YorRobots Exhibition 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact More than 100 researchers and industrialists working in the area of robotics attended a one-day exhibition involving talks, posters, and demonstrations of work carried out in the University of York and in industry around the UK. There was plenty of opportunity for discussion and engagement. I have presented the results and the vision for RoboCalc and RoboTest, and beyond.
Year(s) Of Engagement Activity 2020
URL https://www.york.ac.uk/yorrobots/news-events/yorrobots-events/2020/exhibition-2020/
 
Description YorRobots Industry Exhibition 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Two talks and two posters.
Year(s) Of Engagement Activity 2022
 
Description YorRobots launch event 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Other audiences
Results and Impact This was an afternoon event organised for scientists across nine departments of the university: Computer Science, Electronic Engineering, Physics, Chemistry, Environment, Music, Law, Philosophy, and Mathematics. We presented our work, and as a result created a network of scientists in robotics at York.
Year(s) Of Engagement Activity 2019
URL https://www.york.ac.uk/yorrobots/
 
Description women+@DCS seminar on Software Engineering for Robotics 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Postgraduate students
Results and Impact This activity supports the effort at the University of Sheffield to engage women in science.
Year(s) Of Engagement Activity 2021
URL https://sites.google.com/sheffield.ac.uk/womendcs/