This thesis is about coalgebraic methods in software specification and verification. It extends known techniques of coalgebraic specification to a more general level to pave the way for real world applications of software verification. There are two main contributions of the present thesis: 1. Chapter 3 proposes a generalisation of the familiar notion of coalgebra such that classes containing methods with arbitrary types (including binary methods) can be modelled with these generalised coalgebras. 2. Chapter 4 presents the specification language CCSL (short for Coalgebraic Class Specification Language), its syntax, its semantics, and a prototype compiler that translates CCSL into higher-order logic. / Die Dissertation beschreibt coalgebraische Mittel und Methoden zur Softwarespezifikation und -verifikation. Die Ergebnisse dieser Dissertation vereinfachen die Anwendung coalgebraischer Spezifikations- und Verifikationstechniken und erweitern deren Anwendbarkeit. Damit werden Softwareverifikation im Allgemeinen und im Besonderen coalgebraische Methoden zur Softwareverifikation der praktischen Anwendbarkeit ein Stück nähergebracht. Diese Dissertation enthält zwei wesentliche Beiträge: 1. Im Kapitel 3 wird eine Erweiterung des klassischen Begriffs der Coalgebra vorgestellt. Diese Erweiterung erlaubt die coalgebraische Modellierung von Klassenschnittstellen mit beliebigen Methodentypen (insbesondere mit binären Methoden). 2. Im Kapitel 4 wird die coalgebraische Spezifikationssprache CCSL (Coalgebraic Class Specification Language) vorgestellt. Die Bescheibung umfasst Syntax, Semantik und einen Prototypcompiler, der CCSL Spezifikationen in Logik höherer Ordnung (passend für die Theorembeweiser PVS und Isabelle/HOL) übersetzt.

Zentrales Thema des Oberflächenkolloquiums 2017 ist die anwendungsorientierte, funktionale geometrische Spezifikation und Messung der Oberfläche im Sinne der Gesamtgeometrie. Neben der Mikrogestalt wird dabei das Zusammenwirken mit der Makrogeometrie zur Erfüllung funktionaler Anforderungen diskutiert. Interessante Beiträge aus Industrie und Wissenschaft zeigen sowohl Lösungen als auch Probleme verschiedenster Fachbereiche auf. / Key issue of the International Colloquium on Surfaces 2017 is the application‐oriented, functional geometrical specification and verification of surfaces as part of the entire geometry. Therefore we discuss the interaction of micro and macro geometry, to fulfill functional requirements. Interesting articles from industry and research point out solutions as well as problems from multifaceted fields of expertise.

In der vorliegenden Arbeit wird der Entwurf von Funkempfängern für digitale Modulation betrachtet. Dabei liegt der Schwerpunkt der Betrachtungen beim Finden einer geeigneten Empfängerarchitektur, der Spezifikation der einzusetzenden Bausteine, der Auswahl einer geeigneten Arbeitsfrequenz und eines passenden Modulationsverfahrens sowie der Festlegung einer dem Einsatzzweck angepaßten Datenrate. Ein wesentlicher Punkt ist die der Empfangsaufgabe angepaßte gewichtete Bekämpfung der auftretenden Störbeiträge. Dafür werden zunächst Grundlagen, wie wichtige Modulationsverfahren, Empfängerarchitekturen sowie Bestimmungsgleichungen für Parameter eingeführt. Darauf aufbauend wird eine allgemeingültige Methode zum Entwurf von Funkempfängern für digitale Modulation entwickelt. Diese Methode kann stets angewendet werden, wenn ein Empfänger für digitale Modulation entworfen werden soll. Wesentliche zu berücksichtigende Einsatzparameter und Randbedingungen werden an passender Stelle in den Entwurf einbezogen und eine entsprechend angepaßte Lösung wird weiterverwendet. Die Entwurfsmethode eignet sich sowohl für den freien Empfängerentwurf als auch für Entwürfe, die sich an der Einhaltung von Standards orientieren müssen. Der Kerngedanke besteht darin, das alle Störeinflüsse einen gleichgroßen Beitrag zur Signalverfälschung liefern sollen. Um dies zu erreichen, werden potentielle Störeinflüsse analysiert und entsprechend ihres Einflusses gewichtet zur weiteren Bestimmung der notwendigen Eigenschaften der Empfängerbaugruppen herangezogen. In der vorliegenden Arbeit wird hauptsächlich der allgemeine Anwendungsfall des freien nicht standardbezogenen Empfängerentwurfes betrachtet. Es wird aufgezeigt, wie durch die Analyse und entsprechende Berücksichtigung einer variablen Anzahl von Störeinflüssen die Eigenschaften der einzelnen Empfängerkomponenten jeweils bestmöglich eingestellt werden können. Diese Methode wird anschließend anhand von verschiedenartigen Beispielen weiter illustriert und ihre erfolgreiche Anwendbarkeit veranschaulicht. Anhand einer Mischerschaltung wird beispielhaft auf grundlegende Ansätze zur Verbesserung der Linearitätseigenschaften eingegangen. Dabei werden spezifische Unterschiede zwischen einer Superhet- bzw. einer Direktmischarchitektur hervorgehoben. Weiterhin wird eine Methode zur Wiederverwendung (Re-Use) von analogen Schaltungen oder ähnlichen Objekten vorgeschlagen. Dabei werden die Schaltungen anhand einer Vorgabe bewertet, und es wird eine Rangfolge aufgestellt. Damit ist gewährleistet, daß die der Vorgabe am besten entsprechende Schaltung gefunden werden kann, auch wenn eine 100%ige Übereinstimmung nicht gegeben ist. Die hierfür notwendigen Bewertungsalgorithmen werden ausführlich dargestellt und ihr jeweiliger Einsatz wird erläutert. Abschließend erfolgt eine überblicksweise Darstellung von Simulationswerkzeugen und -verfahren, die für den Empfängerentwurf bedeutsam sind. Dabei wird hauptsächlich auf die Verbindung von System- und Schaltungsentwurf eingegangen, und es werden bestehende Probleme dargelegt sowie vorhandene Lösungsmöglichkeiten aufgezeigt. Einige im Zusammenhang mit der Simulation interessante Modellierungsgesichtspunkte werden ebenfalls dargestellt.

Univ., Diss.--Zugl.: Oslo, 2007.

Der Elektrik/Elektronik- und der IT-Anteil steigt derzeit in den aktuellen Premium -Fahrzeugen stetig an. Durch den Verbau von immer mehr (hochvernetzten) Steuergeräten im Fahrzeug wird versucht, dem Wunsch der Kunden nach mehr Funktionalität, Sicherheit, etc. gerecht zu werden. Aufgrund der Komplexität und der großen Entwicklungssprünge sind jedoch die neuen Steuergeräte meistens nicht mehr kompatibel mit den Vorgänger-Steuergeräten. Hier ist ein großes Einsparpotenzial vorhanden und dies ist auch der Ansatzpunkt des Forschungsthemas ”CompA“ (Compatibility Analysis of Electronic Control Units), das in diesem Dokument beschrieben wird. Im Rahmen dieses Forschungsthemas wird eine Methode definiert, mit der zwei Steuergeräte auf Rückwärtskompatibilität untersucht werden können. Der Ansatz baut auf drei Schwerpunkten auf: • Definition eines Spezifikationsansatzes zur hinreichenden Beschreibung von Steuergeräten auf Basis eines XML-Schemas. Es werden hierbei sowohl die statischen als auch die dynamischen Eigenschaften abgebildet. Dieser neuartige Spezifikationsansatz bildet die Basis für den nächsten Schwerpunkt. • Definition einer Methode zur Analyse von Rückwärtskompatibilität von Steuergeräten auf Basis eines XML-Schemas. Die Rückwärtskompatibilität zweier Steuergeräte bzw. Systeme wird auf Basis der zugehörigen XML-Dokumente analysiert. Kern der Vergleichsmethode ist hierbei ein effizientes Mapping der XML-Dokumente und ein Experten-Regelwerk. • Definition einer Methode zur Kompatibilitätsanalyse von Message Sequence Charts (MSC). MSCs werden eingesetzt, um dynamisches Verhalten an der Schnittstelle von Steuergeräten zu beschreiben. In diesem Dokument wird ein Ansatz definiert, mit dem MSCs zueinander auf Rückwärtskompatibilität geprüft werden können. Der Vergleich erfolgt auf Basis deterministischer Automaten. Des Weiteren wird im vorliegenden Dokument ein Konzept für eine graphische Benutzeroberfläche (GUI) vorgestellt, die zur Spezifikation von Steuergeräten geeignet ist und sich adaptiv unterschiedlichen Schemata anpasst. Alle vorgestellten Konzepte wurden in einem Software-Tool implementiert und die Gültigkeit an mehreren Beispielen validiert.

Ausgehend von einer modularen Plattform zur Erfassung und Verarbeitung von Sensordaten bereichert die vorliegende Dissertationsschrift den Systementwurf eingebetteter Systeme um neue Facetten. Ihr besonderer Fokus liegt dabei auf rekonfigurierbaren Architekturen und Linux-basierten Systemen. Ein wesentlicher Beitrag ist die Darstellung und Diskussion von Konzepten und Architekturen vorgenannter Systeme durch ihre Betrachtung auf einer hohen Abstraktionsebene. Dazu schafft die Arbeit ein umfassendes Verständnis für Kommunikation und Konfiguration in heterogenen rekonfigurierbaren Systemen und überträgt die Erkenntnisse auf das Linux-Betriebssystem. Es erfolgt außerdem eine systematische Darstellung der etablierten Zusammenhänge und Abläufe beim Software-, Paket- und Versionsmanagement im Linux-Umfeld. Zur Verbesserung des Entwurfsflusses werden Konzepte und ein geeignetes Werkzeug zur High-Level Spezifikation von Linux-Systemen dargestellt. Die in der Arbeit gewonnenen wissenschaftlichen Erkenntnisse werden hinsichtlich praktischer Relevanz evaluiert und durch prototypische Implementierungen verifiziert. / Based on a modular platform for recording and processing of sensor data the present thesis enriches the field of system design of embedded systems with new facets. Its particular focus is on reconfigurable architectures and Linux-based systems. A major contribution is the presentation and discussion of concepts and architectures of aforementioned systems by investigating them on a high level of abstraction. To achieve this, the work creates a comprehensive understanding of communication and configuration in heterogeneous reconfigurable systems. This knowledge is transferred on the Linux operating system. In addition, a systematic presentation of the established relationships and processes in software, package and version management in the Linux environment takes place. To improve the design flow of Linux systems, the thesis presents appropriate concepts as well as a tool for high-level specification of embedded Linux systems. The gained scientific findings are evaluated in terms of practical relevance and verified by prototype implementations.

The specification of a decoder, i.e., a program that translates sentences from one natural language into another, is an intricate process, driven by the application and lacking a canonical methodology. The practical nature of decoder development inhibits the transfer of knowledge between theory and application, which is unfortunate because many contemporary decoders are in fact related to formal-language theory. This thesis proposes an algebraic framework where a decoder is specified by an expression built from a fixed set of operations. As yet, this framework accommodates contemporary syntax-based decoders, it spans two levels of abstraction, and, primarily, it encourages mutual stimulation between the theory of weighted tree automata and the application.

Calif., Univ. of California, Diss.--San Diego, 2004. / Kopie, ersch. im Verl. UMI, Ann Arbor, Mich. - Ent. 3 Beitr.

Wiss. Hochsch.für Unternehmensführung (WHU), Diss.--Vallendar, 2006.

DC, George Washington Univ., Columbian College of Arts and Sciences, Diss.--Washington, 2003. / Kopie, ersch. im Verl. UMI, Ann Arbor, Mich. - Enth. 3 Beitr.