The Importance of Being Formal

Udo Frese, Daniel Hausmann, Christoph Lüth, Holger Täubig, Dennis Walter

In: M. Huhn , H. Hungar (Hrsg.). Proceedings of the First Workshop on Certification of Safety-Critical Software Controlled Systems. International Workshop on Certification of Safety-Critical Software Controlled Systems (SafeCert-08) befindet sich ETAPS'08 March 29 Budapest Hungary Seiten 57-70 238 4 Elsevier B.V. 2009.


This paper presents work in the context of the certification of a safety component for autonomous service robots, and investigates the potential advantages offered by formally modelling the domain knowledge, specification and implementation in a theorem prover in higher-order logic. This allows safety properties to be stated in an abstract manner close to textbook mathematics. The automatic proof checking alleviates correctness concerns, and provides a seamless development process from high-level safety requirements down to concrete implementation. Moreover, the formalisation can be checked for correctness automatically, and the certification review process can focus on the correctness of the specification and safety cases.


safecert08.pdf (pdf, 338 KB )

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