UKRI Trustworthy Autonomous Systems Node in Verifiability

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

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.

Related Projects

Project Reference Relationship Related To Start End Award Value
EP/V026801/1 01/11/2020 14/08/2021 £2,923,653
EP/V026801/2 Transfer EP/V026801/1 15/08/2021 29/04/2024 £2,621,150
 
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, studying and identifying the basic building blocks of a 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/). We highlight below a few of these results.

- Designed the first generation of 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 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 We used our early findings to engage with both our 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 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 Digital/Communication/Information Technologies (including Software),Healthcare,Transport

URL https://verifiability.org/annual-reports/
 
Description Our Node embarked on an ambitious plan on building a strong and inclusive community interested in Verifiability for Autonomous Systems. To realise this plan, we organised several community building and public and policy engagement activities during the first year. To reach out to the community and disseminate our community-building and engagement activities we have adopted various media and resources. We have a professional website (https://verifiability.org), which went live right from the start of the project to make our results accessible to all stakeholders and interested parties. We have actively used social media (Twitter handle @tas_verif and a LinkedIn page), and maintained and expanded our public mailing list (verifiability@googlegroups.com). Our public mailing list currently has close to 150 members. Finally, we have disseminated our events through our Youtube channel with about 2000 views to date. Our community building activities aimed at engaging with researchers and industry participants to present and discuss state-ofthe- art research. The outcome of such activities has been a wider reach of the Node's research and knowledge exchange. We organised about 30 instances of the Verifiability Talk: a bi-weekly seminar, in which distinguished experts on the subject of testing, validation, and verification of autonomous systems present their research to members of our community. Thus far, we have held 24 instances of the Talk. We have edited and published the recordings on our Youtube channel, where we have had close to 2,000 views so far. We provided response to two policy-making calls for evidence and engaged in two standardisation committees.
First Year Of Impact 2022
Sector Digital/Communication/Information Technologies (including Software),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 Data: a new direction: A call for evidence from Department for Digital, Culture, Media & Sport
Geographic Reach National 
Policy Influence Type Gave evidence to a government review
URL https://kclpure.kcl.ac.uk/portal/files/163776916/Data_a_new_direction_FINAL_APPROVED.pdf
 
Description Gave evidence at the All Party Parliamentary Group on AI evidence meeting concerning national security: Regulation of AI-driven live facial recognition technologies
Geographic Reach National 
Policy Influence Type Participation in a advisory committee
 
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 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 Gave evidence to a government review
URL https://eprints.soton.ac.uk/450228/
 
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 Computational Agent Responsibility
Amount £642,184 (GBP)
Funding ID EP/W01081X/1 
Organisation Engineering and Physical Sciences Research Council (EPSRC) 
Sector Public
Country United Kingdom
Start 01/2022 
End 06/2024
 
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 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 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 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 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 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 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
 
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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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/