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.