Domänenspezifische Sprachen (DSLs) sind Software-Sprachen, die speziell für bestimmte Anwendungsdomänen entwickelt wurden. Mithilfe von DSLs können Domänenexperten ihr Domänenwissen auf einem hohen Abstraktionsniveau beschreiben. Wie andere Software-Sprachen auch, benötigen DSLs Sprachwerkzeuge, die Assistenz bei der Erstellung und Verarbeitung von domänenspezifischen Modellen bieten. Eine domänenspezifische Werkbank (DSW) ist ein Software-Werkzeug, welches mehrere solcher Sprachwerkzeuge für eine DSL miteinander integriert. Existierende Werkzeuge, die es erlauben eine DSW aufgrund der Beschreibung einer DSL automatisch generieren zu lassen, unterstützen jedoch nicht die Beschreibung und Generierung von editierbaren Sichten. Eine Sicht ist ein Teil einer DSW, der nur einen bestimmten Aspekt eines Modells darstellt. Diese Dissertation stellt spezielle Modelltransformationssprachen (MTLs) vor, mit denen die Synchronisation von Sichten in einer generierten DSW beschrieben werden kann. Dadurch können DSWs mit editierbaren Sichten mittels existierender Werkzeuge zur Generierung von Sprachwerkzeugen erstellt werden. Dafür wird eine DSW für die Nanophysik-Domäne sowie eine Taxonomie von Synchronisationstypen vorgestellt, welche es erlaubt genau zu bestimmen, welche Art von Modelltransformationen für die Synchronisation von Sichten in dieser Werkbank benötigt werden. Entsprechend dieser Anforderungen werden zwei MTLs entwickelt. Insbesondere wird eine bidirektionale MTL entwickelt. Mit solch einer Sprache kann man eine Relation, welche definiert ob zwei Modelle synchron sind, so beschreiben, dass die entsprechende Synchronisationslogik automatisch abgeleitet werden kann. Die gezeigten MTLs werden als interne DSLs - das heißt eingebettet als ausdrucksstarke Bibliotheken - in der Programmiersprache Scala implementiert. Auf diese Weise kann Scalas Typprüfung genutzt werden, um Transformationen und deren Komposition statisch zu verifizieren. / Domain-specific languages (DSLs) are software languages which are tailored to a specific application domain. DSLs enable domain experts to create domain-specific models, that is, high-level descriptions of domain knowledge. As any other software languages, DSLs rely on language tools which provide assistance for processing and managing domain-specific models. A domain-specific workbench is an integrated set of such tools for a DSL. A recently proposed approach is to automatically generate a domain-specific workbench for a DSL from a description of that DSL. However, existing tools which apply this approach do not support to describe and generate editable domain-specific views. A view is a part of domain-specific workbench that presents only one aspect of a model, for example, its hierarchical structure. This dissertation presents special model transformation languages which support the description of view synchronization in a generated domain-specific workbench. This allows a multi-view domain-specific workbench to be created with existing tools for language tool generation. We present a generated domain-specific workbench for the nanophysics domain and present a taxonomy of synchronization types. This allows us to precisely define what model transformations are required for view synchronization in that workbench. According to these requirements, we develop two transformation languages by adapting existing ones. In particular, we develop a bidirectional transformation language. With such a language one can describe a relation which defines whether two models are in sync and let the synchronization logic be inferred automatically. We implement model transformation languages as internal DSLs - that is, embedded as expressive libraries - in the Scala programming language and use Scala''s type checking for static verification of transformations and their composition.

Durch Kreuzkorrelation von ECoG- und EEG-Signalen hoher Bandbreite (10 - 400 Hz) mit dem Muster eines Amplituden - Zeit - Templates von 10 ms Dauer können Subpotentiale (SP) selektiert werden, die dem sogenannten ?local field potential? ähnlich sind.Diese Ähnlichkeit ergibt sich i. durch den Vergleich mit dem ermittelten Amplituden - Zeit - Template des SP. ii. durch den Vergleich mit der Lage der Quellstrukturen zur ableitenden Elektrode. Die SP - Modulanalyse liefert Potentialverteilung für jede untersuchte Elektrode. Diese ist stets in ein Nahfeld und Fernfelder organisiert, wobei die Polarität des Nahfeld der Polarität des Trigger- SP entspricht und das Fernfeld von entgegengesetzter Polarität ist. Diese Quellstrukturen sind um so kleiner, je geringer der Elektrodenabstand ist. iii. aus der Kohärenz von SP, die im Ableitfeld auftreten. Dafür wurde die SP- Zweikanalkopplungsanalyse entwickelt.Die einzelnen Schritte dieser SP - Methode, die sich aus der SP - event-, SP - Modul- und SP - Zweikanalkopplungsanalyse zusammensetzt, werden beschrieben und an einem Beispiel einer 30 kanaligen subduralen interiktalen ECoG - Ableitung eines Patienten mit fokaler Epilepsie unter drei verschiedenen Bedingungen (normales ECoG, ECoG mit spikes bzw. ECoG mit slow waves) sowie am Beispiel einer 30 kanaligen EEG-Ableitung eines Probanden unter drei verschiedenen kognitiven Anforderungen (relaxierte Wachheit, Kopfrechnen, beim Anhören eines Hörspiels) vergleichend demonstriert. Beide Beispiele sind repräsentativ für zwei größere Untersuchungsreihen. / We obtained subpotentials (SP), similar to so called ?local field potentials? by application of cross - correlation on ECoG- and EEG- Signals with large band width (10 - 400 Hz) with the pattern of an amplitude-time-template with a duration of 10ms. This similarity is given by i. the comparison with obtained amplitude-time-template of the SP ii. the comparison with the position of source- structures to the deriving electrode. The potential distribution is given by the SP - moduleanalysis for each investigated electrode. This SP - module - analysis is always organised in a near- and in a far-field. The polarity of the near-field corresponds to the trigger-SP and the far-field to the opposite. The smaller the source-structure, the lower the distance of the electrodes iii.the coherence of SP in the deriving array The SP - method, consisting of SP - event, SP - module and SP ?two-channel-coupling -analysis? is described. The comparison between an example of an 30 channel subdural interictal derived ECoG of a patient, who was suffering from focal epilepsy, under three conditions (normal ECoG, ECoG with spikes and ECoG with slow-waves) and one of an 30 channel derived EEG of a candidate under three different cognitive demands (relaxed vigilance, doing mental arithmetic, listening to a radio serial) is demonstrated an discussed. Both examples are representatives for two extensive serials.

Globally Asynchronous Locally Synchronous (GALS) Design ist eine Lösung zur Skalierbarkeit und Modularität für die SoC-Integration. Heutzutage ist GALS-Design weit in der Industrie angewendet. Die meisten GALS-Systeme basieren auf Dual-Clock-FIFOs für die Kommunikation Zwischen Taktdomänen. Um Leistungsverluste aufgrund der Synchronisationslatenzzeit zu vermindern, müssen die On-Chip-FIFOs ausreichend groß sein. Dies führt jedoch oft zu erheblichen Kosten-Hardware. Effiziente GALS- Lösungen sind daher vonnöten. Diese Arbeit berichtet unsere neuesten Fortschritte in GALS Design, das auf der Pausierenden Taktung basiert. Kritische Designthemen in Bezug auf Synchronisation-szuverlässigkeit bzw. Kommunikationsfähigkeit sind systematisch und analytisch un-tersucht. Ein lose gekoppeltes GALS Data-Link-Design wird vorgeschlagen. Es unter-stützt metastabilitätsfreie Synchronisation für Sub-Takt-Baum Verzögerungen. Außer-dem unterstützt es kontinuierliche Datenübertragung für High-Throughput-Kommuni-kation. Die Rosten hinsichtlich Energie verbrauch und Chipfläche sind marginal. GALS Design ist eingesetzt, um digitales On-Chip Umschaltrauschen zu verringern. Plesiochron Taktung mit balanciertem Leistungsverbrauch zwischen GALS Blöcken wird insbesondere untersucht. Für M Taktbereiche wird eine Reduzierung um 20lgM dB für die spektralen Spitzen des Versorgungsstroms bei der Takt-Grundfrequenz theoretisch hergcleitet. Im Vergleich zu den bestehenden synchronen Lösungen, geben diese Methode eine Alternative, um das digitale schaltrauschen effektiv zu senken. Schließlich wurde die entwickelte GALS Design Methodik schon bei reale Chip-Implementierungen angewendet. Zwei komplizierte industriell relevante Test-Chips, Lighthouse und Moonrake, wurden entworfen und mit State-Of-The-Art-Technologien hergestellt. Die experimentellen Ergebnisse bzw. / Globally asynchronous locally synchronous (GALS) design presents a solution of scalability and modularity to SoC integration. Today, it has been widely applied in the industry. Most of the GALS systems are based on dual-clock FIFOs for clock domain crossing. To avoid performance loss due to synchronization latency, the on-chip FIFOs need to be sufficiently large. This, however, often leads to considerable hardware costs. Efficient design solutions of GALS are therefore in great demand. This thesis reports our latest progress in GALS design bases on pausible clocking. Critical design issues on synchronization reliability and communication performance are studied systematically and analytically. A loosely-coupled GALS data-link design is proposed. It supports metastability-free synchronization for sub-cycle clock-tree delay, and accommodates continuous data transfer for high-throughput communication. Only marginal costs of power and silicon area are required. GALS design has been employed to cope with the on-chip digital switching noise in our work. Plesiochronous clocking with power-consumption balance between GALS blocks is in particular explored. Given M clock domains, a reduction of 20lgM dB on the spectral peaks of supply current at the fundamental clock frequency is theoretically derived. In comparison with the existing synchronous design solutions, it thus presents an alternative to effective attenuation of digital switching noise. The developed GALS design methodology has been applied to chip implementation. Two complicated industry-relevant test chips, named Lighthouse and Moonrake, were designed and fabricated using state-of-the-art technologies. The experimental results as well as the on-chip measurements are reported here in detail. We expect that, our work will contribute to the practical applications of GALS design based on pausible clocking in the industry.

Motiviert durch strukturelle Eigenschaften molekularer Ähnlichkeitsnetzwerke werden die Evolution der größten Komponente eines Netzwerkes in zwei verschiedenen stochastischen Modellen, zufälligen Hypergraphen und zufälligen Schnittgraphen, untersucht. Zuerst wird bewiesen, dass die Anzahl der Knoten in der größten Komponente d-uniformer Hypergraphen einer Normalverteilung folgt. Der Beweis nutzt dabei ausschließlich probabilistische Argumente und keine enumerative Kombinatorik. Diesem grundlegenden Resultat folgen weitere Grenzwertsätze für die gemeinsame Verteilung von Knoten- und Kantenzahl sowie Sätze zur Zusammenhangswahrscheinlichkeit zufälliger Hypergraphen und zur asymptotischen Anzahl zusammenhängender Hypergraphen. Da das Hypergraphenmodell einige Eigenschaften der Realweltdaten nur unzureichend abbildet, wird anschließend die Evolution der größten Komponente in zufälligen Schnittgraphen, die Clustereigenschaften realer Netzwerke widerspiegeln, untersucht. Es wird gezeigt, dass zufällige Schnittgraphen sich von zufälligen (Hyper-)Graphen dadurch unterscheiden, dass (bei einer durchschnittlichen Nachbaranzahl von mehr als eins) weder die größte Komponente linear noch die zweitgrößte Komponente logarithmisch groß in Abhängigkeit von der Knotenzahl ist. Weiterhin wird ein Polynomialzeitalgorithmus zur Überdeckung der Kanten eines Graphen mit möglichst wenigen Cliquen (vollständigen Graphen) beschrieben und seine asymptotische Optimalität im Modell der zufälligen Schnittgraphen bewiesen. Anschließend wird die Entwicklung der chromatischen Zahl untersucht und gezeigt, dass zufällige Schnittgraphen mit hoher Wahrscheinlichkeit mittels verschiedener Greedystrategien optimal gefärbt werden können. Letztendlich zeigen Experimente auf realen Netzen eine Übereinstimmung mit den theoretischen Vorhersagen und legen eine gegenseitige Zertifizierung der Optimalität von Cliquen- und Färbungszahl durch Heuristiken nahe. / Motivated by structural properties of molecular similarity networks we study the behaviour of the component evolution in two different stochastic network models, that is random hypergraphs and random intersection graphs. We prove gaussian distribution for the number of vertices in the giant component of a random d-uniform hypergraph. We provide a proof using only probabilistic arguments, avoiding enumerative methods completely. This fundamental result is followed by further limit theorems concerning joint distributions of vertices and edges as well as the connectivity probability of random hypergraphs and the number of connected hypergraphs. Due to deficiencies of the hypergraph model in reflecting properties of the real--world data, we switch the model and study the evolution of the order of the largest component in the random intersection graph model which reflects some clustering properties of real--world networks. We show that for appropriate choice of the parameters random intersection graphs differ from random (hyper-)graphs in that neither the so-called giant component, appearing when the average number of neighbours of a vertex gets larger than one, has linear order nor is the second largest of logarithmic order in the number of vertices. Furthermore we describe a polynomial time algorithm for covering graphs with cliques, prove its asymptotic optimality in a random intersection graph model and study the evolution of the chromatic number in the model showing that, in a certain range of parameters, these random graphs can be coloured optimally with high probability using different greedy algorithms. Experiments on real network data confirm the positive theoretical predictions and suggest that heuristics for the clique and the chromatic number can work hand in hand proving mutual optimality.

Vor allem bei der Betrachtung großer und komplexer Szenarien ist eine Kombination der Vorteile der sequentiellen und parallelen Simulationswelten wünschenswert. Derartige Szenarien lassen sich meist nur bei einer adäquaten, strukturäquivalenten Modellierung, wie in der sequentiellen Simulationswelt üblich, beherrschen. Es sind aber auch gleichzeitig genau diese Simulationsszenarien, die auch am ehesten nach einer Beschleunigung der Simulationsausführung, z.B. durch eine Parallelisierung, verlangen. Die vorliegende Arbeit beschreibt die Konzeption und Implementation einer optimistisch-parallelen Simulationsbibliothek in Java. Diese vereint die Vorzüge optimistisch-paralleler Simulation (automatische Ausnutzung modellinhärenter Parallelität zur Simulationsbeschleunigung) mit der des prozessorientierten Paradigmas (modellabhängig strukturäquivalente und intuitive Modellbeschreibungen). Eine Implementation des prozessorientierten Paradigmas in einer parallelen Simulation ist allerdings nicht unproblematisch. Dies gilt vor allem im Spezialfall der optimistisch-parallelen Simulation, die sich dadurch auszeichnet, dass Simulationsmodelle während eines Simulationslaufes in ungültige Zustände geraten können, was jeweils durch eine Rückkehr des Simulationsmodells in einen früheren, korrekten Zustand korrigiert wird. Ein weiteres Entwicklungsziel besteht darin, im Gegensatz zu den meisten existierenden PDES-Implementationen die interne Arbeitsweise des optimistisch-parallelen Simulationskerns so gut wie möglich zu verbergen. Stattdessen gleichen die vom Simulationskern angebotenen Schnittstellen weitestgehend denen von sequentiellen Simulationskernen. Dadurch wird die Erstellung eines passenden Simulationsmodells im Vergleich zu anderen parallelen Simulationsimplementationen deutlich erleichtert. Auch der Mehraufwand gegenüber der Erstellung von Simulationsmodellen für rein sequentielle Simulationskerne ist relativ gering. / A combination of the advantages of the sequential, as well as the parallel simulation approach is desirable, especially in the case of large and complex simulation scenarios. These are only manageable if a corresponding structurally equivalent simulation model is employed. Also, the very same models will profit most from a speed-up by parallelization. Unfortunately, the implementation of a process-oriented view in a parallel fashion is not a trivial task. Parallel simulation implementations generally suffer from additional computational cost that can offset the parallel speed-up and even lead to a diminished parallel performance, which is even more likely to happen when using process-oriented simulation models. This is especially the case in optimistic-parallel simulations. These are characterized by the ability of the model to get into invalid states which is costly being corrected at runtime by returning the model to valid former states preliminarily saved. The aim of this thesis is the design and implementation of a simulation library in Java. It combines the advantages of optimistic-parallel simulation (i.e. use of parallelism for speed-up) and the process-oriented modeling (creation of an intuitive and structurally equivalent model). Another central objective of the development is to hide the internals of the optimistic-parallel simulation kernel from the modeler, in contrast to most existing PDES implementations. Instead, the implementation is encapsulated by interfaces, which resemble those of sequential simulation kernels, reducing the additional effort needed to create a suited model. A noteworthy aspect of the implementation is the reuse of a web application framework for retroactive modification of the Java bytecode, generated by the Java compiler. This bytecode rewriting solves in an elegant way the task of realizing coroutines, which are the base for the implementation of processes as needed by process-oriented simulation models.

Binary Decision Diagrams (BDDs) sind eine Datenstruktur für Boolesche Funktionen, die auch unter dem Namen branching program bekannt ist. In ordered binary decision diagrams (OBDDs) müssen die Tests einer festen Variablenordnung genügen. In free binary decision diagrams (FBDDs) darf jede Variable höchstens einmal getestet werden. Die Effizienz neuer Varianten des BDD-Konzepts wird gewöhnlich anhand spektakulärer (worst-case) Beispiele aufgezeigt. Wir verfolgen einen anderen Ansatz und vergleichen die Darstellungsgrößen für fast alle Booleschen Funktionen. Während I. Wegener bewiesen hat, daß für die `meisten' n die erwartete OBDD-Größe einer zufälligen Booleschen Funktion von n Variablen gleich der worst-case Größe bis auf Terme kleinerer Ordnung ist, zeigen wir daß dies nicht der Fall ist für n innerhalb von Intervallen konstanter Länge um die Werte n = 2h + h. Ferner gibt es Bereiche von n, in denen minimale FBDDs fast immer um mindestens einen konstanten Faktor kleiner sind als minimale OBDDs. Unsere Hauptsätze ha ben doppelt exponentielle Wahrschein- lichkeitsschranken (in n). Außerdem untersuchen wir die Entwicklung zufälliger OBDDs und ihrer worst-case Größe und decken dabei ein oszillierendes Verhalten auf, das erklärt, warum gewisse Aussagen im allgemeinen nicht verstärkt werden können. / Binary Decision Diagrams (BDDs) are a data structure for Boolean functions which are also known as branching programs. In ordered binary decision diagrams (OBDDs), the tests have to obey a fixed variable ordering. In free binary decision diagrams (FBDDs), each variable can be tested at most once. The efficiency of new variants of the BDD concept is usually demonstrated with spectacular (worst-case) examples. We pursue another approach and compare the representation sizes of almost all Boolean functions. Whereas I. Wegener proved that for `most' values of n the expected OBDD size of a random Boolean function of n variables is equal to the worst-case size up to terms of lower order, we show that this is not the case for n within intervals of constant length around the values n = 2h + h. Furthermore, ranges of n exist for which minimal FBDDs are almost always at least a constant factor smaller than minimal OBDDs. Our main theorems have doubly exponentially small probability bounds (in n). We also investigate the evolution of random OBDDs and their worst-case size, revealing an oscillating behaviour that explains why certain results cannot be improved in general.

In den letzten Jahren haben sich spezielle Prinzipien zur Veröffentlichung strukturierter Daten im World Wide Web (WWW) etabliert. Diese Prinzipien erlauben es, von den jeweils angebotenen Daten auf weitere, nach den selben Prinzipien veröffentlichten Daten zu verweisen. Die daraus resultierende Form von Web-Daten wird entsprechend als Linked Data bezeichnet. Mit der Veröffentlichung von Linked Data im WWW entsteht ein sehr großer Datenraum, welcher Daten verschiedenster Anbieter miteinander verbindet und neuartige Möglichkeiten für Web-basierte Anwendungen bietet. Als Basis für die Entwicklung solcher Anwendungen haben mehrere Forschungsgruppen begonnen, Ansätze zu untersuchen, welche diesen Datenraum als eine Art verteilte Datenbank auffassen und die Ausführung deklarativer Anfragen über dieser Datenbank ermöglichen. Forschungsarbeit zu theoretischen Grundlagen der untersuchten Ansätze fehlt jedoch nahezu vollständig. Die vorliegende Dissertation schließt diese Lücke. / During recent years a set of best practices for publishing and connecting structured data on the World Wide Web (WWW) has emerged. These best practices are referred to as the Linked Data principles and the resulting form of Web data is called Linked Data. The increasing adoption of these principles has lead to the creation of a globally distributed space of Linked Data that covers various domains such as government, libraries, life sciences, and media. Approaches that conceive this data space as a huge distributed database and enable an execution of declarative queries over this database hold an enormous potential; they allow users to benefit from a virtually unbounded set of up-to-date data. As a consequence, several research groups have started to study such approaches. However, the main focus of existing work is to address practical challenges that arise in this context. Research on the foundations of such approaches is largely missing. This dissertation closes this gap.

Viele Probleme der Kombinatorik, Zahlentheorie, Wahrscheinlichkeitstheorie, Zuverlässigkeitstheorie und Statistik lassen sich durch Anwendung einer einheitlichen Methode lösen, die als Prinzip der Inklusion-Exklusion bekannt ist. Das Prinzip der Inklusion-Exklusion drückt die Indikatorfunktion einer Vereinigung endlich vieler Ereignisse als alternierende Summe der Indikatorfunktionen ihrer Durchschnitte aus. Die vorliegende Schrift befasst sich mit verbesserten Inklusions-Exklusions-Identitäten und verbesserten Bonferroni-Ungleichungen, die voraussetzen, dass die Ereignisfamilie gewissen strukturellen Anforderungen genügt. Solche wohl-strukturierten Ereignisfamilien finden sich u.a. in der schließenden Statistik, der kombinatorischen Zuverlässigkeitstheorie und der chromatischen Graphentheorie. / Many problems in combinatorics, number theory, probability theory , reliability theory and statistics can be solved by applying a unifying method, which is known as the principle of inclusion-exclusion. The principle of inclusion-exclusion expresses the indicator function of a union of finitely many events as an alternating sum of indicator functions of their intersections. This thesis deals with improved inclusion-exclusion identities and improved Bonferroni inequalities that require the family of events to satisfy some structural restrictions. Examples of such well-structured families arise in problems of statistical inference, combinatorial reliability theory and chromatic graph theory.

Mit der aktuellen Überarbeitung der Sprache SDL (Specification and Description Language) der ITU-T wurde die semantische Fundierung der formalen Definition dieser Sprache vollständig überarbeitet; die formale Definition basiert nun auf dem Kalkül der Abstract State Machines (ASMs). Ebenfalls neu definiert wurde das um objekt-orientierte Konzepte erweiterte Datentypsystem. Damit musste eine formale semantische Fundierung für diese neuen Konzepte gefunden werden. Der bisher verwendete Kalkül ACT.ONE sollte nicht mehr verwendet werden, da er schwer verwendbar, nicht implementierbar und nicht auf Objektsysteme erweiterbar ist. In der vorliegenden Arbeit werden die Prinzipien einer formalen Sprachdefinition dargelegt und die Umsetzung dieser Prinzipien für die Sprache SDL-2000 vorgestellt. Dabei wird erläutert, dass eine konsistente Sprachdefinition nur dadurch erreicht werden konnte, dass die Definition der formalen Semantik der Sprache parallel mit der Entwicklung der informalen Definition erfolgte. Dabei deckt die formale Sprachdefinition alle Aspekte der Sprache ab: Syn-tax, statische Semantik und dynamische Semantik. Am Beispiel der Datentypsemantik wird erläutert, wie jeder dieser Aspekte informal beschrieben und dann formalisiert wurde. Von zentraler Rolle für die Anwendbarkeit der formalen Semantikdefinition in der Praxis ist der Einsatz von Werkzeugen. Die Arbeit erläutert, wie aus der formalen Sprachdefinition voll-automatisch ein Werkzeug generiert wurde, das die Sprache SDL implementiert, und wie die durch die Umsetzung der formalen Semantikdefinition in ein Werkzeug Fehler in dieser Definition aufgedeckt und behoben werden konnten. / With the latest revision of ITU-T SDL (Specification and Description Language), the semantic foundations of the formal language definition were completely revised; the formal definition is now based on the calculus of Abstract State Machines (ASMs). In addition, the data type system of SDL was revised, as object-oriented concepts were added. As a result, a new semantical foundation for these new concepts had to be defined. The ACT.ONE calculus that had been used so far was not suitable as a foundation any more, as it is hard to use, unimplementable and not extensible for the object oriented features. In this thesis, we elaborate the principles of a formal language definition, and the realisation of these principles in SDL-2000. We explains that a consistent language definition can only be achieved by developing the formal semantics definition in parallel with the development of the informal definition. The formal language definition covers all aspects of the language: syntax, static semantics, and dynamic semantics. Using the data type semantics as an example, we show how each of these aspects is informally described, and then formalized. For the applicability of the formal semantics definition for practitioners, usage of tools plays a central role. We explain how we transform the formal language definition fully automatically into a tool that implements the language SDL. We also explain how creating the tool allowed us to uncover and correct errors in the informal definition.

Ein drahtloses Multihop-Netzwerk (DMN) ist ein verteiltes Kommunikationssystem, welches vor allem die Fähigkeit zur automatischen Anpassung an sich ständig änderne Umgebungsbedingungen hat. Eine zentrale Fragestellung in DMNen ist, ob das Netzwerk partitioniert ist, ob also nicht mehr jeder Knoten mit jedem anderen Knoten kommunizieren kann. Um festzustellen, ob eine Partitionierung droht werden mit Hilfe von 2-Zusammenhangstests Brücken und Artikulationspunkte im Kommunikationsgraphen gesucht. Daraufhin können anschließend korrektive Aktionen eingeleitet werden um die Partitionierung zu verhindern und somit die Netzwerkverfügbarkeit zu erhöhen. Eine Vielzahl von 2-Zusammenhangstestverfahren wurde bereits erfolgreich bei drahtgebundenen Netzen eingesetzt. Allerdings sind diese Verfahren ungeeignet für drahtlose Netze, da die Ungenauigkeiten durch den häufigen Paketverlust in solchen Systemen bisher nicht berücksichtigt wurden. Mit Hilfe von stochastischen Modellen wird gezeigt, dass Fehler in der Entscheidungsfindung für DMNen bereits bei sehr einfachen Problemen wie der Link-Erkennung signifikant sein können. In dieser Arbeit werden daher verschiedene Verfahren präsentiert, die auch auf Grundlage unsicherer Informationen noch eine verlässliche Entscheidungsfindung ermöglichen. Die Arbeit präsentiert einen neuen verteilten Algorithmus zum Test auf 2-Zusammenhang, welcher Fehler durch Nachrichtenverlust berücksichtigt und gleichzeitig die Anzahl an Nachrichten reduziert. Basierend auf einer umfassenden Analyse der Einflüsse von Kommunikationsfehlern auf den Algorithmus, wurden Abstimmungsprozeduren entwickelt, die die Wahrscheinlichkeit von Fehlentscheidungen nochmals reduzieren. Zur weiteren Analyse werden die Algorithmen erstens in der Motelab-Umgebung und zweitens mit Hilfe von Simulationen untersucht. Die präsentierten Algorithmen zeigen überzeugende Ergebnisse unter variierenden Bedingungen, was ihre Anwendbarkeit in realen Szenarien unterstreicht. / Wireless multi-hop network (WMN) is a distributed communication system composed of autonomous processing nodes that is known for its ability to automatically adjust to rapidly changing conditions in the surrounding environment. Connectivity is one of the basic properties of a network. Removal of a bridge or an articulation point partitions a network. Biconnectivity testing identifies bridges and articulation points in a network, and once they are known corrective actions can be performed in order to improve network''s reliability. Numerous biconnectivity testing algorithms are successfully applied in graphs, wired networks and multiprocessor systems. However, they are inadequate for application in wireless networks since the frequent packet losses introduce uncertainty in the system which these algorithms cannot handle. The stochastic analysis shows that errors in decision-making in WMNs are considerable even for seemingly simple tasks such as the detection of links. The main contribution of this work is to provide means for accurate binary decision-making under uncertainty within the context of biconnectivity testing in WMNs. A distributed algorithm is developed that successfully handles the faults caused by message losses and simultaneously utilizes benefits of wireless communication to reduce message complexity from O(e) to O(n). Based on stochastic analysis of WMN topologies and a comprehensive analysis of impact of communication faults on algorithm''s behavior, the algorithm is extended by voting theory to reduce probability of erroneous decisions. The algorithm and the voting rules are evaluated in experiments in Motelab testbed and in the event-based simulator Jist/SWANS. The algorithm is accurate under various conditions which demonstrates its applicability in reality and capability of successful operation in presence of packet losses.