A Layered Approach to Polygon Processing for Safety-Critical Embedded Systems

Embedded systems have become ubiquitous in everyday life, and especially in the automotive industry. New applications challenge their design by introducing a new class of problems that are based on a detailed analysis of the environmental situation. Situation analysis systems rely on models and algorithms of the domain of computational geometry. The basic model is usually an Euclidean plane, which contains polygons to represent the objects of the environment. Usual implementations of computational geometry algorithms cannot be directly used for safety-critical systems. First, a strict analysis of their correctness is indispensable and second, nonfunctional requirements with respect to the limited resources must be considered. This thesis proposes a layered approach to a polygon-processing system. On top of rational numbers, a geometry kernel is formalised at first. Subsequently, geometric primitives form a second layer of abstraction that is used for plane sweep and polygon algorithms. These layers do not only divide the whole system into manageable parts but make it possible to model problems and reason about them at the appropriate level of abstraction. This structure is used for the verification as well as the implementation of the developed polygon-processing library.
Eingebettete Systeme sind in vielen Bereichen unseres heutigen Alltags mittlerweile unersetzlich. Ein sehr wichtiger Anwendungsbereich ist unter anderem die Automobilindustrie. Der Entwurf dieser Systeme wird durch neue Anwendungen und Anforderungen vor neue Herausforderungen gestellt. So besteht der Wunsch nach Systemen zur Situationsanalyse. Diese basieren im Allgemeinen auf Modellen und Algorithmen der algorithmischen Geometrie. Üblicherweise wird die Umgebung als Euklidische Ebene modelliert, in der Polygone verschiedene Objekte der Umgebung repräsentieren. Übliche Implementierungen von Algorithmen der algorithmischen Geometrie sind nicht ohne weiteres für den Einsatz auf sicherheitskritischen eingebetteten Systemen geeignet. Zum einen fordern die hohen Sicherheitsanforderungen eine genaue Untersuchung der Korrektheit der Algorithmen. Zum anderen müssen nichtfunktionale Eigenschaften betreffend der begrenzten Ressourcen berücksichtigt werden. Diese Dissertation schlägt ein schichtbasiertes Polygonverarbeitungssystem vor. Auf der Basis von rationalen Zahlen, wird ein Geometrie-Kernel formalisiert. Darauf aufbauend bilden geometrische Primitive eine weitere Abstraktionsebene, die für Plane-Sweep-Algorithmen und Polygone benutzt werden. Die Aufteilung in Schichten unterteilt das System nicht nur in handhabbare Teile, sondern ermöglicht es auch, auftretende Probleme auf den jeweils geeigneten Abstraktionsniveau zu betrachten. Dabei wird die Struktur konsequent in der Verifikation wie auch in der Implementierung der entwickelten Polygonverarbeitungsbibliothek eingesetzt.