| الوصف: |
Verified algorithms play an important role in the context of different applications from various areas of science. An open question is the interoperability between different verified range arithmetics and their numerical comparability. In this thesis, a theoretical framework is provided for interoperable handling of the arithmetics without altering their verification features. For this purpose, we formalize the arithmetics using a heterogeneous algebra. Based on this algebra, we introduce the concept of function representation objects. They characterize a mathematical function by inclusion functions in different arithmetics and allow for representing particular features of the function (e.g., differentiability). The representation objects allow us to describe problems by functional and relational dependencies so that different verified methods can be used interchangeably. On this basis, we develop a new verified distance computation algorithm which can handle non-convex objects. Furthermore, a verified global optimization algorithm is adapted so that it can use the different methods made accessible by the function representation objects. Moreover, we formalize and improve interval-based hierarchical structures which are used by both algorithms. To evaluate our approach, we provide a prototypical implementation and perform fair numerical comparisons between the different arithmetics. Finally, we apply the framework to relevant application cases from biomechanics and modeling, simulation and control of fuel cells. We demonstrate that our implementation supports parallel computations on the CPU and GPU and show that it can be extended by interfacing additional external IVP solver libraries. Originally published in Dr. Hut Verlag, ISBN: 978-3-8439-1625-7 Verifizierte numerische Verfahren spielen in zahlreichen Anwendungskontexten eine wichtige Rolle. Hierbei ist die Interoperabilität zwischen den verschiedenen verwendeten Wertebereichsarithmetiken sowie ihre numerische Vergleichbarkeit eine offene Frage. In dieser Arbeit wird ein theoretisches Rahmenwerk zur Verfügung gestellt, welches die Interoperabilität zwischen den Arithmetiken unter Beibehaltung der Verifikationseigenschaften sicherstellt. Hierzu werden die Arithmetiken mittels einer heterogenen Algebra formalisiert und darauf aufbauend das Konzept der "Funktionsrepräsentationsobjekte" eingeführt. Damit können mathematische Funktionen mittels Inklusionsfunktionen in unterschiedlichen Arithmetiken charakterisiert und ihre Eigenschaften (z.B. Differenzierbarkeit) dargestellt werden. Mit Hilfe der Repräsentationsobjekte ist es möglich Problemstellungen, die mittels funktionaler und relationaler Beziehungen repräsentierbar sind, derart zu beschreiben, dass unterschiedliche verifizierte Methoden eingesetzt werden können. Aufbauend hierauf wird ein neuer Algorithmus zur verifizierten Abstandsberechnung zwischen nicht konvexen Körpern entwickelt. Weiterhin wird ein verifizierter globaler Optimierungsalgorithmus derart angepasst, dass er die durch Funktionsrepräsentationsobjekte zugänglich gemachten, unterschiedlichen Methoden flexibel nutzen kann. Beide Algorithmen greifen auf in das Rahmenwerk integrierte Hilfsdatenstrukturen zur intervallbasierten hierarchischen Zerlegung zurück, die im Kontext dieser Arbeit formalisiert und verbessert werden. Zur Evaluation wird der Gesamtansatz prototypisch implementiert. Hierbei werden nicht nur numerische Vergleiche zwischen den unterschiedlichen Arithmetiken durchgeführt, sondern auch relevante Anwendungsfälle aus der Biomechanik und der Simulation von Brennstoffzellen behandelt. Weiterhin wird demonstriert, dass die vorliegende Implementierung parallele Berechnungen auf der CPU und GPU unterstützt und durch die Anbindung weiterer externer AWP Löserbibliotheken flexibel erweiterbar ist. |
