CyPhyAssure Spring School

The 2019 CyPhyAssure School has now finished. Thank you everyone for attending and supporting this event!

Call for Participation

Department of Computer Science, University of York, 19th-22nd March, 2019

Join us in March 2019 to attend the first CyPhyAssure Spring School on computer-assisted assurance, targetted at early stage researchers.

Hear from world-leading academics speaking on assurance, robotics, and formal methods
Build your knowledge of a variety of computer-assisted assurance techniques
Develop new collaborations with industry and other academic institutions

– Simon Foster and Mario Gleirscher (co-organisers)

Background

“How can we use integrated formal methods to the maximum advantage for computer-assisted assurance of autonomous robots?”

Robots and autonomous systems (RAS) are no longer isolated from humans by walls and safety cages. They increasingly inhabit the spaces in which we live and work. Consequently, they must be engineered so that they are able to perform their jobs without impacting the safety of the humans around them. There is a need to assure us that these systems have been developed using rigorous techniques that ensure safe and predictable behaviour. As the Assuring Autonomy International Programme at York makes clear, this is a major challenge with many critical barriers that must be overcome.

We believe that formal methods have a great deal to offer in supporting assurance activities through the use of model-based development and verification tools. Such tools offer both a high degree of automation, and also mathematically principled results that can be used to substantiate safety claims. Nevertheless, in order for formal methods research to be exploited in RAS assurance, it is important to appreciate the greater context of safety certification, the specific challenges of RAS, and also the problems industry is facing.

Who should attend?

Our primary audience is early stage researchers who have a focus on computer-assisted assurance for autonomous robots. Academics and industrial practitioners who are interested in this area are also welcome.

Lectures

For more details on each lecture, please see this page. The timetable for the school be found here.

Formal Methods for Certification of Control Software and Potential for their Successful Application in Autonomous Robot Control. Prof. Alan Wassyng, McMaster University.
Gaining Confidence in the Correctness of Robotic and Autonomous Systems. Prof. Kerstin Eder, Bristol University.
Assurance of Cyber-Physical Systems using Interactive Theorem Proving. Prof. Burkhart Wolff, University Paris-Saclay.
Arguing Safety with the Structured Assurance Case Metamodel. Prof. Tim Kelly, University of York.
Robotics – Autonomy, Verification, and Responsibility. Prof. Michael Fisher, University of Liverpool.
Critical Barriers to Assuring Autonomous Robots. Prof. John McDermid, University of York.
Assurance challenges for robotics and AI in nuclear fusion. Robert Skilton, Lead Technologist at RACE.
Second Generation Model-based Testing – Provably Strong Testing Methods for the Certification of Autonomous Systems. Prof. Jan Peleska, University of Bremen.
RoboChart and RoboSim: Verified Simulation for Robotics. Prof. Ana Cavalcanti, University of York.
Challenges of Modelling, Verifying, and Assuring a Robot Assistant. Dr Clare Dixon, University of Liverpool.
Dynamic Assurance of Safety. Dr. Ibrahim Habli, University of York.
Model-based hazard analysis of human-robot interactions with HAZOP-UML. Prof. Jérémie Guiochet, LAAS-CNRS, University of Toulouse III.

Teaching will be conducted by both mandatory lectures and also optional “breakout” sessions that will occur at intervals during the school. The breakouts will allow more in-depth and hands-on learning for topics of interest which can be selected by the participants. Industrial practioners are also invited to give short 10-15 talks on the assurance challenge they are facing, and to pose research questions. Early stage researchers will also have the opportunity to deliver short talks on their work and interests to the audience. Finally, we will also have question and answer panel sessions to faciliate discussion.

Isabelle/UTP Tutorial

In concert with the school, we are also planning an optional one-day tutorial on Friday 22nd of March, focusing on the use of the Isabelle/UTP verification framework. This tool is being further developed at York as part of the CyPhyAssure project, and can be used for both formation of heterogeneous semantic models and their application to verification. More details on this to follow soon.

SCDR Course

In the week following the CyPhyAssure school, the Safety Case Development and Review (SCDR) course will also take place at the University of York, taught by Prof. Tim Kelly. You can find out more and book your place here. If you are travelling to York for the CyPhyAssure school, and could stay for an extra week, then this would be a very useful companion course to take.

Travel and Accommodation

The school will take place at the Department of Computer Science at the University of York. Please see this page for information on travelling to the school venue.

You can find below a list of potential low cost hotels. The first is close to campus, and the rest are in the city centre. You can take the 66 or 66a busses from the centre to campus.