Experiences in Applying Formal Verification in Robotics

11 years 11 months ago
Experiences in Applying Formal Verification in Robotics
Formal verification efforts in the area of robotics are still comparatively scarce. In this paper we report on our experiences with one such effort, which was concerned with designing, implementing and certifying a safety function for autonomous vehicles and robots. We outline the algorithm which was specifically designed with safety through formal verification in mind, and present our verification methodology, which is based on formal proof and verification using the theorem prover Isabelle. The necessary normative measures that are covered are discussed. The algorithm and our methodology have been certified for use in applications up to SIL 3 of IEC 61508-3 by a certification authority. 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,...
Dennis Walter, Holger Täubig, Christoph L&uum
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Authors Dennis Walter, Holger Täubig, Christoph Lüth
Comments (0)