Skip to main content Skip to main navigation

Publication

Experiences in Applying Formal Verification in Robotics

Dennis Walter; Holger Täubig; Christoph Lüth
In: SafeComp 2010 --- 29th International Conference on Computer Safety, Reliability and Security, Proceedings. International Conference on Computer Safety, Reliability and Security (SAFEComp-2010), September 14-17, Vienna, Austria, Pages 347-360, Lecture Notes in Computer Science (LNCS), Vol. 6351, Springer, 2010.

Abstract

In this paper we report on our experiences in applying formal methods, more precisely formal domain modelling and code verification within the theorem prover Isabelle, in the domain of safety-related opto-electronic protective devices. We outline an algorithm that was specifically designed with safety through formal verification in mind. The algorithm has been certified for use in applications up to SIL 3 of IEC 61508 by a certification authority. Our verification methodolody is presented, which has also been accepted for use in safety contexts up to SIL 3, and the necessary normative measures that are covered by its use are discussed. Throughout, issues we recognised as being important for a successful application of formal methods in the domain at hand are highlighted. These pertain to the development process, the abstraction level at which specifications should be formulated, and the interplay between simulation and verification, among others.

Projekte