Department of Computer Science

Mechanised Assurance for Autonomous Robots

Autonomous robots present opportunities to overcome a number of future societal challenges, and for new exciting business models. However, adoption of such systems raises the important questions of trustworthiness and safety, as they closely interact with humans. Consequently, their benefits can only be harnessed if they acquire both consumer trust and regulatory acceptance. This can be achieved through a certification process that produces a credible case for safety, with tangible evidence. The production of assurance cases for autonomous robots is a challenge, due to the need for complex robotic models coupled with uncertainty in their environment. We believe this challenge can be met by integration of formal methods tools into a unified platform for constructing and validating assurance cases.

The goal of the CyPhyAssure project is, therefore, to develop a methodology for compositional assurance of autonomous robots, supported by a mechanical safety case platform for robotic multi-models, and supporting verification tools. The platform will be based in Isabelle/HOL, 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 program.

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 then can 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