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.


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.


safecomp2010.pdf (pdf, 518 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence