CyPhyAssure: Compositional Safety Assurance for Cyber-Physical Systems

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

Abstract

This research concerns assuring safety of autonomous robots. A robot is a machine that is capable of performing a complex sequence of steps, in order to achieve some goal. Autonomous robots act independently and do not require the direct intervention of a human operator. For example, autonomous vehicles are cars, lorries, or other road vehicles that are able to drive themselves to a destination without the need for a human driver. Another example are robot carers, that are able to assist elderly or disabled people with every day tasks, such as retrieving items, cleaning, playing games, and so on. Autonomous robots therefore present a number of exciting future opportunities for overcoming societal challenges.

Robots are computer systems, and the software that runs on them is very complex, far more so than a typical desktop, laptop computer, or mobile phone. Such computers have very simple inputs, like keyboard, mouse, and touchscreen. Robots, however, are "cyber-physical systems": they are both computational (cyber) devices, but they also interact with their physical environment. They have both sensors, that allow them to "see", "hear", and "feel" the world, and also actuators which allow them to manipulate objects in the world. For example, a care robot may have arms that it can move, and wheels to move around with. The software as a robot therefore has to be constantly monitoring its environment, and be able to quickly, appropriately, and, most importantly, safely respond to the changing environment.

If we cannot guarantee that a robot carries out its tasks safely, we cannot risk using them, as human injury or even death could result. A recent example concerns a Tesla Model S automated car that was unable to see a large white lorry crossing its path, and ploughed into the side of it killing its driver. Such tragic accidents reveal why safety is an utmost concern.

Our research will employ mathematical and logical techniques in an attempt to demonstrate that a robot is safe to operate in its target environment. We will employ a document called a "safety case" that contains a credible and convincing safety argument. This argument must, of course, be supported by evidence, and our technique will provide this through "model-based design", where computerised models of individual system parts are created as virtual prototypes. Such models can be described using complicated mathematics, such as algebra, differential equations, and probabilistic models. Probability, in particular, is very important since robots need to plan for possible uncertainty in there environment - such as a human being in an unexpected place.

Mathematics allows us to be rigorous - considering a large range of possible scenarios that would be very expensive to test in the real world. However, it is also difficult for a human to do the necessary mathematics manually. We will therefore use software called an "automated theorem prover" to try and show that each of the robot models behaves correctly and safely. This will include new techniques specifically for reasoning about cyber-physical systems.

We will apply our new techniques to a number of industrial problems, gleaned from our a number of robotics companies that we will partner with. This will allow us to provide guidance to them in ensuring their systems are safe. Our hope is that ultimately our project will ensure that robots can be safely introduced into our society, and thus open up a host of exciting future business opportunities.

Planned Impact

Autonomous robot technology promises to provide a variety of societal and economic benefits. Autonomous vehicles, for example, promise to make roads safer, and give better use of transport capacity. However, these benefits can only be harnessed by society if the technology has both public trust, and regulatory acceptance. There can often be understandable scepticism towards the technology, due to its unpredictable nature, and so methods are needed to assure their safety.

The outcome of our project is unified assurance technology that can be applied to engineer safe autonomous robots, which will be validated through application to industrial demonstrators. This assurance platform will have a transformative effect in the field of safety assurance for autonomous robots by harnessing results from automated formal verification to produce safety cases undergirded by specific mathematical guarantees of their consistency and adequacy of the evidence. In particular, our software will provide a potential route to regulatory acceptance for autonomous robots, through the production of internally verified safety certificates. Moreover, automating the safety process provides a means to dynamically re-certify a robot when some of the underlying behavioural models change, perhaps due to machine learning, which could provide the disruptive development of self-certifying autonomous robots.

The economic and societal impacts of this work will be mainly realised through industrial collaboration. Provision of advanced automated techniques for assurance has the potential to open a variety of new markets, by supporting both consumer trust in novel AR technology, and regulatory acceptance. Our industrial demonstrators will enable us to translate our scientific results from academia to industry. Our partners provide us with a broad spectrum of players within the fields of safety, verification, and autonomous systems in the complementary areas of railways, marine, automotive, and aerospace. Through regular collaboration, and supported by our demonstrator repository and technology, our project will have a positive impact on industrial certification. It will reduce time to market, through virtual prototyping, and thus provide cost reduction. It will also improve confidence in correctness of safety cases, improve productivity, and prevent costly corrections at the engineering phase. Our industrial partners will periodically trial our technology and provide feedback to enable appropriate alignment.

Our partners are ClearSy, DRisQ, and UTRC, who will support complementary demonstrators. DRisQ, based in Malvern, are safety and certification experts, with a portfolio of existing formal verification solutions, which have been applied to robotics. They are well placed to both provide requirements to our assurance framework, and also potentially to link with their products. United Technologies Research Centre (UTRC), in Ireland, is the research and innovation division of United Technologies (UTC). UTC is multinational conglomerate that manufactures products in several areas, including the aerospace domain, and own the famous Pratt & Whitney aircraft engine brand. They are therefore experts in certification of large scale aerospace systems, including UAVs. ClearSy, based in France, specialises in the production of safety-critical systems and software, and are experts in railway certification. They have worked on major railway projects in São Paulo, Stockholm, and France, including driverless trains. Successful application our technology within these industries will act as a springboard for future commercial exploitation, such as a start-up company which supports our technology.

Publications

10 25 50

publication icon
Foster S (2020) Unifying theories of reactive design contracts in Theoretical Computer Science

publication icon
Foster S (2021) Automated verification of reactive and concurrent programs by calculation in Journal of Logical and Algebraic Methods in Programming

publication icon
Foster S (2020) Unifying semantic foundations for automated verification tools in Isabelle/UTP in Science of Computer Programming

publication icon
Foster S. (2021) Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL in Leibniz International Proceedings in Informatics, LIPIcs

publication icon
Foster, S. (2021) A Sound Type System for Physical Quantities, Units, and Measurements in Archive of Formal Proofs

 
Description We have discovered that the Isabelle system can be used for computer-aided assurance cases, and the development and verification of associated models of cyber-physical systems and autonomous robots. As a part of our work, we have focussed on developing applicable formal methods tools, with a good user experience and automated workflow.

Assurance cases are usually required to demonstrate safety of a critical system, such as autonomous and mobile robots, usually including compliance with international standards. Our Isabelle/SACM framework allows us to encode assurance cases and use formal methods to provide evidence for them. Formal methods are mathematically rigorous techniques that can be used to model and provide evidence for desirable properties of a system.

Our Isabelle/UTP framework also allows to formally verify heterogeneous systems models and code, that can be used in a high assurance development. For example, we can verify graphical state machine models, which makes our technique accessible to software engineers. We can also verify hybrid dynamical systems, which involve both a discrete controller and continuous plant described using differential equations. Our integrated framework therefore allows us to develop mathematically rigorous assurance cases, underpinned by formal verification evidence. We have so far applied this to two case studies: an industrial demonstrator based on an autonomous underwater vehicle, and a secure entry system. We have also developed tools for simulation of formal models, using a mathematically well-founded code generator, which aids in prototyping of formal models for mobile and autonomous robots. This can also provide a route to verified software implementations, and we are currently experimenting to see if we can automatically generate a controller for a small ground robot (the TurtleBot).
Exploitation Route Companies developing safety and security critical systems will be able to use the technology to provide a higher level of rigour in developing and assuring them. We are exploring a KTP in the near future to enable us to perform knowledge transfer.
Sectors Aerospace

Defence and Marine

Digital/Communication/Information Technologies (including Software)

Electronics

Energy

Security and Diplomacy

Transport

URL https://www.cs.york.ac.uk/circus/CyPhyAssure/
 
Description My work has impacted how D-RisQ assure their systems, as reported in a recent report they delivered to the Office for Nuclear Regulation. This work relates to an Autonomous Underwater Vehicle demonstrator, a formal model, assurance case, and verification results in Isabelle/HOL. I am currently also collaborating with Galois Inc. in the US, who are interested to apply my research results (Isabelle/UTP) in their work. Moreover, the research and software has led to the development of a new undergraduate module, called "Assurance and Proof", where students learn how to apply Isabelle in developing high-assurance systems. Results have also been applied in a second-year undergraduate theory module, which has being expanded to include proof and program verification. Finally, we are developed and successfully delivered a Continuing Professional Development (CPD) course for in 2023 to industrial participants, which based upon our results.
Sector Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Education,Energy
Impact Types Societal

Economic

Policy & public services

 
Description Collaboration with DRisQ 
Organisation D-RisQ
Country United Kingdom 
Sector Private 
PI Contribution We have made first steps toward development of a platform for assurance cases using the SACM standard, which we will in the future apply to certification of systems using the DO-178C standard. So far, we developed a first demonstrator for CyPhyAssure based on an autonomous under water vehicle, and its assurance case.
Collaborator Contribution DRisQ have provided requirements for the assurance framework we are developing, and background information on an autonomous boat case study that we will use as a demonstrator. They also provided several documents for a runtime assurance system for an autonomous underwater vehicle that we have developed into a demonstrator and published.
Impact The initial output is a set of requirements for the assurance platform, and in particular the requirement that the tool should support DO-178C, together with information on how DRisQ at present applies this standard. They have also supplied information on the assurance demonstrator, which we will apply our assurance framework to, once the latter has been developed. We also had a joint paper published in 2020 entitled "Formal Model-Based Assurance Cases in Isabelle/SACM", and we used their case study in a further paper entitled "Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles" in 2020.
Start Year 2018
 
Description Collaboration with Seoul National University 
Organisation Seoul National University
Country Korea, Republic of 
Sector Academic/University 
PI Contribution During a research visit to Seoul National University, I worked with Prof. Chung-Kil Hur from the Software Foundations group. This led to the implementation of the "Interaction Trees" Isabelle/HOL library, and an associated publication to CONCUR 2021. I contributed the knowledge on the CSP process algebra and RoboChart, and their use in modelling cyber-physical systems.
Collaborator Contribution Prof. Hur introduced me to Interactions Trees, and helped me to develop coinductive proofs, which are essential to this kind of verification.
Impact "Interaction Trees" Software CONCUR 2021 Publication "Formally Verified Simulations of State-rich Processes using Interaction Trees in Isabelle/HOL"
Start Year 2020
 
Description Collaboration with UTRC 
Organisation United Technologies Research Center (UTRC)
Country United States 
Sector Private 
PI Contribution We have presented our work at United Technologies Research Centre in Ireland (our industrial partner), and have begun to develop a demonstrator for our assurance framework. We also hosted a research visit from one of their staff.
Collaborator Contribution UTRC have provided case study materials for a cyber-security assurance case, which we will apply our assurance technology to. They have also been very helpful in understand how assurance cases and formal methods are used for certification in an industrial setting. They also contributed to our CyPhyAssure School on Computer-Aided Assurance in 2019, by providing an industrial lecture.
Impact Industrial Lecture at CyPhyAssure Spring School, 2019. Presentation and Training at UTRC in September 2019 Department Seminar at the University of York from UTRC in February 2020.
Start Year 2018
 
Description Collaboration with Universities of Bremen, Copenhagen, and Sheffield 
Organisation University of Copenhagen
Country Denmark 
Sector Academic/University 
PI Contribution This collaboration developed a verification tool for hybrid systems, and thus cyber-physical systems, in Isabelle/HOL. We contributed a library for shallow expressions in Isabelle/HOL, and additional verification rules for the differential Hoare logic. We also co-wrote the resulting paper.
Collaborator Contribution Knowledge of hybrid systems, implementation of rules for differential Hoare logic, case studies, and paper writing.
Impact FM 2021 paper: "Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs" "Components for Verifying Hybrid Systems in Isabelle/HOL" Software
Start Year 2018
 
Description Collaboration with Universities of Bremen, Copenhagen, and Sheffield 
Organisation University of Sheffield
Country United Kingdom 
Sector Academic/University 
PI Contribution This collaboration developed a verification tool for hybrid systems, and thus cyber-physical systems, in Isabelle/HOL. We contributed a library for shallow expressions in Isabelle/HOL, and additional verification rules for the differential Hoare logic. We also co-wrote the resulting paper.
Collaborator Contribution Knowledge of hybrid systems, implementation of rules for differential Hoare logic, case studies, and paper writing.
Impact FM 2021 paper: "Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs" "Components for Verifying Hybrid Systems in Isabelle/HOL" Software
Start Year 2018
 
Description Collaboration with Universities of Bremen, Copenhagen, and Sheffield 
Organisation Universum Bremen
Country Germany 
Sector Public 
PI Contribution This collaboration developed a verification tool for hybrid systems, and thus cyber-physical systems, in Isabelle/HOL. We contributed a library for shallow expressions in Isabelle/HOL, and additional verification rules for the differential Hoare logic. We also co-wrote the resulting paper.
Collaborator Contribution Knowledge of hybrid systems, implementation of rules for differential Hoare logic, case studies, and paper writing.
Impact FM 2021 paper: "Hybrid Systems Verification with Isabelle/HOL: Simpler Syntax, Better Models, Faster Proofs" "Components for Verifying Hybrid Systems in Isabelle/HOL" Software
Start Year 2018
 
Title Automated Verification of Reactive and Concurrent Programs by Calculation, supporting material 
Description Abstract Event-driven reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber physical systems and autonomous robots, and so verification support for them is highly desirable. We present a verification strategy for concurrent and reactive programs, with a large or infinite state space, utilising algebraic laws for reactive relations. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, which is supported by Kleene algebra, and parallel composition, which allows flexible specification of various concurrency schemes. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He's Unifying Theories of Programming (UTP) semantic framework, which provides soundness guarantees, and practical verification support. Isabelle Formalisation This archive accompanies the JLAMP journal submission, "Automated Verification of Reactive and Concurrent Programs by Calculation". All of the Isabelle/HOL theories needed to support the theorems developed in this paper are included, and also the dependencies from the Archive of Formal Proofs (AFP). This development depends on Isabelle/2019 (from https://isabelle.in.tum.de/). In order to view the theories, you first need to make Isabelle aware of the Isabelle/UTP directly. You can either do this by adding a reference to its absolute path in the ROOTS file of your Isabelle installation, or else by invoking Isabelle on the command line with a command such as:
isabelle jedit -d /path/to/isabelle/utp -l UTP-Circus
The main heap images of interest are UTP, UTP-Reactive-Designs, and UTP-Circus. The first time you invoke the command, you may need to wait for a while to allow Isabelle to build the heap image. You can find the reactive buffer example under tutorial/utp_csp_buffer.thy and further reactive program examples in tutorial/utp_csp_ex.thy. The theories for reactive designs and stateful failure reactive designs may be found under theories/{rea_designs, sf_rdes}. 
Type Of Technology Software 
Year Produced 2019 
Open Source License? Yes  
URL https://zenodo.org/record/3541080
 
Title Automated Verification of Reactive and Concurrent Programs by Calculation, supporting material 
Description Abstract Event-driven reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber physical systems and autonomous robots, and so verification support for them is highly desirable. We present a verification strategy for concurrent and reactive programs, with a large or infinite state space, utilising algebraic laws for reactive relations. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, and thereby facilitate automated proof. Of note is our reasoning support for iterative programs with reactive invariants, which is supported by Kleene algebra, and parallel composition, which allows flexible specification of various concurrency schemes. We illustrate our strategy by verifying a reactive buffer. Our laws and strategy are mechanised in Isabelle/UTP, our implementation of Hoare and He's Unifying Theories of Programming (UTP) semantic framework, which provides soundness guarantees, and practical verification support. Isabelle Formalisation This archive accompanies the JLAMP journal submission, "Automated Verification of Reactive and Concurrent Programs by Calculation". All of the Isabelle/HOL theories needed to support the theorems developed in this paper are included, and also the dependencies from the Archive of Formal Proofs (AFP). This development depends on Isabelle/2019 (from https://isabelle.in.tum.de/). In order to view the theories, you first need to make Isabelle aware of the Isabelle/UTP directly. You can either do this by adding a reference to its absolute path in the ROOTS file of your Isabelle installation, or else by invoking Isabelle on the command line with a command such as:
isabelle jedit -d /path/to/isabelle/utp -l UTP-Circus
The main heap images of interest are UTP, UTP-Reactive-Designs, and UTP-Circus. The first time you invoke the command, you may need to wait for a while to allow Isabelle to build the heap image. You can find the reactive buffer example under tutorial/utp_csp_buffer.thy and further reactive program examples in tutorial/utp_csp_ex.thy. The theories for reactive designs and stateful failure reactive designs may be found under theories/{rea_designs, sf_rdes}. 
Type Of Technology Software 
Year Produced 2019 
Open Source License? Yes  
URL https://zenodo.org/record/3541079
 
Title Components for Verifying Hybrid Systems in Isabelle/HOL 
Description This is a library for verifying hybrid systems using Isabelle/HOL, which is strongly inspired by differential dynamic logic, but goes beyond it in several ways, e.g. addition of matrices and transcendental functions. 
Type Of Technology Software 
Year Produced 2020 
Open Source License? Yes  
Impact It is being used as part of my new undergraduate module "Assurance and Proof". 
URL https://github.com/isabelle-utp/Hybrid-Verification
 
Title Formal Model-Based Assurance Cases in Isabelle/SACM, supporting materials 
Description Abstract Isabelle/SACM is a tool for automated construction of model-based assurance cases with integrated formal methods, based on the Isabelle proof assistant. Assurance cases show how a system is safe to operate, through a human comprehensible argument demonstrating that the requirements are satisfied, using evidence of various provenances. They are usually required for certification of critical systems, often with evidence that originates from formal methods. Automating assurance cases increases rigour, and helps with maintenance and evolution. In this paper we apply Isabelle/SACM to a fragment of the assurance case for an autonomous underwater vehicle demonstrator. We encode the metric unit system (SI) in Isabelle, to allow modelling requirements and state spaces using physical units. We develop a behavioural model in the graphical RoboChart state machine language, embed the artifacts into Isabelle/SACM, and use it to demonstrate satisfaction of the requirements. Isabelle Formalisation This archive accompanies the FormaliSE 2020 paper "Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study". The larger of the two files contains a Linux distribution of Isabelle2019 with all the additional files needed to start Isabelle/SACM and see the results presented in the paper. The archive also Isabelle/DOF 1.0 (from Prof. Achim Brucker and Prof. Burkhart Wolff), Isabelle/UTP, and several Archive of Formal Proofs (AFP) entries that our development depends upon. These theories are redistributed under the terms of the 2 and 3 clause BSD license. The smaller file contains only those Isabelle files directly related to the LRE case study. In order to get started, extract the larger archive to a suitable directory, and then from here execute
bin/isabelle jedit -l RoboChart-Assurance
This will start Isabelle and build several session heap images, including Isabelle/DOF and RoboChart. Once finished, the assurance case example can be found under src/CyPhyAssure/AUV/LRE/LRE.thy, and the various theory files it imports. In particular, the state machine can be found in LRE_Beh.thy. 
Type Of Technology Software 
Year Produced 2020 
Open Source License? Yes  
URL https://zenodo.org/record/3739236
 
Title Formal Model-Based Assurance Cases in Isabelle/SACM, supporting materials 
Description Abstract Isabelle/SACM is a tool for automated construction of model-based assurance cases with integrated formal methods, based on the Isabelle proof assistant. Assurance cases show how a system is safe to operate, through a human comprehensible argument demonstrating that the requirements are satisfied, using evidence of various provenances. They are usually required for certification of critical systems, often with evidence that originates from formal methods. Automating assurance cases increases rigour, and helps with maintenance and evolution. In this paper we apply Isabelle/SACM to a fragment of the assurance case for an autonomous underwater vehicle demonstrator. We encode the metric unit system (SI) in Isabelle, to allow modelling requirements and state spaces using physical units. We develop a behavioural model in the graphical RoboChart state machine language, embed the artifacts into Isabelle/SACM, and use it to demonstrate satisfaction of the requirements. Isabelle Formalisation This archive accompanies the FormaliSE 2020 paper "Formal Model-Based Assurance Cases in Isabelle/SACM: An Autonomous Underwater Vehicle Case Study". The larger of the two files contains a Linux distribution of Isabelle2019 with all the additional files needed to start Isabelle/SACM and see the results presented in the paper. The archive also Isabelle/DOF 1.0 (from Prof. Achim Brucker and Prof. Burkhart Wolff), Isabelle/UTP, and several Archive of Formal Proofs (AFP) entries that our development depends upon. These theories are redistributed under the terms of the 2 and 3 clause BSD license. The smaller file contains only those Isabelle files directly related to the LRE case study. In order to get started, extract the larger archive to a suitable directory, and then from here execute
bin/isabelle jedit -l RoboChart-Assurance
This will start Isabelle and build several session heap images, including Isabelle/DOF and RoboChart. Once finished, the assurance case example can be found under src/CyPhyAssure/AUV/LRE/LRE.thy, and the various theory files it imports. In particular, the state machine can be found in LRE_Beh.thy. 
Type Of Technology Software 
Year Produced 2020 
Open Source License? Yes  
URL https://zenodo.org/record/3739235
 
Title Interaction Trees 
Description A library for verification and animation of sequential and concurrent systems based in Isabelle/HOL. 
Type Of Technology Software 
Year Produced 2021 
Open Source License? Yes  
Impact This library has been integral to a new undergraduate module, called Assurance and Proof. 
URL https://github.com/isabelle-utp/interaction-trees
 
Title Isabelle/SACM 
Description Isabelle/SACM is an implementation of the OMG standard "Structure Assurance Case Metamodel". It allows the development of assurance cases to support certification of critical systems. 
Type Of Technology Software 
Year Produced 2019 
Impact We have developed two case studies: one based on a Tokeneer secure entry system, and a second based on an autonomous underwater vehicle in partnership with D-RisQ. 
 
Title Isabelle/UTP 
Description Hoare and He's Unifying Theories of Programming is a framework for construction of denotational semantic meta-models for a variety of programming languages based on an alphabetised relational calculus. Isabelle/UTP is an implementation of their framework based in Isabelle/HOL. It can be used to formalise semantic building blocks for programming language paradigms (based on UTP theories), prove algebraic laws of programming, and then use these laws to construct program verification tools. 
Type Of Technology Software 
Year Produced 2023 
Open Source License? Yes  
Impact The software was applied to verification of a fan control unit controller, and a railway signalling system as part of the previous INTO-CPS EU project. It is currently being applied to model autonomous robots. 
URL https://isabelle-utp.york.ac.uk/
 
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 Postgraduate students
Results and Impact 60 participants attended the CyPhyAssure School, which will took place at the Department of Computer Science, University of York, March 19th-22nd, 2019. The primary aim of the school is to engage young researchers with the CyPhyAssure project, whilst educating them in the latest assurance and verification techniques. We hosted leading academics from Canada, Europe, and the UK to give lectures on a variety of related topics. A number of industrial participants also presented research challenges in order to provide connections between academia and industry, and in particular to focus the activities of the former. There was several panel discussions, break-out sessions, and the opportunities for young researchers to present their work to the industrial and academic participants.
Year(s) Of Engagement Activity 2019
URL https://www.cs.york.ac.uk/circus/CyPhyAssure/school/
 
Description Presentation Hybrid Systems Workshop, Chongqing 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact Simon Foster gave a talk at a workshop on Hybrid Systems in UTP, based on the CyPhyAssure technology, in Chongqing, China, in October 2018.
Year(s) Of Engagement Activity 2018
 
Description Presentation at CONCUR 2021 conference 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact I presented my paper on "Formally Verified Simulations of State-Rich Processes Using Interaction Trees in Isabelle/HOL" at the CONCUR 2021 online conference.
Year(s) Of Engagement Activity 2021
URL https://qonfest2021.lacl.fr/concur21.php
 
Description Presentation at FormaliSE 2020 Conference 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact We gave a presentation on our paper "Formal Model-based Assurance Cases in Isabelle/SACM" at the online FormaliSE 2020 conference. Around 30 people attended, and the presentation is available on YouTube.
Year(s) Of Engagement Activity 2020
URL https://www.youtube.com/watch?v=KJshdwgjRTk
 
Description Presentation at ICECCS 2020 Conference 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact We gave a presentation on our paper "Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles" at ICECCS 2020, a core A venue. The presentation is available on YouTube.
Year(s) Of Engagement Activity 2021
URL https://www.youtube.com/watch?v=URPb_8XVGr8
 
Description Presentation at UTP 2019 Conference 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Professional Practitioners
Results and Impact I presented our paper "Hybrid Relations in UTP" at the 2019 UTP Symposium in Porto, Portugal. Attendance was around 30 people. There were several interesting questions afterwards from academics attending the presentation.
Year(s) Of Engagement Activity 2019
URL https://easychair.org/smart-program/UTP2019/2019-10-08.html#talk:132623
 
Description Presentation at WG 2.3 on Programming Methodology 
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 Simon Foster gave a presentation on the work so far of the CyPhyAssure project.
Year(s) Of Engagement Activity 2019
 
Description Presentation at iFM 2019 Conference 
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 the presentation of our paper "Isabelle/SACM: Computer-Assisted Assurance Cases with Integrated Formal Methods" at the iFM conference in Bergen, Norway. Around 50 people attended, and the talk lead to a collaboration with the University of Paris-Saclay.
Year(s) Of Engagement Activity 2020
URL https://easychair.org/smart-program/iFM2019/2019-12-04.html#talk:138716
 
Description Seminar about Animation of RoboChart with Interaction Trees to RoboStar group 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach Local
Primary Audience Professional Practitioners
Results and Impact I gave a seminar about "Animation of RoboChart with Interaction Trees" to the RoboStar group in York.
Year(s) Of Engagement Activity 2021
 
Description Tutorial on CyPhyAssure Technology and Results 
Form Of Engagement Activity A talk or presentation
Part Of Official Scheme? No
Geographic Reach International
Primary Audience Postgraduate students
Results and Impact We gave a 1.5 hour lecture on the CyPhyAssure outputs to a group of around 20 postgraduate students as part of the "Safer Autonomous Systems" European Training Network.
Year(s) Of Engagement Activity 2020
URL https://www.youtube.com/watch?v=OmlnLNIaMtw