Sciweavers

Share
EUC
2005
Springer

Dependable Polygon-Processing Algorithms for Safety-Critical Embedded Systems

11 years 7 months ago
Dependable Polygon-Processing Algorithms for Safety-Critical Embedded Systems
Algorithms that process geometric objects become more and more important for many safety-critical embedded systems, e.g. for motion planning or collision detection, where correctness is indispensable. The main challenge to demonstrating correctness is the consistent handling of degenerate cases like collinear line segments. In this paper, we therefore propose the use of an interactive theorem prover to develop dependable geometry algorithms for safety-critical embedded systems. Our solution is based on the use of a three-valued logic to make degenerate cases explicit. Using the theorem prover, we are not only able to prove the correctness of the obtained algorithms, but also to directly derive a software library of provably correct geometry algorithms for safety-critical applications.
Jens Brandt, Klaus Schneider
Added 27 Jun 2010
Updated 27 Jun 2010
Type Conference
Year 2005
Where EUC
Authors Jens Brandt, Klaus Schneider
Comments (0)
books