Universität Bremen  
  FB 3  
  Group BKB > Publications > Search > Deutsch

Publications Search - Details

Publication type: Article
Author: Holger Täubig, Udo Frese, Christoph Hertzberg, Christoph Lüth, Stefan Mohr, Elena Vorobev, Dennis Walter
Title: Guaranteeing Functional Safety: Design for Provability and Computer-Aided Verification
Volume: 32
Page(s): 303 – 331
Journal: Autonomous Robots
Number: 3
Year published: 2012
Abstract: When autonomous robots begin to share the human living and working spaces, safety becomes paramount. It is legally required that the safety of such systems is ensured, e.g. by certification according to relevant standards such as IEC61508. However, such safety considerations are usually not addressed in academic robotics. In this paper we report on one such successful endeavour, which is concerned with designing, implementing, and certifying a collision avoidance safety function for autonomous vehicles and static obstacles. The safety function calculates a safety zone for the vehicle, depending on its current motion, which is as large as required but as small as feasible, thus ensuring safety against collision with static obstacles. We outline the algorithm which was specifically designed with safety in mind, and present our verification methodology which is based on formal proof and verification using the theorem prover Isabelle. The implementation and our methodology have been certified for use in applications up to SIL3 of IEC61508 by a certification authority (TÜV Süd Rail GmbH, Germany). Throughout, issues we recognised as being important for a successful application of formal methods in robotics are highlighted. Moreover, we argue that formal analysis deepens the understanding of the algorithm, and hence is valuable even outside the safety context.
PDF Version: http://www.informatik.uni-bremen.de/agebv/downloads/published/Taubig2012_AR_author.pdf
Keywords: collision detection Functional Safety Formal Verification Certification IEC 61508 Braking Model Mathematical Proof
Status: Reviewed
Last updated: 18. 04. 2012

 Back to result list
Author: Automatically generated page
  Group BKB 
Last updated: February 23, 2006   impressum