UKRI Trustworthy Autonomous Systems Node in Verifiability

Lead Research Organisation: King's College London
Department Name: Informatics

Abstract

Autonomous systems promise to improve our lives;
driverless trains and robotic cleaners are examples of autonomous systems that are already among us and
work well within confined environments.
It is time we work to ensure developers can design trustworthy autonomous systems for dynamic environments and
provide evidence of their trustworthiness.

Due to the complexity of autonomous systems, typically involving AI
components, low-level hardware control, and sophisticated interactions with
humans and the uncertain environment, evidence of any nature requires efforts from a
variety of disciplines. To tackle this challenge, we gathered consortium of
experts on AI, robotics, human-computer interaction, systems and software
engineering, and testing. Together, we will establish the foundations and
techniques for verification of properties of autonomous systems to inform
designs, provide evidence of key properties, and guide monitoring
after deployment.

Currently, verifiability is hampered by several issues: difficulties to
understand how evidence provided by techniques that focus on individual
aspects of a system (control engineering, AI, or human
interaction, for example) compose to provide evidence for the system as
whole; difficulties of communication between stakeholders that use different
languages and practices in their disciplines; difficulties in dealing with
advanced concepts in AI, control and hardware design, software for critical
systems; and others. As a consequence, autonomous systems are often developed
using advanced engineering techniques, but outdated approaches to
verification.

We propose a creative programme of work that will enable fundamental changes
to the current state of the art and of practice. We will define a
mathematical framework that enables a common understanding of the diverse
practices and concepts involved in verification of autonomy. Our framework
will provide the mathematical underpinning, required by any engineering
effort, to accommodate the notations used by the various disciplines. With
this common understanding, we will justify translations between languages,
compositions of artefacts (engineering models, tests, simulations, and so on)
defined in different languages, and system-level inferences from
verifications of components.

With such a rich foundation and wealth of results, we will
transform the state of practice. Currently, developers build systems from
scratch, or reusing components without any evidence of their
operational conditions. Resulting systems are deployed in constrained
conditions (reduced speed or contained environment, for example) or offered
for deployment at the user's own risk. Instead, we envisage the future
availability of a store of verified autonomous systems and components.

In such a future, in the store, users will find not just system
implementations, but also evidence of their operational conditions and
expected behaviour (engineering models, mathematical results, tests, and so
on). When a developer checks in a product, the store will require all these
artefacts, described in well understood languages, and will automatically
verify the evidence of trustworthiness. Developers will also be able to check
in components for other developers; equally, they will be accompanied by
evidence required to permit confidence in their use.

In this changed world, users will buy applications with clear guarantees of
their operational requirements and profile. Users will also be able to ask
for verification of adequacy for customised platforms and environment, for
example. Verification is no longer an issue.

Working with the EPSRC TAS Hub and other nodes, and our extensive range of
academic and industrial partners, we will collaborate to ensure that the
notations, verification techniques, and properties, that we consider,
contribute to our common agenda to bring autonomy to our everyday lives.

Organisations

 
Description The Verifiability Node was established in November 2020 with the goal of establishing a unifying framework for holisting and system-level verification of autonomous systems. The Node has already achieved several significant results. These include identifying language and notational abstractions across various domains, establishing a unifying semantic framework, and defining algorithmic abstractions, refinements, and translations across various sub-domains in the unifying framework. A detailed description of these results can be found in the Node Annual Report (available at: https://verifiability.org/annual-reports/) as well as the Node outputs (https://verifiability.org/publications/). We highlight below a few of these results.

- Designed languages to define properties for verification, operational requirements, and mappings between platform-independent and platform models;

- Formalised heterogeneous semantics, using and implemented this in the theorem proving framework;

- Designed a compositional framework for heterogeneous specifications; we took a bottom-up approach by developing a composition of various models for the assistive dressing case study; - Accommodated variability in learning and analysing behavioural models of autonomous systems;

- Used AI (in particular reinforcement learning) to increase efficiency of verification strategies;

- Developed causal analysis techniques to analyse the behaviour of robotic and autonomous systems and applied them to assitive education for neurodiverse children;

- Developed runtime monitoring algorithms to search for anomalies in autonomous system; and

- Formally verified human-level rules for autonomous systems and ethical concerns in autonomous systems.
Exploitation Route Were the award's original objectives met?

Too early to say (the award is still active)

Please expand on why the award's original objectives were not met, if you wish.

Are there any further details of the outcomes of this funding on the web? If so, please provide the most relevant URL(s) here.

https://verifiability.org/annual-reports/
We used our early findings to build a community, engage with our community, industrial partners and policy makers. In the context of policy engagement, we have produced two policy papers in response to the U.K. government requests. More specifically, we have responded to consultations about connected and automated mobility (CAM) in the UK and data protection. In the former, we give evidence about the impact of CAM in the UK's future, the country's preparedness and how it fares compared to other countries. In the latter, we emphasise the importance of research in explainable AI and also in facilitation and transparency of data sharing.
We have also engaged with the International Transport Federation and Organisation for Economic Co-operation and Developmen in defining policies for automated vehicle functions.
We have taken part in the development of the cross-sector safety assessment framework led by the Department for Transport; the results are to be presented on 21 March 2023 in Westminster.
We have also taken part in workshops co-organised by UKRI on Ethical Funding for AI as well as a Workshop on a Funding Scheme at the Intersection of Quantum Computing and ICT. With our expertise in verification and autonomous systems, we are also involved in a range of standards activities, both at the national and international levels. At the national level, Fisher is a member of the British Standards Institution AMT/10 committee on Robotics, which feeds into the ISO TC299 international standards activity on Robotics. Particularly relevant is involvement in the updating and revision of the BS8611 "Guide to the ethical design and application of robots and robotic systems", due to be published in 2022. Internationally, Dennis and Fisher are both involved in the "IEEE Global Initiative on Ethics of Autonomous and Intelligent Systems" and specifically the new international standards being developed on "Transparency of Autonomous Systems" (IEEE P7001; Dennis) and "Failsafe Design of Autonomous Systems" (IEEE P7009; Fisher).
Sectors Education

Manufacturing

including Industrial Biotechology

Transport
URL https://verifiability.org/
 
Description The challenge addressed by the UKRI TAS Verifiability Node is a holistic and inclusive framework for verification of autonomous systems that allows stakeholders across many different domains to express and verify their concerns and requirements. To complement the technical and scientific activities in the Node, we organised and participated in a number of activities, created a large interdisciplinary community, and provided input to both academic, policy, and public engagements. A selection of some of these impactful activities is given below: • We organised 55 instances of the Verifiability Talk series to date, open to public. Most talks are featured on the Verifiability YouTube Channel, with more than 120 subscribers and more than 3000 views. • We co-authored the report led by WMG Warwick on Cross-Domain Safety Assurance for Automated Transport Systems, and participated in the panel discussion at the report launch event. • We delivered a keynote and participated in the ITF Roundtable on Policy and Regulation for Autonomous Vehicles held at OECD in Paris. • We have contributed and continue to contribute to the National RAS Regulations, Standards and Ethics Committee. • We hosted a delegation of about 60 delegates from the Wallenberg AI, Autonomous Systems and Software Program (WASP) in Sweden; organised a number of mutual visits for faculty members and PhD students within WASP. Additionally, we have contributed to the development of effective means for assited education for neurodiverse children by means of explaining the behaviour of assistive robots using our Verifiability platform (in the contex of the Kaspar Explains pump-priming project). We are currently working on our assistive-dressing robotic case study which will further provide impact in the healthcare domain.
Sector Education,Healthcare,Transport
Impact Types Policy & public services
 
Description Co-Chair of IEEE Technical Committee on the Verificaiton of Autonomous Systems
Geographic Reach Multiple continents/international 
Policy Influence Type Membership of a guideline committee
URL https://www.ieee-ras.org/verification-of-autonomous-systems
 
Description Co-Chair of the UKRI TAS Hub EDI Working Group and continuous ongoing participation to formal UKRI TAS Hub Workshop events to shape TAS EDI guiding principles and TAS Hub EDI Framework
Geographic Reach National 
Policy Influence Type Membership of a guideline committee
Impact The impact is ongoing as the UKRI TAS Hub gets updated. It aims to support the key guiding principles defined for the design and development of Trustworthy Autonomous Systems; one of the ways this has impacted research practices so far is e.g. by embedding in e.g. research funding proposals practice explicit highlights and discussion on how EDI is achieved and safeguarded within the proposed research. This will lead to a longer-term impact of delivering more respectful, inclusive and diverse innovations that will be experienced equally by everyone.
URL https://www.tas.ac.uk/wp-content/uploads/2021/10/TAS-EDI-Framework-v3.pdf
 
Description Connected tech: smart or sinister? A call for evidence from Department for Digital, Culture, Media & Sport
Geographic Reach National 
Policy Influence Type Contribution to a national consultation/review
URL https://kclpure.kcl.ac.uk/portal/files/175710766/Call_for_evidence_Parliamentary_inquiry_FINAL_2.pdf
 
Description Data: a new direction: A call for evidence from Department for Digital, Culture, Media & Sport
Geographic Reach National 
Policy Influence Type Contribution to a national consultation/review
URL https://kclpure.kcl.ac.uk/portal/files/163776916/Data_a_new_direction_FINAL_APPROVED.pdf
 
Description Input to the Government's Cyber-Physical Infrastructure consultation
Geographic Reach National 
Policy Influence Type Contribution to a national consultation/review
URL https://www.gov.uk/government/consultations/enabling-a-national-cyber-physical-infrastructure-to-cat...
 
Description Membership of IEEE P7009 Standards committee on "Failsafe Design of Autonomous Systems"
Geographic Reach Multiple continents/international 
Policy Influence Type Membership of a guideline committee
URL https://standards.ieee.org/project/7009.html
 
Description Ongoing contribution to: Cross-Domain Safety Assurance for Automated Transport Systems
Geographic Reach National 
Policy Influence Type Contribution to a national consultation/review
URL https://warwick.ac.uk/fac/sci/wmg/research/research-areas/verification-and-validation/ukriflf/2023cr...
 
Description Sandpit: trustworthiness of autonomous robotic systems for national security and defence
Geographic Reach National 
Policy Influence Type Contribution to a national consultation/review
URL https://www.ukri.org/opportunity/sandpit-trustworthiness-of-autonomous-robotic-systems-for-national-...
 
Description Secondment to DSIT
Geographic Reach National 
Policy Influence Type Contribution to a national consultation/review
 
Description The future of connected and automated mobility in the UK - a call for evidence from the Department for Business, Energy & Industrial Strategy and the Centre for Connected and Autonomous Vehicles
Geographic Reach National 
Policy Influence Type Contribution to a national consultation/review
URL https://eprints.soton.ac.uk/450228/
 
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 Advanced Manufacturing and productivity institute (AMPI)
Amount £21,000,000 (GBP)
Organisation Innovate UK 
Sector Public
Country United Kingdom
Start 03/2022 
End 02/2027
 
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 DASA Competition:Telexistence
Amount £80,000 (GBP)
Organisation Defence Science & Technology Laboratory (DSTL) 
Sector Public
Country United Kingdom
Start 02/2021 
End 10/2021
 
Description EMRP
Amount € 100,000 (EUR)
Funding ID NEW06-REG4(UoY) 
Organisation European Association of National Metrology Institutes (EURAMET) 
Sector Charity/Non Profit
Country Germany
Start 05/2014 
End 05/2015
 
Description EPSRC responsive mode
Amount £1,029,474 (GBP)
Funding ID EP/H017461/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 05/2010 
End 09/2015
 
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 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 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 Scalable Quantum Network Technologies: Collaborative R&D
Amount £1,972,000 (GBP)
Organisation Innovate UK 
Sector Public
Country United Kingdom
Start 03/2024 
End 10/2025
 
Description Seventh Framework Programme
Amount € 6,000,000 (EUR)
Funding ID 287829 
Organisation European Commission 
Sector Public
Country European Union (EU)
Start 09/2011 
End 09/2014
 
Description Verified Simulation for Large Quantum Systems (VSL-Q)
Amount £620,778 (GBP)
Funding ID EP/Y005244/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 05/2023 
End 03/2025
 
Title Benchmark models for evaluating the robustness of machine learning 
Description The dataset provides a list of models that come from common databases and can be used as a benchmark for robustness in ML algorithms 
Type Of Material Computer model/algorithm 
Year Produced 2023 
Provided To Others? Yes  
Impact We actively collaborate with different research partners on improving algorithms and their quality by using these specific models 
URL https://github.com/hdg7/ictai2023models
 
Title Dataset for Paper "Digital twin based testing for cyber-physical systems: A systematic literature review" 
Description An excel spreadsheet containing exported metadata collected during a systematic literature review on digital twin based testing for cyber-physical systems. 
Type Of Material Database/Collection of data 
Year Produced 2022 
Provided To Others? Yes  
URL https://figshare.shef.ac.uk/articles/dataset/Dataset_for_Paper_Digital_twin_based_testing_for_cyber-...
 
Title Dataset for Paper "Digital twin based testing for cyber-physical systems: A systematic literature review" 
Description An excel spreadsheet containing exported metadata collected during a systematic literature review on digital twin based testing for cyber-physical systems. 
Type Of Material Database/Collection of data 
Year Produced 2022 
Provided To Others? Yes  
URL https://figshare.shef.ac.uk/articles/dataset/Dataset_for_Paper_Digital_twin_based_testing_for_cyber-...
 
Title Verifiability Node Models for the Firefighting Drone and Robot-Assisted Dressing 
Description We publicly provide a wide spectrum of models developed at the Verifiability Node for our two main case studies: Firefighting Drone and Robot-Assisted Dressing. 
Type Of Material Computer model/algorithm 
Year Produced 2022 
Provided To Others? Yes  
Impact We actively collaborate with various research partners on these models and their verification; examples include collaboration with the Americal University of Sharjah, as well as the RoboStar and Resilience Node teams. 
URL https://github.com/hlsa/Verifiability-Node
 
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 CRADLE Prosperity Partnership 
Organisation Jacobs Engineering Group
Country United States 
Sector Private 
PI Contribution CRADLE Prosperity Partnership, funded by UKRI, Jacobs and University of Manchester is providing a route for our research to have impact on real robotic systems.
Collaborator Contribution Jacobs is a strong partner, providing engineering expertise, problem sets, and routes to impact.
Impact No outputs yet.
Start Year 2023
 
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 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 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 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 DORIAN: Doctor-centred Auditing of Healthcare AI With Testing of Fairness 
Organisation Johns Hopkins University
Country United States 
Sector Academic/University 
PI Contribution This collaboration aims to build trust in AI-aided diagnosis by engaging doctors' interest in the auditing process of AI tools. We will develop an audit tool and dashboard that will enable doctors to visualise their audits of AI systems.
Collaborator Contribution King's College London provides the MLighter tool,that will be the starting point for the project and will contribute to its development, evaluation, and research related outcomes, apart from coordinating the project. Johns Hopkins University will contribute to the design and development of the prototype of the auditing algorithms and the dashboard. University of Nottingham will contribute on the engagement with UK doctors. University of Texas at Austin will contribute on the engagement with USA doctors. University of Southampton will contribute on creating policies related to the evaluation and validation of AI.
Impact The collaboration started in March 2023. The main current output is the funding of 72460 pounds obtained by the team. This is a multidisciplinary collaboration involving: medicine, computer science and law.
Start Year 2023
 
Description DORIAN: Doctor-centred Auditing of Healthcare AI With Testing of Fairness 
Organisation King's College London
Country United Kingdom 
Sector Academic/University 
PI Contribution This collaboration aims to build trust in AI-aided diagnosis by engaging doctors' interest in the auditing process of AI tools. We will develop an audit tool and dashboard that will enable doctors to visualise their audits of AI systems.
Collaborator Contribution King's College London provides the MLighter tool,that will be the starting point for the project and will contribute to its development, evaluation, and research related outcomes, apart from coordinating the project. Johns Hopkins University will contribute to the design and development of the prototype of the auditing algorithms and the dashboard. University of Nottingham will contribute on the engagement with UK doctors. University of Texas at Austin will contribute on the engagement with USA doctors. University of Southampton will contribute on creating policies related to the evaluation and validation of AI.
Impact The collaboration started in March 2023. The main current output is the funding of 72460 pounds obtained by the team. This is a multidisciplinary collaboration involving: medicine, computer science and law.
Start Year 2023
 
Description DORIAN: Doctor-centred Auditing of Healthcare AI With Testing of Fairness 
Organisation University of Nottingham
Country United Kingdom 
Sector Academic/University 
PI Contribution This collaboration aims to build trust in AI-aided diagnosis by engaging doctors' interest in the auditing process of AI tools. We will develop an audit tool and dashboard that will enable doctors to visualise their audits of AI systems.
Collaborator Contribution King's College London provides the MLighter tool,that will be the starting point for the project and will contribute to its development, evaluation, and research related outcomes, apart from coordinating the project. Johns Hopkins University will contribute to the design and development of the prototype of the auditing algorithms and the dashboard. University of Nottingham will contribute on the engagement with UK doctors. University of Texas at Austin will contribute on the engagement with USA doctors. University of Southampton will contribute on creating policies related to the evaluation and validation of AI.
Impact The collaboration started in March 2023. The main current output is the funding of 72460 pounds obtained by the team. This is a multidisciplinary collaboration involving: medicine, computer science and law.
Start Year 2023
 
Description DORIAN: Doctor-centred Auditing of Healthcare AI With Testing of Fairness 
Organisation University of Southampton
Country United Kingdom 
Sector Academic/University 
PI Contribution This collaboration aims to build trust in AI-aided diagnosis by engaging doctors' interest in the auditing process of AI tools. We will develop an audit tool and dashboard that will enable doctors to visualise their audits of AI systems.
Collaborator Contribution King's College London provides the MLighter tool,that will be the starting point for the project and will contribute to its development, evaluation, and research related outcomes, apart from coordinating the project. Johns Hopkins University will contribute to the design and development of the prototype of the auditing algorithms and the dashboard. University of Nottingham will contribute on the engagement with UK doctors. University of Texas at Austin will contribute on the engagement with USA doctors. University of Southampton will contribute on creating policies related to the evaluation and validation of AI.
Impact The collaboration started in March 2023. The main current output is the funding of 72460 pounds obtained by the team. This is a multidisciplinary collaboration involving: medicine, computer science and law.
Start Year 2023
 
Description DORIAN: Doctor-centred Auditing of Healthcare AI With Testing of Fairness 
Organisation University of Texas at Austin
Country United States 
Sector Academic/University 
PI Contribution This collaboration aims to build trust in AI-aided diagnosis by engaging doctors' interest in the auditing process of AI tools. We will develop an audit tool and dashboard that will enable doctors to visualise their audits of AI systems.
Collaborator Contribution King's College London provides the MLighter tool,that will be the starting point for the project and will contribute to its development, evaluation, and research related outcomes, apart from coordinating the project. Johns Hopkins University will contribute to the design and development of the prototype of the auditing algorithms and the dashboard. University of Nottingham will contribute on the engagement with UK doctors. University of Texas at Austin will contribute on the engagement with USA doctors. University of Southampton will contribute on creating policies related to the evaluation and validation of AI.
Impact The collaboration started in March 2023. The main current output is the funding of 72460 pounds obtained by the team. This is a multidisciplinary collaboration involving: medicine, computer science and law.
Start Year 2023
 
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 Enhanced medical robotics case study 
Organisation Johns Hopkins University
Department John Hopkins Malaria Research Institute
Country United States 
Sector Academic/University 
PI Contribution We are still at an early stage - work to date has involved discussions and planning.
Collaborator Contribution Similar to above - discussions and planning.
Impact Computer Science and Medical Devices.
Start Year 2022
 
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 Integration Project on Verifiably Human-Centric Robot Assisted Dressing 
Organisation Durham University
Country United Kingdom 
Sector Academic/University 
PI Contribution We have been involved in establishing this project, with Dr Rafiq leading much of the development (as part of a small team). The project has just been accepted, subject to some changes, and we hope that it will start soon.
Collaborator Contribution Developing the ideas and proposal, through meetings/discussions.
Impact It is about to start - so too early.
Start Year 2022
 
Description Integration Project on Verifiably Human-Centric Robot Assisted Dressing 
Organisation King's College London
Country United Kingdom 
Sector Academic/University 
PI Contribution We have been involved in establishing this project, with Dr Rafiq leading much of the development (as part of a small team). The project has just been accepted, subject to some changes, and we hope that it will start soon.
Collaborator Contribution Developing the ideas and proposal, through meetings/discussions.
Impact It is about to start - so too early.
Start Year 2022
 
Description Integration Project on Verifiably Human-Centric Robot Assisted Dressing 
Organisation University of Lincoln
Country United Kingdom 
Sector Academic/University 
PI Contribution We have been involved in establishing this project, with Dr Rafiq leading much of the development (as part of a small team). The project has just been accepted, subject to some changes, and we hope that it will start soon.
Collaborator Contribution Developing the ideas and proposal, through meetings/discussions.
Impact It is about to start - so too early.
Start Year 2022
 
Description Integration Project on Verifiably Human-Centric Robot Assisted Dressing 
Organisation University of York
Country United Kingdom 
Sector Academic/University 
PI Contribution We have been involved in establishing this project, with Dr Rafiq leading much of the development (as part of a small team). The project has just been accepted, subject to some changes, and we hope that it will start soon.
Collaborator Contribution Developing the ideas and proposal, through meetings/discussions.
Impact It is about to start - so too early.
Start Year 2022
 
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 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 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 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 MLighter: The holistic tool for security evaluations of machine learning systems 
Description MLighter is a tool for machine learning testing that aims to integrate three testing levels: performance, security and reliability. The tool can be used as a library although it also contains a graphical user interface that aims to connect all the different levels. 
Type Of Technology Software 
Year Produced 2023 
Open Source License? Yes  
Impact MLighter is finding multiple applications in different areas. At KCL we are extending the abilities of MLighter to discover vulnerabilities in software related to machine learning. The team is also collaborating with the TAS Hub in a project called DORIAN, which focuses on auditing medical diagnosis systems based on machine learning. This collaboration involves people from the Johns Hopkins University, University of Texas at Austin, University of Southampton, and the University of Nottingham, making it an international project. Furthermore, MLighter is also being applied to measure the robustness of mental state examination models, in an international multi-disciplinary collaboration involving Dr Mariana Pinto da Costa, a Consultant Psychiatrist at South London and Maudsley NHS Foundation Trust and a Senior Lecturer at the Psychological Medicine Department at King's College London, and Dr Gema Bello-Orgaz from the Universidad Politécnica of Madrid. 
URL http://mlighter.freedevelop.org/
 
Title RoboTool Plugin for RoboCert 
Description Series of Eclipse plugins to extend the existing RoboTool software distribution with support for the new version of the RoboCert property language, which now has a textual notation for producing sequence diagram based property specifications. RoboTool is extended to generate tock-CSP for each such diagram and any assertions over said diagrams. This software is an early draft. Source available at https://github.com/UoY-RoboStar (see repositories marked 'robocert-'). 
Type Of Technology Software 
Year Produced 2022 
Open Source License? Yes  
Impact Contribution towards paper to appear at ICFEM 2022. 
URL https://robostar.cs.york.ac.uk/robotool/
 
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
 
Title The MCAPL Framework 
Description The MCAPL framework is a suite of tools for building interpreters for agent programming languages and model checking programs executing in those interpreters. It consists of the AIL toolkit for building interpreters for rational agent programming languages (BDI languages) and the AJPF model checker. AJPF extends the JavaPathfinder model checker to prove LTL properties of BDI agents. This distribution also contains a number of programming languages implemented in the AIL. Chief among these are Gwendolen, the EASS variant of Gwendolen that can be used to program hybrid autonomous systems and GOAL. This is the 2021 release of the framework, consisting of all necessary source code files and manuals. 
Type Of Technology Software 
Year Produced 2021 
Open Source License? Yes  
Impact None 
URL https://zenodo.org/record/5720861
 
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 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 AsturCon: Keynote about the malware Arms Race 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Industry/Business
Results and Impact This activity was a cybersecurity industry workshop with more than 400 attendees, 15 speakers and more than 30 companies involved. My presentation as a keynote speaker was related to the security of systems, mainly how malware attack them and how to defend from them.
Year(s) Of Engagement Activity 2022
URL https://asturcon.tech/
 
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 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 21381: Conversational Agent as Trustworthy Autonomous System (Trust-CA) 
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 The overall goal of the Dagstuhl Seminar 21381 "Conversational Agent as Trustworthy Autonomous System" (Trust-CA) was to bring together researchers and practitioners, who are currently engaged in diverse communities related to Conversational Agents (CA), to explore challenges in maximising the trustworthiness of and trust in conversational agents as AI-driven autonomous systems - an issue deemed increasingly significant given their widespread uses in every sector of life - and to chart a roadmap for the future conversational agent research. The three main challenges we identified were:
How do we develop trustworthy conversational agents?
How do we build people's trust in them?
How do we optimise human and conversational agent collaboration?
The Seminar Trust-CA took place on 19-24 September 2021 in a hybrid mode. Out of 50 invitees, 19 attended in person and the rest joined online from all over the world, including Brazil, Canada, France, Germany, Greece, Ireland, Netherlands, Norway, Poland, South Korea, Sweden, Switzerland, UK and USA.
Year(s) Of Engagement Activity 2021
URL https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=21381
 
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 EAI International Conference on IoT and Big Data Technologies for HealthCare 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Keynote lecture presented:

I.Tyukin. The challenge of trustworthy data- driven Artificial Intelligence: boundaries, limitations, and opportunities, October 18-19, 2021
Year(s) Of Engagement Activity 2021
 
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 East China Normal University Summer School on Trustworthy Systems 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Myself, Ana Cavalcanti, and James Woodcock (among others not in the Node) gave seminars and lectures as part of a weeklong online Summer School on Trustworthy Systems. While this was primarily discussing the RoboStar approach to model-driven robotic system engineering, topics touched on verifiability node work as the Firefighting UAV case study was used extensively as a running example, and the current state of the RoboCert property language was disseminated.
Year(s) Of Engagement Activity 2022
 
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 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 ICERM Safety and Security of Deep Learning 
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 on the subject of mathematical quantification and high-level tests of non-symbolic AI / data-driven AI vulnerabilities

I.Tyukin. Breaking into a Deep Learning box, April 10 - 11, 2021. ICERM Safety and Security of Deep Learning
Year(s) Of Engagement Activity 2021
 
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 IEEE Technical Committee on Verification of Autonomous Systems 
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 I pariticipated actively in the IEEE Technical Committee on the Verification of Autonomous Systems.
In particular, I delivered a talk about the activities of the Node and also participated in the founding activities of its Education Committee.
Year(s) Of Engagement Activity 2021
URL https://www.ieee-ras.org/verification-of-autonomous-systems
 
Description IEEE Technical Committee on the Verification of Autonomous Systems seminar 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Other audiences
Results and Impact About 25 people attended a virtual talk at this monthly seminar. The topic was about causal analysis for the verification of autonomous systems and there were many questions and an interesting discussion with the audience afterwards.
Year(s) Of Engagement Activity 2023
 
Description INI Concurrency Meeting 2022 - RoboCert talk 
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 Gave a talk about my work on the RoboCert property language, and its use of formal concurrency reasoning methods, to the 2022 instalment of a long-running Concurrency Workshop series (circa 46 participants, including some industrial researchers and postgraduate students). This talk sparked questions and some discussion afterwards, while relating my area of research to a general current of research in concurrency reasoning (which would otherwise be outside the scope of the Verifiability Node, but is related to my work).
Year(s) Of Engagement Activity 2022
URL https://johnwickerson.github.io/cw2022.html
 
Description ITF Roundtable on Artificial Intelligence, Machine Learning and Regulation 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Policymakers/politicians
Results and Impact International Transport Forum Roundtable on Artificial Intelligence, Machine Learning and Regulation, 26-27 January at the OECD Premises, in Paris
Year(s) Of Engagement Activity 2023
 
Description Increasing Confidence in Autonomous Systems, Invited talk at VORtEX workshop 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Increasing Confidence in Autonomous Systems, Invited talk at VORtEX workshop
Year(s) Of Engagement Activity 2021
 
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 International Transport Forum Round Table on Artificial Intelligence, Machine Learning, and Regulation 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Policymakers/politicians
Results and Impact ITF-OECD roundtables are closed events designed to provide a forum for experts in a specific area of transport policy to exchange views and ideas in depth. I attended this round table and was invited to give a short presentation on Algorithmic Bias and participate in discussions around the regulation of Autonomous Vehicles and both Ethical and Technical issues with their verification and assurance. My slides were made available to other participants and I will be contributing to the resulting report that will be circulated to member countries of the ITF.
Year(s) Of Engagement Activity 2023
 
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 Panel member for the UKRI TAS Hub Equality, Diversity, and Inclusion Framework Launch Panel Discussion at the TAS Hub All-Hands meeting (14-16 September 2021) 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact I have been invited to be a panel member on a Panel Discussion event organised by the UKRI TAS Hub for the TAS Hub All-Hands meeting, which was held on 14-16 September 2021. The intention of the Panel Discussion event was to focus on EDI aspects, specific to TAS and on the intersection of EDI and RRI, addressing questions such as the following:

• What EDI issues does TAS research raise that are unique or particularly prevalent or pernicious?
• Which issues can we/should we focus on addressing (again, focused on TAS)?
• Conversely, what are the rabbit hole issues that we can't realistically do anything about?
• More generally, what has been the most effective/impactful intervention that has made a real difference to EDI that the panel members have ever seen?
• What will be your personal commitment to EDI as part of the TAS project?

The Panel Discussion session was held online and has been viewed by approx. 100 attendees of the event.
Year(s) Of Engagement Activity 2021
URL https://www.tas.ac.uk/bigeventscpt/all-hands-meeting/
 
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 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 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 Inward Visit to Computer Science from Laurus Ryecroft Academy 
Form Of Engagement Activity Participation in an open day or visit at my research institution
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact An inward visit of Year 9 students. Students attended a short lecture on Computer Graphics, toured the Cognitive Robotics Lab and undertook a Mars Rover themed programming activity.
Year(s) Of Engagement Activity 2024
 
Description Isaac Newton Institute workshop: Mathematics of Deep Learning 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact A lecture was delivered on the subject of security and vulnerabilities in data-driven AI models

I.Tyukin. Breaking into Deep Learning models, October 5, 2021, Isaac Newton Institute.
Year(s) Of Engagement Activity 2021
 
Description Keynote at LOPSTR 2022 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Public/other audiences
Results and Impact Gave a keynote at the 32nd International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2022). The title of the keynote was "Systematic Software Testing for Robotics".
Year(s) Of Engagement Activity 2022
URL https://lopstr2022.webs.upv.es/#speakers
 
Description Keynote at the 15th International Conference on Tests and Proofs (TAP 2021). 
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 keynote delivered at an international conference comprising both academic experts and professional practitioners.
The abstract of the keynote is appended below.

Learning About the Change: An Adaptive Approach to Automata Learning

Mohammad Reza Mousavi, University of Leicester, UK

Abstract: Automata learning is a technique to learn behavioural models from black-box systems. Variability and evolution are inherent to much of the modern autonomous systems and hence, new sorts of automata learning techniques are needed to learn about variability-intensive and evolving systems. In this talk, we first present the basic principles of automata learning and then report on two novel techniques for learning variability-annotated models as well as efficient learning for evolving systems by identifying the commonalities and differences in the learning process.

This talk is based on joint work with several people, and in particular, with Diego Damasceno and Adenilso Simao.
Year(s) Of Engagement Activity 2021
URL https://www.univ-orleans.fr/lifo/events/TAP2021/invited.html
 
Description Keynote at the 17th Workshop on Advances in Model Based Testing (A-MOST 2021). 
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 keynote presented at an international workshop for industrial and academic audience comprising about 40 participants. The keynote led to a very active engagement both during the workshop and also contacts by some of the participating company representatives.
The abstract of the keynote is appended below.

ariability is an inherent part of modern software and systems and deserves a first-class treatment in software and systems engineering. Moreover, due to the sheer size of the variability space, variability needs to be treated rigorously and in a structured manner in order to come up with meaningful assurances about this huge space. In this talk, I will start with some basic results about modelling behavioural variability. Subsequently, I present some techniques on model-based testing based on variability-aware models and finally, conclude with recent techniques on learning behavioural models from variability-intensive systems.

The material present in this talk on based on about a decade of joint research with many people including Harsh Beohar, Andre Takeshi Endo, Vanderson Hafemann Fragal, Fatemeh Ghassemi, Malte Lochau, Lars Luthmann, Carlos Diego Nascimento Damasceno, Adenilso Simao, Uraz Türker, and Mahsa Varshosaz.
Year(s) Of Engagement Activity 2021
URL https://icst2021.icmc.usp.br/home/a-most-2021
 
Description Keynote at the 33rd IFIP International Conference on Testing Software and Systems (ICTSS 2021) 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact This is a keynote delivered at an international conference held at UCL. The audience comprised a mix of academic experts and industrial professionals. The keynote was about the environmental impact and sustainability of autonomous systems and led to a lively discussion. It also led to further contacts with some industrial professionals. The abstract of the talk is appended below.

Catch Me If You Can: Doping Detection in Cyber-Physical Systems

Abstract:
We will start with a broad overview of our research philosophy on trust in autonomous systems. We will review some of the ongoing projects at our group in this context. Subsequently, we present a novel notion of doping cleanness for cyber-physical systems. This notion allows for perturbing the inputs and observing the perturbed outputs both in the time- and value-domains. We instantiate our definition using existing techniques for conformance testing and runtime monitoring for cyber-physical systems. We show that our generalised definitions are essential in a data-driven method for doping detection and apply our definitions to a case study concerning diesel emission tests. We report on the doping detection results on the NOx emission of a particular diesel vehicle.

The talk is based on joint work with the following people:
Sebastian Biewer (Saarland University), Rayna Dimitrova (CISPA Saarbrücken), Michael Fris (Automotive Powertrain HTW Saar), Maciej Gazda (University of Sheffield), Thomas Heinze (Automotive Powertrain HTW Saar), and Holger Hermanns (Saarland University)
Year(s) Of Engagement Activity 2021
URL http://ictss2021.cs.ucl.ac.uk/keynotes.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 Lego Rovers at Anderton Primary School 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at Callands Primary 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at Cathedral School of St. Peter and St. Paul 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in a primary school prompting interesting questions from children.
Year(s) Of Engagement Activity 2023
 
Description Lego Rovers at Chorlton Primary 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at Co-op Academy Medlock 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Mars Rover themed programming workshops involving Lego Robots delivered to after school coding club.
Year(s) Of Engagement Activity 2024
 
Description Lego Rovers at Croston Cub and Beaver Scouts 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Other audiences
Results and Impact Robot programming activity delivered at the regular Cub Scout event themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at Heaton School 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Lego Rover programming activity delivered to SEND students at a Special Needs school.
Year(s) Of Engagement Activity 2023
 
Description Lego Rovers at Hope School 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2021
 
Description Lego Rovers at John Fisher Catholic High School 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at Kingsway Primary Academy 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Lego Robot programming activity delivered in a primary school prompting interesting questions and discussion from children.
Year(s) Of Engagement Activity 2023
 
Description Lego Rovers at Medlock Primary School 
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 Robot stand themed around Mars Rovers at local primary school community fair.
Year(s) Of Engagement Activity 2021
 
Description Lego Rovers at Middlewich High School 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Five Mars Rover themed programming workshops involving Lego Robots delivered to Year 7.
Year(s) Of Engagement Activity 2024
 
Description Lego Rovers at Plymouth Grove Primary School 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at Rushbrook Primary Academy 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at ScienceX 
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 Drop-in stand involving programming Lego Rovers at University Science Event.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at St Paul's Primary School 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at St. Helens Bever Group 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Other audiences
Results and Impact Lego Robot programming activity delivered to a Beaver Scout group.
Year(s) Of Engagement Activity 2023
 
Description Lego Rovers at St. Mary's Blackbrook 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at St. Saviors 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Lego Robot programming workshop run for children in years 3-6. Sparked interesting questions from the children.
Year(s) Of Engagement Activity 2023
 
Description Lego Rovers at St. Teresa's Catholic Primary 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at Stargazing 
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 Lego Robot stand at the World Museum, Liverpool in support of their Stargazing Event.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at The Sutton Academy 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2021
 
Description Lego Rovers at University of Manchester Community Fair 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Public/other audiences
Results and Impact Robot programming activity themed around Mars Rovers, delivered as a drop-in stand.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at Weston Village Primary 
Form Of Engagement Activity Participation in an activity, workshop or similar
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Schools
Results and Impact Robot programming activity delivered in school themed around Mars Rovers. Sparked discussion and questions form the children.
Year(s) Of Engagement Activity 2022
 
Description Lego Rovers at the World Museum 
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 Robot programming activity themed around Mars Rovers delivered as family workshops at the World Museum.
Year(s) Of Engagement Activity 2022
 
Description Living With AI Podcast: Exploring Trust & Driverless Cars 
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 Public/other audiences
Results and Impact An episode of the Living with AI podcast on Exploring Trust & Driverless Cars.
To date, this episode attracted 162 downloads, from four continents and more than ten countries.
The programme of the episode is appended below.

Exploring Trust & Driverless Cars
Living With AI Podcast: Challenges of Living with Artificial Intelligence
Genre: Technology

00:30 Paurav Shukla
00:39 Gary Burnett
00:44 Christian Enemark
00:58 Sean Riley
01:42 Amazon's first Robotaxi (The Verge)
03:00 Google/Waymo Ride Sharing (Tech Crunch)
03:35 Connected Everything Driverless Pods (Computerphile)
06:25 Small Computer Industry aside became viral joke 'Bill Gates vs GM' (Snopes)

08:40 Mohammad Mousavi

09:17 Honda Tier3 Car (Autonews)
12:25 Internet of Things Problems (Computerphile)
22:15 Will your driverless car be willing to kill you to save the lives of others? (Guardian)
42:30 Unexpected Item in the Bagging Area (Twitter Thread)
Year(s) Of Engagement Activity 2021
URL https://podcasts.apple.com/us/podcast/exploring-trust-driverless-cars/id1538425599?i=1000508492099
 
Description MDE-Network Panel: What does it take to get MDE practically adopted? 
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 Panel chaired by Perdita Stevens. Federico Tomassetti, Tony Clark, Nelly Bencomo and Mohammad Mousavi as panellists on 'What does it take to get MDE practically adopted?''. The panel was held at the MDE-Net Annual Conference 2022.
Year(s) Of Engagement Activity 2022
URL https://www.youtube.com/watch?v=H3QHic9yzNM&t=1s
 
Description MDENet Annual Symposium 2022 - MDE for cyber-physical systems 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Keynote at the MDENet Annual Symposium 2022 about MDE for cyber-physical systems.
Year(s) Of Engagement Activity 2022
URL https://www.youtube.com/watch?v=Z8wWtODD7nA&t=1s
 
Description National RAS Regulations, Standards and Ethics Committee 
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 I was invited to and participated in the initial discussions leading to the National RAS Regulations, Standards and Ethics Committee. The committee is now formed, approved by the Department for Science, Innovation, and Technology and funded by InnovateUK. It will continue its operation and will establish policy guidance regarding safety and trustworthiness of RAS.
Year(s) Of Engagement Activity 2023,2024
 
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 Panel on Fellowships and Funding: Skills Day Mentoring Session 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact Panel on Fellowships and Funding: Skills Day Mentoring Session
We shared our experiences on applying for funding and Fellowship opportunities, and provided some tips for success. This interactive session was mostly designed for those at the early stages of their careers.
It was attended by some 40 ECRs and was viewed seven times offline.

The session was delivered at the UKRI TAS Programme All Hands Meeting in September 2021 by Professor Mohammad Mousavi, Professor Susan Gourvenec, and Professor Weisi Guo.
Year(s) Of Engagement Activity 2021
URL https://vimeo.com/showcase/9033904/video/647258406
 
Description Participation and Winners of Oxford-York UAV Hackathon 
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 A total of 34 participants from the University of York and the Oxford Robotics Institute participated in this challenge to develop a safe return-to-home function and an associated safety case for an Uncrewed Aerial Vehicle (UAV).

On the day, the judges voted Team 3 as the overall winners, which comprised research fellow Philippa Ryan, graduate research student, Samuel Sze from the Oxford Robotics Institute, research student, Arjun Badyal from the University of York, PhD student Hasan Bin Firoz also from the University of York, Ben Hardin from Oxford Robotics Institute, and research associate Felix Ulrich-Oltean from the University of York. The approach of Team 3 centred around developing and implementing a formal model using RoboSim, and its inclusion in a safety case. This has led to further collaboration with fellow team members and hackathon organisers.
Year(s) Of Engagement Activity 2023
URL https://www.york.ac.uk/assuring-autonomy/news/blog/york-oxford-hackathon/
 
Description Ph.D. Symposium with Wallenberg Autonomous Systems Program (Sweden), Trustworthy Autonomous Systems Program (UK-wide) and Safe and Trusted AI (KCL) 
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 On Monday the 10th of October 2022, a delegation of about 60 Ph.D. students from the Wallenberg Autonomous Systems Program (https://wasp-sweden.org/) visited the Verifiability Node and met with the team as well as representatives from the TAS Hub and projects and Ph.D. students from Safe and Trusted AI program at King's College London.
Year(s) Of Engagement Activity 2022
URL https://wasp-sweden.org/
 
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 Sheffield Robotics day - with external visitors and collaborators 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Industry/Business
Results and Impact This was a talk at an open one day event held by Sheffield Robotics: the annual Sheffield Robotics Showcase. Participants include researchers from across the university, researchers from Sheffield Halam (also a member of Sheffield Robotics), industrial collaborators, and health professions. The puprose was to provide an overview of the Verifiability Node, outline the work being carried out at Sheffield, and encourage collaboration.
Year(s) Of Engagement Activity 2022
 
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 Research visit from American University of Sharjah 
Form Of Engagement Activity Participation in an open day or visit at my research institution
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact In November we hosted a research visit from American University of Sharjah (UAE) at the Verifiability Node.
Year(s) Of Engagement Activity 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 RoboStar and YorRobots Industrial 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 YorRobots and RoboStar York jointly presented a two-day exhibition, which included one day of RoboStar lightning talks and another day of industrial talks in the field of robotics. As part of this, several members of the Verifiability Node presented on both their case studies - the Firefighting UAV (Shival Dubey, Bilal Kaddouh, Mohammad Mousavi, Matt Windsor along with colleague Pedro Ribeiro) and Robot Assisted Dresser (Thomas Wright and Yasmeen Rafeeq), as well as their own work and ventures (Rob Hierons, Matt Windsor, James Woodcock). In addition, there was a two day poster display. The audience included predominantly industry members from a wide area but also local faculty and postdoctoral researchers, postgraduate students, and some undergraduate students.
Year(s) Of Engagement Activity 2022
URL https://robostar.cs.york.ac.uk/events/yrie2022/
 
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 Stargazing at the World Museum 
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 Lego Robot programming activity as a stand at an evening event at a Museum. Prompted engagement from several teenagers in programming tasks and problems.
Year(s) Of Engagement Activity 2023
 
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 TAS Conversations - Autonomous Vehicles 
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 Public/other audiences
Results and Impact This is the first episode of the TAS Conversation on Autonomous Vehicles, featuring Siddhartha Khastgir, Sarah Sharples, Jo-Ann Pattinson, Mohammad Mousavi, and Jack Stilgoe. This was a multidisciplinary panel debating various technical, legal, and social issues in the deployment of autonomous vehicles. The conversation attracted 36 viewers.


TAS Conversation Episode 1. Autonomous Vehicles

Consider the subtleties of driving that we take for granted

How long do human driver's wait at a zebra crossing before we realise the pedestrian isn't crossing? How do we translate that interaction into an autonomous vehicle's decision-making process?

This episode delves into the complexities of bringing autonomous vehicles safely into society and asks many poignant questions, including:

- Are we ready for autonomous vehicles?
- What does the utopian world of autonomous vehicles look like?
- How does the law keep up with the changing technology?
- What are the ethical implications of autonomous vehicles?
- How do we translate everyday assumptions that human drivers make into autonomous vehicles?
Year(s) Of Engagement Activity 2021
URL https://www.tas.ac.uk/bigeventscpt/tas-conversations-autonomous-vehicles/
 
Description TAS Fireside Chat 
Form Of Engagement Activity A formal working group, expert panel or dialogue
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact This fireside chat featured a panel comprising the PIs of the TAS Hub and all Nodes.
We engaged the audience with the aims and objectives of the TAS programs, its research programs, and early results.
The fireside chat was attended live by 68 people, and subsequently watched offline by 34 people to date.
Year(s) Of Engagement Activity 2021
URL https://vimeo.com/616104307
 
Description TAS Maritime Sector Workshop 
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 In collaboration with the TAS Hub, Connected People and Places Catapult and the Institute for Assured Autonomy at York University, we organised a workshop on autonomy in the maritime sector with participation from government / policy makers, industry, and academia. It involved keynotes and workshops on ideation and creation of future bids.
Year(s) Of Engagement Activity 2022
 
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 Sheffield Robotics 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Regional
Primary Audience Professional Practitioners
Results and Impact Short presentation to describe the Verifiabiltiy Node and the TAS programme, outline the work to date at Sheffield, explain our plans, and encourage collaboration.
Year(s) Of Engagement Activity 2022
 
Description Tutorial at Midlands Graduate School 2021 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Postgraduate students
Results and Impact Mohammad Reza Mousavi delivered an advanced course at the Midlands Graduate School in the Foundations of Computing Science 2021.
Year(s) Of Engagement Activity 2021
URL https://staffwww.dcs.shef.ac.uk/people/G.Struth/mgs21.html
 
Description U3A talk 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Public/other audiences
Results and Impact Gave a talk to the Cheadle "University of the Third Age" group around AI and Robotics.
Year(s) Of Engagement Activity 2023
 
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 University of York 'HackSoc' Student Society talk: 'RoboCert: Property Specification for Robot Software' 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Undergraduate students
Results and Impact I (Matt Windsor) gave a largely informal talk to a small group of students as part of the HackSoc (University of York computer science society) talk series on my work on RoboCert, as funded by the TAS verifiability node work package 1.
Year(s) Of Engagement Activity 2022
 
Description Verifiability Channel 
Form Of Engagement Activity Engagement focused website, blog or social media channel
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Media (as a channel to the public)
Results and Impact We established an accessible talk series by world-leading experts in the area of Verifiability of Autonomous Systems.
The channel has attracted close to 2000 views of the featured talks to date.
Year(s) Of Engagement Activity 2021,2022
URL http://bit.ly/VerifiabilityChannel
 
Description Verifiability Mailing List 
Form Of Engagement Activity Engagement focused website, blog or social media channel
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact To build a community around Verfiability of Autonomous Systems, we established an open mailing list for announcing events and disseminating results.
The mailing list has 108 members and 49 conversations to date.
Year(s) Of Engagement Activity 2021,2022
URL http://verifiability@googlegroups.com
 
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 Verifiability Website 
Form Of Engagement Activity Engagement focused website, blog or social media channel
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact We designed a professional website to disseminate our scientific papers, tools, policy papers, talks, and reports. The site has on average 1.5k visitor per month, with a total of over 21k visitors to date.
Year(s) Of Engagement Activity 2021,2022
URL http://verifiability.org/
 
Description Verifying Autonomous Systems - We need help from you! Invited talk at CPS-IoT Week Workshop on Machine Learning in Control (LEAC), 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact Verifying Autonomous Systems - We need help from you! Invited talk at CPS-IoT Week Workshop on Machine Learning in Control (LEAC),
Year(s) Of Engagement Activity 2021
 
Description Verifying Autonomous Systems, Invited talk at ORCA/SOLITUDE Workshop on Safety Assurance for Deep Learning in Underwater Robotics 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach National
Primary Audience Professional Practitioners
Results and Impact Verifying Autonomous Systems, Invited talk at ORCA/SOLITUDE Workshop on Safety Assurance for Deep Learning in Underwater Robotics
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 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 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 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 Workshop on Complex and simple models of multidimensional data : from graphs to neural networks 
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 The purpose of the workshop was to create an international forum for a broad discussion around the topics of complexity, dimensionality, and artificial intelligence and disseminate state-of-the-art knowledge in the area. The event was held online, with more than 150 registrations. In addition to organising the workshop a lecture on the topic of certifiable learning from low-sample high-dimensional data was delivered too.

I.Tyukin, A.N. Gorban. The mathematics of learning from high-dimensional low-sample data with small neural networks, December 1, 2021. Workshop on Complex and simple models of multidimensional data : from graphs to neural networks.
Year(s) Of Engagement Activity 2021
 
Description Workshop organisation/chairing 
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 Co-organised a Dagstuhl Seminar aiming to develop a "Roadmap for Responsible Robotics"
Year(s) Of Engagement Activity 2023
URL https://www.dagstuhl.de/23371
 
Description Workshop organisation/chairing 
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 Co-organised the Second Workshop on "Quality and Reliability Assessment of Robotic Software Architectures and Components" as part of the International Conference on Robotics and Automation in June 2023
Year(s) Of Engagement Activity 2023
URL https://sites.google.com/view/qrarsac2023
 
Description Workshop organisation/chairing 
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 Co-ord=ganised this first international symposium on the Verificaiton of Autonomous Mobile Systems in 2023. The aim was to facilitate the transfer of knowledge and experience between academia, regulators, and industry concerning the Verification of Autonomous Mobile Systems operating over large outdoor spaces, and to work towards a report aimed at the diverse organisations involved in the use of Autonomous Systems across air, land, and sea applications, particularly those that are safety-critical.
Year(s) Of Engagement Activity 2023
URL https://www.irt-systemx.fr/evenements/vams-is-23
 
Description Workshop organisation/chairing 
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 Co-organised the IROS 2023 workshop " `It Works Really Well!': Verification in Theory and Practice" showcasing verificaiton issues and techniques at one of the world's leading robotics conferences.
Year(s) Of Engagement Activity 2023
URL https://robotistry.org/vaswg/IROS23_Workshop/
 
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 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/