| Publication type: |
Article in Proceedings |
| Author: |
Udo Frese, Daniel Hausmann, Christoph Lüth, Holger Täubig, Dennis Walter |
| Editor: |
M. Huhn, H. Hungar |
| Title: |
The Importance of Being Formal |
| Book / Collection title: |
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), located at ETAPS'08, March 29, Budapest, Hungary |
| Volume: |
238 |
| Page(s): |
57 – 70 |
| Series: |
Electronic Notes in Theoretical Computer Science |
| Number: |
4 |
| Year published: |
2009 |
| Publisher: |
Elsevier Science |
| Abstract: |
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.
|
| PDF Version: |
http://www.informatik.uni-bremen.de/~cxl/papers/safecert08.pdf |
| Keywords: |
software certification formal methods robotics safety Isabelle |
| Status: |
Reviewed |
| Last updated: |
29. 11. 2011 |
|
 |
