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.
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
- University of Leicester (Lead Research Organisation)
- University of Surrey (Collaboration)
- Technical University of Munich (Collaboration)
- Thales Group (Collaboration)
- Jacobs Engineering Group (Collaboration)
- Microsoft Research (Collaboration)
- UFPE (Collaboration)
- University of Bremen (Collaboration)
- Seoul National University (Collaboration)
- Aarhus University (Collaboration)
- D-RisQ (Collaboration)
- Southwest University (Collaboration)
- Technical University Berlin (Collaboration)
- Lancaster University (Collaboration)
- Galois, Inc. (Collaboration)
- Trinity College Dublin (Collaboration)
- Defence Science & Technology Laboratory (DSTL) (Collaboration)
- Praxis Systems Ltd (Collaboration)
- Altran (Collaboration)
- Indian Institute of Science Bangalore (Collaboration)
- University of Toronto (Collaboration)
- UNIVERSITY OF YORK (Collaboration)
- KING'S COLLEGE LONDON (Collaboration)
- ClearSy (Project Partner)
- D-RisQ (United Kingdom) (Project Partner)
- Cyberselves Universal Limited (Project Partner)
- BT Group (United Kingdom) (Project Partner)
- Bloc Digital (Project Partner)
- Amazon (United States) (Project Partner)
- Connected Places Catapult (Project Partner)
- Shadow Robot (United Kingdom) (Project Partner)
- Guidance Automation Ltd (Project Partner)
- Consequential Robotics Ltd (Project Partner)
- Scoutek Ltd (Project Partner)
- Sheffield Children's NHS Foundation Trust (Project Partner)
- BAE Systems (United Kingdom) (Project Partner)
Publications
Ferrando A
(2022)
Bridging the gap between single- and multi-model predictive runtime verification
in Formal Methods in System Design
Fisher M
(2020)
Towards a framework for certification of reliable autonomous systems
in Autonomous Agents and Multi-Agent Systems
Fisher M
(2022)
AI Journal Special Issue on Ethics for Autonomous Systems
in Artificial Intelligence
Fisher M
(2021)
Increasing confidence in autonomous systems
Folstad A
(2022)
Chatbot Research and Design
Foster S
(2021)
Automated verification of reactive and concurrent programs by calculation
in Journal of Logical and Algebraic Methods in Programming
Foster S
(2021)
Automated verification of reactive and concurrent programs by calculation
in Journal of Logical and Algebraic Methods in Programming
Foster S
(2020)
Unifying theories of reactive design contracts
in Theoretical Computer Science
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 | Please note that this award is followed up by EP/V026801/2. For the sake of completeness I copy the narrative impact from EP/V026801/2 here. Please consult the EP/V026801/2 entry for other entries. 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 assisted education for neurodiverse children by means of explaining the behaviour of assistive robots using our Verifiability platform. We are currently working on our assistive-dressing robotic case study which will further provide impact in the healthcare domain. |
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 | 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 | 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 guidance/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 | 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 | 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 | 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 | 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 | 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 | 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 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 | 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 | 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 | Uncertainty |
Organisation | King's College London |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Discussions between the University of York and King's College London on a future research proposal. |
Collaborator Contribution | Discussions between the University of York and King's College London on a future research proposal. |
Impact | Draft research proposal. |
Start Year | 2022 |
Description | Uncertainty in autonomous systems |
Organisation | King's College London |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Definition of probabilistic semantics in UTP and implementation in Isabelle/UTP. |
Collaborator Contribution | Problems, examples, case studies. |
Impact | No outputs yet. |
Start Year | 2021 |
Description | Uncertainty in autonomous systems |
Organisation | University of York |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Definition of probabilistic semantics in UTP and implementation in Isabelle/UTP. |
Collaborator Contribution | Problems, examples, case studies. |
Impact | No outputs yet. |
Start Year | 2021 |
Description | VSR collaborations |
Organisation | Microsoft Research |
Department | Microsoft Research Cambridge |
Country | United Kingdom |
Sector | Private |
PI Contribution | Organising the UK's contribution to the Verified Software Initiative. |
Collaborator Contribution | Suppliers of case studies, verification technology, challenge project prizes, organisers of workshops. |
Impact | Collection of verification case studies for experimentation by the verification community. |
Start Year | 2006 |
Description | VSR collaborations |
Organisation | Praxis Systems Ltd |
Country | United Kingdom |
Sector | Private |
PI Contribution | Organising the UK's contribution to the Verified Software Initiative. |
Collaborator Contribution | Suppliers of case studies, verification technology, challenge project prizes, organisers of workshops. |
Impact | Collection of verification case studies for experimentation by the verification community. |
Start Year | 2006 |
Description | Verification and uncertainties in self-integrating systems |
Organisation | Aarhus University |
Department | Department of Engineering |
Country | Denmark |
Sector | Academic/University |
PI Contribution | Expertise in unification of semantics and verification techniques. |
Collaborator Contribution | Expertise in self-integrating systems and uncertainty. |
Impact | Publication: Lukas Esterle, Barry Porter, Jim Woodcock: Verification and Uncertainties in Self-integrating System. ACSOS-C 2021: 220-225 DOI: 10.1109/ACSOS-C52956.2021.00050 |
Start Year | 2021 |
Description | Verification and uncertainties in self-integrating systems |
Organisation | Lancaster University |
Department | School of Computing and Communications |
Country | United Kingdom |
Sector | Academic/University |
PI Contribution | Expertise in unification of semantics and verification techniques. |
Collaborator Contribution | Expertise in self-integrating systems and uncertainty. |
Impact | Publication: Lukas Esterle, Barry Porter, Jim Woodcock: Verification and Uncertainties in Self-integrating System. ACSOS-C 2021: 220-225 DOI: 10.1109/ACSOS-C52956.2021.00050 |
Start Year | 2021 |
Description | Verification grand challenge history |
Organisation | Altran |
Country | United Kingdom |
Sector | Private |
PI Contribution | History of the Verified Software Initiative |
Collaborator Contribution | Personal accounts of contributions to the Verified Software Initiative. |
Impact | Publication: Jim Woodcock, Janet Barnes, Rod Chapman, Simon Foster, Thomas Santen: Verification in the Grand Challenge. Theories of Programming 2021: 125-156 DOI: 10.1145/3477355.3477363 |
Start Year | 2021 |
Description | Verification grand challenge history |
Organisation | Technical University Berlin |
Country | Germany |
Sector | Academic/University |
PI Contribution | History of the Verified Software Initiative |
Collaborator Contribution | Personal accounts of contributions to the Verified Software Initiative. |
Impact | Publication: Jim Woodcock, Janet Barnes, Rod Chapman, Simon Foster, Thomas Santen: Verification in the Grand Challenge. Theories of Programming 2021: 125-156 DOI: 10.1145/3477355.3477363 |
Start Year | 2021 |
Description | bangalore-2018 |
Organisation | Indian Institute of Science Bangalore |
Country | India |
Sector | Academic/University |
PI Contribution | Newton grant from RAEng held by IIIT-B. Contributions on refinement of simulink models. |
Collaborator Contribution | Research in refinement of simulink models. |
Impact | Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. RAMiCS 2018: 205-224 Simon Foster, Kangfeng Ye, Ana Cavalcanti, Jim Woodcock: Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra. CoRR abs/1806.02101 (2018) |
Start Year | 2018 |
Description | butterfield-tcd-march-2018 |
Organisation | Trinity College Dublin |
Department | Trinity Biomedical Sciences Institute |
Country | Ireland |
Sector | Hospitals |
PI Contribution | Research discussions at TCD. |
Collaborator Contribution | Research discussions. |
Impact | Discussions on future research collaborations. |
Start Year | 2018 |
Description | chongqing-2-2018 |
Organisation | Southwest University |
Country | China |
Sector | Academic/University |
PI Contribution | Royal Society China Cost Share Programme |
Collaborator Contribution | Research contributions. |
Impact | None yet. |
Start Year | 2018 |
Description | chongqing2018 |
Organisation | Southwest University |
Country | China |
Sector | Academic/University |
PI Contribution | Royal Society China Cost Share Programme. |
Collaborator Contribution | Rsearch contributions. |
Impact | No outputs yet. |
Start Year | 2018 |
Description | digit-2018 |
Organisation | Aarhus University |
Department | Aarhus Institute of Advanced Studies |
Country | Denmark |
Sector | Academic/University |
PI Contribution | Planning for future collaboration. |
Collaborator Contribution | Research exchanges. |
Impact | Proposal to Grundfos Foundation. |
Start Year | 2018 |
Description | peleska-testing-2018 |
Organisation | University of Bremen |
Country | Germany |
Sector | Academic/University |
PI Contribution | Rsearch discussions. |
Collaborator Contribution | Rsearch discussions. |
Impact | Research proposals. |
Start Year | 2018 |
Title | 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 | 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 | 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 | CyPhyAssure Spring School |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Participation in Spring School on the assurance of cyber-physical systems. |
Year(s) Of Engagement Activity | 2019 |
URL | https://www.cs.york.ac.uk/circus/CyPhyAssure/school/ |
Description | DIGIT Advisory Board |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Participation in the advisory board of the center for digital twins at Aarhus University, |
Year(s) Of Engagement Activity | 2018 |
Description | Dagstuhl Seminar 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 | Encouraging Enterprise at KCL (March 2023) |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | Local |
Primary Audience | Professional Practitioners |
Results and Impact | The goal of the event was to encourage and advocate engagement of King's academic communities with industries and other stakeholders in the area of AI. The lecture was very well received by the audience who appreciated the advice. |
Year(s) Of Engagement Activity | 2023 |
Description | FM 2019 |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Talks and discussions with international colleagues. |
Year(s) Of Engagement Activity | 2019 |
Description | Few-shot learning (Sheffield, July 2022) |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | Regional |
Primary Audience | Professional Practitioners |
Results and Impact | Approximately 30 people attended the talk which has led to the discussion around the foundational problem of learning from few examples in high-dimensional and low-dimensional settings. A collaborative activity around the analysis of the notion of dimension of data sampled from trajectories of dynamical systems. The project involves academics from the University of Sheffield, Leicester, and King's College London. We have also agreed to work on a grant proposal and have already submitted one outline proposal (AI Hubs: Computational and Mathematical Foundations) |
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 | Huawei Research Forum |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Presentation on formal methods for assurance of security-related software in Huawei 5G products. |
Year(s) Of Engagement Activity | 2019 |
Description | Huawei Research Symposium |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Presentation of my research agenda to Huawei engineers. I gave advice on future research policy for their company. |
Year(s) Of Engagement Activity | 2019 |
Description | 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 | IFIP WG 2.3 Programming Methodology |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Hosted meeting of IFIP WG 2.3 on Programming Methodology. Organised scientific and social agenda, chaired the meeting, and gave an extended scientific talk. I involved my doctoral students and research assistants in the meeting. |
Year(s) Of Engagement Activity | 2019 |
URL | https://ifip-tc2-wg23.paluno.uni-due.de/?page_id=455 |
Description | 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 Joint Conference on Neural Networks 2022 |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | A presentation at the World Congress on Computational Intelligence / International Joint Conference on Neural Networks |
Year(s) Of Engagement Activity | 2022 |
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 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 seminar on the limitations of data-driven AI, the hierarchy of AI instabilities, and approaches to address them (Cambridge 2023) |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | Regional |
Primary Audience | Professional Practitioners |
Results and Impact | About 15 people attended the seminar followed by a discussion of further methods and tools needed for better understanding of the phenomenon. An agreement has been reached to work on several related topics and on the application of the tools to the analysis of dynamical systems. |
Year(s) Of Engagement Activity | 2023 |
Description | Invited seminar on the limitations, verifiability, and the challenge of AI errors (Newcastle 2023) |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | Regional |
Primary Audience | Professional Practitioners |
Results and Impact | Approximately 20 people attended the seminar where I presented our latest findings on the inevitable typicality of AI errors. |
Year(s) Of Engagement Activity | 2023 |
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 | 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 | Learning and generalisation from low-sample high-dimensional data (Edinburgh, October 2022) |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | Regional |
Primary Audience | Professional Practitioners |
Results and Impact | Approximately 60 people attended the seminar, which was followed by the discussion around the need to rethink the problem of learning in the context of the prevalence of distribution-agnostic approaches. New collaboration with Alex Serb and his research group emerged as a result of the activity. This was followed by a hackathon with two PDRAs participating from our side and one PDRA from Edinburgh. We are now working towards a joint paper summarising the findings. |
Year(s) Of Engagement Activity | 2022 |
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 | Newton Institue Workshop |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | I gave a talk about the impact of verification technology on practical application. |
Year(s) Of Engagement Activity | 2019 |
Description | Opening of Aarhus Centre for Digital Twins |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Keynote talk on research direction at the opening of the Centre for Digital Twins at Aarhus University. |
Year(s) Of Engagement Activity | 2019 |
URL | https://digit.au.dk/research-projects/centre-for-digital-twins/ |
Description | Organisation of RoboStar and YorRobots Industry Exhibition |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | On 11-12 October YorRobots and RoboStar hosted an Industry Exhibition. There were talks and demonstrations by RoboStar colleagues and from YorRobots, The Institute for Safe Autonomy, Adelard, AgroIntelli, BAE, Bristol Robotics Lab, ClearSy, Chemspeed Technologies, Connected Places, LabMan, LDRA, DRis-Q, Dyson, RobotCenter, ShadowRobot, Thales and VSI. |
Year(s) Of Engagement Activity | 2022 |
URL | https://robostar.cs.york.ac.uk/events/yrie2022/ |
Description | 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 | 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 | 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 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 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 | Symposium for Marie-Claude Gaudel |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | I gave a talk on software engineering for robotic control. |
Year(s) Of Engagement Activity | 2019 |
Description | 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 | Talk at Huawei engineering conference |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | A talk was given at Huawei's engineering conference on advance software engineering practice. |
Year(s) Of Engagement Activity | 2022 |
Description | Talk at Verification Future Meeting |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | National |
Primary Audience | Industry/Business |
Results and Impact | I gave an invited talk at this industry meeting. |
Year(s) Of Engagement Activity | 2019 |
URL | https://www.testandverification.com/conferences/verification-futures/vf2019 |
Description | Tutorial at 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 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 Jan Pekeska |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Discussions on research collaboration. |
Year(s) Of Engagement Activity | 2018 |
Description | Visit by Ziming Liiu |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit to discuss long-term research collaboration. |
Year(s) Of Engagement Activity | 2018 |
Description | Visit from Southwest University |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit from a delegation from Southwest University, Chongqing, China. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit from TCD Ireland |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Visit from colleagues from Trinity College Dublin. Contributions on probabilistic semantic for robotics. |
Year(s) Of Engagement Activity | 2018,2019 |
Description | Visit ti Aarhus University |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit to exchange research ideas. |
Year(s) Of Engagement Activity | 2018 |
Description | Visit to Aarhus University |
Form Of Engagement Activity | A formal working group, expert panel or dialogue |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Professional Practitioners |
Results and Impact | Research visit to AArhus University for continuing collaboration |
Year(s) Of Engagement Activity | 2023 |
Description | Visit to Chongqing |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit Southwest University to give lectures and direct doctoral students. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit to Chongqing |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | Workshop on formal methods for human-cyber-=physical systems. I gave talks on software engineering for robotics. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit to IISc |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Presentation of research work. Exchange of research ideas for future research proposals. |
Year(s) Of Engagement Activity | 2018 |
Description | Visit to IISc Bangalore |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Workshop at IISc funded by Royal Academy of Engineering. Discussed work on formal verification of operating system real-time kernels. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit to Malardalen University |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Postgraduate students |
Results and Impact | External examining of a doctoral student. Interaction with academic colleagues on research directions. Interaction with industry colleagues on research directions. |
Year(s) Of Engagement Activity | 2019 |
Description | Visit to Southwest University |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Study participants or study members |
Results and Impact | Visit to exchange ideas. |
Year(s) Of Engagement Activity | 2018 |
Description | Visit to Southwest University, Chongqing, China. Visit to Tong Ji University, Shanghai. |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Other audiences |
Results and Impact | Presentation of research and planning for future funding of international research programme. |
Year(s) Of Engagement Activity | 2023 |
Description | Visit to VSI Bremen |
Form Of Engagement Activity | A talk or presentation |
Part Of Official Scheme? | No |
Geographic Reach | International |
Primary Audience | Industry/Business |
Results and Impact | Visit to VSI in Bremen to discuss future research collaboration, especially in verification of learning-enabled systems. |
Year(s) Of Engagement Activity | 2023 |
Description | White Rose Retreat on Robotics |
Form Of Engagement Activity | Participation in an activity, workshop or similar |
Part Of Official Scheme? | No |
Geographic Reach | Local |
Primary Audience | Study participants or study members |
Results and Impact | Discussed future collaborative in robotics. |
Year(s) Of Engagement Activity | 2019 |
Description | Workshop 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 on Robust, Stable, and Secure AI (November 2022) |
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 | I organised the workshop and invited world-leading experts to participate. The workshop brought together experts across both academia and industry to debate the challenge of AI errors and the impact these errors have. All participants confirmed the importance of the topic and reported on the new perspectives and directions the workshop brought into their own research. |
Year(s) Of Engagement Activity | 2022 |
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 | 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 | 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 | 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 | 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/ |