The goal of the CyPhyAssure project is to develop a methodology for compositional assurance of autonomous robots. This will be supported by a mechanical safety case platform for robotic multi- models, and associated verification tools.
The recent drive for the adoption of robotics and autonomous systems (RAS) into human society means that such systems have become safety critical. In order to gain regulatory acceptance it is necessary to produce an assurance case with a clear and unarguable proof of safety supported by evidence.
There are several substantial challenges in assuring the safety of RAS. Assurance cases associated with standards like IEC 61508 and DO-178C can be laborious to create. They are complicated to maintain and evolve, and must be rigorously checked by the evaluation process in order to ensure that all obligations are met.
Production of evidence is costly and time consuming, particularly if a physical prototype is required. Physical prototyping is often incomplete since it is difficult to test all possible real-world scenarios. A solution lies in the use of virtual prototyping using formal models of a hypothetical system’s behaviour to rigorously design and analyse them.
However, autonomous robot models are particularly challenging due to the need to model the software and hardware in a complex physical environment. In order to overcome the “reality gap”, the environment model must account for continuous dynamics, ambient phenomena, and uncertainty, all of which are significant challenges for verification.
Similarly, it is also vital to record an argument of why a given formal model is an adequate represention of its real-world counterpart. By its very nature, such an argument is informal in nature, and so assurance cases must seamlessly integrate both formal and informal artefacts.
Our research hypothesis is that computer-assisted tools for the construction of assurance cases and production of evidence using integrated formal methods will be able to meet the challenge of proving autonomous robots safe.
Machine-checked assurance cases will greatly increase confidence in their sufficiency, and also support their maintenance and evolution through modularisation of arguments and evidence. Integration of formal methods, in particular modern verification tools, will also enable automation of the evidence gathering process, and highlight potential problems when an assurance case changes.
We envisage the need for a long-term research programme that will develop comprehensive mechanised assurance and verification techniques and tools to achieve these objectives.
The goal of the CyPhyAssure project is to develop a methodology for compositional assurance of autonomous robots. This will be supported by a mechanical safety case platform for robotic multi- models, and associated verification tools.
The platform will be based in Isabelle, and will support both construction of arguments and production of supporting evidence from formal verification tools. We will validate it by application to assurance demonstrators from our industrial partners, and support our technology with an outreach programme.
Our methodology is founded on model-based modular assurance; individual architectural elements can be described in a number of different modelling languages, with their behavioural semantics manifested using FMI (Functional Mockup Interface).
We will mechanise denotational semantics for a number of modelling languages using our Isabelle/UTP framework, which will facilitate the production of verification tools. Safety requirements can then be refined, decomposed, and the resulting safety goals apportioned to constituent models. These goals can finally be discharged using a variety of verification tools.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599
