Cyber-physical systems achieve sophisticated system behavior exploring the tight interconnection of physical coupling present in classical engineering systems and information technology based coupling. A particular challenging case are systems where these cyber-physical systems are formed ad hoc according to the specific local topology, the available networking capabilities, and the goals and constraints of the subsystems captured by the information processing part. In this paper we present a formalism that permits to model the sketched class of cyber-physical systems. The ad hoc formation of tightly coupled subsystems of arbitrary size are specified using a UML-based graph transformation system approach. Differential equations are employed to define the resulting tightly coupled behavior. Together, both form hybrid graph transformation systems where the graph transformation rules define the discrete steps where the topology or modes may change, while the differential equations capture the continuous behavior in between such discrete changes. In addition, we demonstrate that automated analysis techniques known for timed graph transformation systems for inductive invariants can be extended to also cover the hybrid case for an expressive case of hybrid models where the formed tightly coupled subsystems are restricted to smaller local networks. / Cyber-physical Systeme erzielen ihr ausgefeiltes Systemverhalten durch die enge Verschränkung von physikalischer Kopplung, wie sie in Systemen der klassichen Igenieurs-Disziplinen vorkommt, und der Kopplung durch Informationstechnologie. Eine besondere Herausforderung stellen in diesem Zusammenhang Systeme dar, die durch die spontane Vernetzung einzelner Cyber-Physical-Systeme entsprechend der lokalen, topologischen Gegebenheiten, verfügbarer Netzwerkfähigkeiten und der Anforderungen und Beschränkungen der Teilsysteme, die durch den informationsverabeitenden Teil vorgegeben sind, entstehen. In diesem Bericht stellen wir einen Formalismus vor, der die Modellierung der eingangs skizzierten Systeme erlaubt. Ein auf UML aufbauender Graph-Transformations-Ansatz wird genutzt, um die spontane Bildung eng kooperierender Teilsysteme beliebiger Größe zu spezifizieren. Differentialgleichungen beschreiben das kombinierte Verhalten auf physikalischer Ebene. In Kombination ergeben diese beiden Formalismen hybride Graph-Transformations-Systeme, in denen die Graph-Transformationen diskrete Schritte und die Differentialgleichungen das kontinuierliche, physikalische Verhalten des Systems beschreiben. Zusätzlich, präsentieren wir die Erweiterung einer automatischen Analysetechnik zur Verifikation induktiver Invarianten, die bereits für zeitbehaftete Systeme bekannt ist, auf den ausdrucksstärkeren Fall der hybriden Modelle.

The service-oriented architecture supports the dynamic assembly and runtime reconfiguration of complex open IT landscapes by means of runtime binding of service contracts, launching of new components and termination of outdated ones. Furthermore, the evolution of these IT landscapes is not restricted to exchanging components with other ones using the same service contracts, as new services contracts can be added as well. However, current approaches for modeling and verification of service-oriented architectures do not support these important capabilities to their full extend.In this report we present an extension of the current OMG proposal for service modeling with UML - SoaML - which overcomes these limitations. It permits modeling services and their service contracts at different levels of abstraction, provides a formal semantics for all modeling concepts, and enables verifying critical properties. Our compositional and incremental verification approach allows for complex properties including communication parameters and time and covers besides the dynamic binding of service contracts and the replacement of components also the evolution of the systems by means of new service contracts. The modeling as well as verification capabilities of the presented approach are demonstrated by means of a supply chain example and the verification results of a first prototype are shown. / Service-Orientierte Architekturen erlauben die dynamische Zusammensetzung und Rekonfiguration komplexer, offener IT Landschaften durch Bindung von Service Contracts zur Laufzeit, starten neuer Komponenten und beenden von veralteten. Die Evolution dieser Systeme ist nicht auf den Austausch von Komponenten-Implementierungen bei Beibehaltung der Service-Contracts beschränkt, sondern das Hinzufügen neuer Service-Contracts wird ebenfalls unterstützt. Aktuelle Ansätze zur Modellierung und Verifikation Service-Orientierter Architekturen unterstützen diese wichtigen Eigenschaften, wenn überhaupt, nur unvollständig. In diesem Bericht stellen wir eine Erweiterung des aktuellen OMG Vorschlags zur Service Modellierung mit UML - SoaML - vor, die diese Einschränkungen aufhebt. Unser Ansatz erlaubt die Modellierung von Service Contracts auf verschiedenen Abstraktionsniveaus, besitzt eine fundierte formale Semantik für alle eingeführten Modellierungskonzepte und erlaubt die Verifikation kritischer Eigenschaften. Unser kompositionaler und inkrementeller Verifikationsansatz erlaubt die Verifikation komplexer Eigenschaften einschließlich Kommunikationsparameter und Zeit und deckt neben der dynamischen Bindung von Service Contracts sowie dem Austausch von Komponenten auch die Evolution des gesamten Systems durch das Hinzufügen neuer Service Contracts ab. Die Modellierungs- als auch die Verifikationsfähigkeiten unseres vorgestellten Ansatzes werden durch ein Anwendungsbeispiel aus dem Bereich des Lieferkettenmanagements veranschaulicht.

Mit der Einführung des europäischen Zugsicherungssystems ETCS sind durch die umfassenden Telegrammdaten, die zwischen Zug und Strecke ausgetauscht werden, neue Herausforderungen bei der Planung, Projektierung, aber auch Prüfung und Validierung verbunden. Im Rahmen der Dissertation wird ein neuartiges Verfahren zur Validierung sicherheitskritischer Anteile von ETCS-Nachrichten entwickelt. Der Ansatz beruht auf der topologischen Aufbereitung der Nachrichteninhalte in einem vierstufigen Prozess. Das Ergebnis der Aufbereitung erlaubt sowohl den automatisierten Abgleich gegen Referenzdaten als auch eine visuelle Prüfung gegen Topologiepläne. Das Optimierungspotential des Ansatzes bei der Validierung wird im Rahmen einer Erprobung anhand realer Projektdaten bestätigt. Mit der topologischen Aufbereitung werden die komplexen Nachrichteninhalte in eine für den Prüfer erfassbare und zu den Referenzdaten vergleichbare Form überführt. Redundante Nachrichteninhalte werden im Zuge der Aufbereitung erkannt und zusammengefasst, was gleichermaßen zur Minimierung des Prüfaufwands sowie zur Erhöhung des Abdeckungsgrades beiträgt.

One of the key challenges in service-oriented systems engineering is the prediction and assurance of non-functional properties, such as the reliability and the availability of composite interorganizational services. Such systems are often characterized by a variety of inherent uncertainties, which must be addressed in the modeling and the analysis approach. The different relevant types of uncertainties can be categorized into (1) epistemic uncertainties due to incomplete knowledge and (2) randomization as explicitly used in protocols or as a result of physical processes. In this report, we study a probabilistic timed model which allows us to quantitatively reason about nonfunctional properties for a restricted class of service-oriented real-time systems using formal methods. To properly motivate the choice for the used approach, we devise a requirements catalogue for the modeling and the analysis of probabilistic real-time systems with uncertainties and provide evidence that the uncertainties of type (1) and (2) in the targeted systems have a major impact on the used models and require distinguished analysis approaches. The formal model we use in this report are Interval Probabilistic Timed Automata (IPTA). Based on the outlined requirements, we give evidence that this model provides both enough expressiveness for a realistic and modular specifiation of the targeted class of systems, and suitable formal methods for analyzing properties, such as safety and reliability properties in a quantitative manner. As technical means for the quantitative analysis, we build on probabilistic model checking, specifically on probabilistic time-bounded reachability analysis and computation of expected reachability rewards and costs. To carry out the quantitative analysis using probabilistic model checking, we developed an extension of the Prism tool for modeling and analyzing IPTA. Our extension of Prism introduces a means for modeling probabilistic uncertainty in the form of probability intervals, as required for IPTA. For analyzing IPTA, our Prism extension moreover adds support for probabilistic reachability checking and computation of expected rewards and costs. We discuss the performance of our extended version of Prism and compare the interval-based IPTA approach to models with fixed probabilities. / Eine der wichtigsten Herausforderungen in der Entwicklung von Service-orientierten Systemen ist die Vorhersage und die Zusicherung von nicht-funktionalen Eigenschaften, wie Ausfallsicherheit und Verfügbarkeit von zusammengesetzten, interorganisationellen Diensten. Diese Systeme sind oft charakterisiert durch eine Vielzahl von inhärenten Unsicherheiten, welche sowohl in der Modellierung als auch in der Analyse eine Rolle spielen. Die verschiedenen relevanten Arten von Unsicherheiten können eingeteilt werden in (1) epistemische Unsicherheiten aufgrund von unvollständigem Wissen und (2) Zufall als Mittel in Protokollen oder als Resultat von physikalischen Prozessen. In diesem Bericht wird ein probabilistisches, Zeit-behaftetes Modell untersucht, welches es ermöglicht quantitative Aussagen über nicht-funktionale Eigenschaften von einer eingeschränkten Klasse von Service-orientierten Echtzeitsystemen mittels formaler Methoden zu treffen. Zur Motivation und Einordnung wird ein Anforderungskatalog für probabilistische Echtzeitsysteme mit Unsicherheiten erstellt und gezeigt, dass die Unsicherheiten vom Typ (1) und (2) in den untersuchten Systemen einen Ein uss auf die Wahl der Modellierungs- und der Analysemethode haben. Als formales Modell werden Interval Probabilistic Timed Automata (IPTA) benutzt. Basierend auf den erarbeiteten Anforderungen wird gezeigt, dass dieses Modell sowohl ausreichende Ausdrucksstärke für eine realistische und modulare Spezifikation als auch geeignete formale Methoden zur Bestimmung von quantitativen Sicherheits- und Zuverlässlichkeitseigenschaften bietet. Als technisches Mittel für die quantitative Analyse wird probabilistisches Model Checking, speziell probabilistische Zeit-beschränkte Erreichbarkeitsanalyse und Bestimmung von Erwartungswerten für Kosten und Vergütungen eingesetzt. Um die quantitative Analyse mittels probabilistischem Model Checking durchzuführen, wird eine Erweiterung des Prism-Werkzeugs zur Modellierung und Analyse von IPTA eingeführt. Die präsentierte Erweiterung von Prism ermöglicht die Modellierung von probabilistischen Unsicherheiten mittelsWahrscheinlichkeitsintervallen, wie sie für IPTA benötigt werden. Zur Verifikation wird probabilistische Erreichbarkeitsanalyse und die Berechnung von Erwartungswerten durch das Werkzeug unterstützt. Es wird die Performanz der Prism-Erweiterung untersucht und der Intervall-basierte IPTA-Ansatz mit Modellen mit festen Wahrscheinlichkeitswerten verglichen.

DNA-basierte Systeme beschreiben formal ein alternatives Berechnungskonzept, beruhend auf der Anwendung molekularbiologischer Operationen. Der Grundgedanke ist dabei die Entwicklung alternativer und universeller Rechnerarchitekturen. Infolge der zugrunde liegenden maximalen Parallelität sowie der hohen Komplexität entsprechender Systeme ist die Korrektheit jedoch schwer zu beweisen. Um dies zu ermöglichen werden in der Arbeit zunächst für drei verschiedene Systemklassen mit unterschiedlichen Berechnungsparadigmen strukturelle operationelle Semantiken definiert und bekannte Formalismen der Prozesstheorie adaptiert. Nachfolgend werden Tableaubeweissysteme beschrieben, mithilfe derer einerseits Invarianten und andererseits die jeweilige Korrektheit von DNA-basierten Systemen mit universeller Berechnungsstärke bewiesen werden können. Durch Anwendung dieser Konzepte konnte für drei universelle Systeme die Korrektheit gezeigt und für ein System widerlegt werden.

During the design and verification of the Hyperstone S5 flash memory controller, we developed a highly effective way to use the SystemVerilog direct programming interface (DPI) to integrate an instruction set simulator (ISS) and a software debugger in logic simulation. The processor simulation was performed by the ISS, while all other hardware components were simulated in the logic simulator. The ISS integration allowed us to filter many of the bus accesses out of the logic simulation, accelerating runtime drastically. The software debugger integration freed both hardware and software engineers to work in their chosen development environments. Other benefits of this approach include testing and integrating code earlier in the design cycle and more easily reproducing, in simulation, problems found in FPGA prototypes.

Långtidsprognoser beskriver gapet mellan väderprognoser och klimatmodeller som förutspår klimatförändringar p.g.a. den globala uppvärmningen. Långtidsprognostik förlitar sig på så kallade “källor av förutsägbarhet”. Dessa kan vara variabler som ändrar sig långsamt, som havsvattnets yttemperatur, eller variationsmönster såsom El Nino-Southern Oscillation. Många industrisektorer och delar av samhället som ´ idag använder väderprognoser i sina dagliga beslut, som t.ex. jordbruksindustrin, energiindustrin eller någon annan väderkänslig sektor, kan potentiellt dra nytta av träffsäkra och pålitliga långtidsprognoser. Bland de potentiella användarna finns förstås också privatpersoner. Syftet med denna studie är att introducera långtidsprognostik och att försöka utvärdera prestandan av ECMWFs välkända och etablerade säsongsmodell SEAS5, genom tidigare forskning och ECMWFs verifikationsfigurer som finns tillgängliga för allmänheten. Utvärderingen gjordes utifrån allmänhetens perspektiv och vad de skulle uppfatta som en “bra” prognos. Marknära temperatur och delvis nederbörd undersöktes för Europa under sommar och vinter, i termer av “skill” (träffsäkerhet) och “reliability” (pålitlighet, på så sätt att en händelse som förutspås med 60% sannolikhet också ska observeras i ungefär 60% av fallen). SEAS5 når inte riktigt upp i “bra” skill-nivåer för marknära temperatur, om “bra” motsvarar synoptiskt användbar prognos. Det finns dock stora skillnader mellan olika platser och säsonger, där “bra” skill framförallt märks i södra/sydöstra Europa på sommaren och delar av norra Europa på vintern. “Reliability” är generellt bra, även om det är svårt att avgöra hur den skiljer mellan olika platser. Nederbörd visar dock mycket dålig skill och låg “reliability” oavsett säsong eller plats. / Long range weather prediction describe weather forecasts with a range longer than 14 days, but shorter than climate prediction models that predict climate change due to global warming. Long range forecasting relies on sources of predictability that, for example, changes slowly such as sea surface temperatures, or varies in predictable patterns like the El Nino-Southern Oscillation. Many sectors of industry and society ´ that today use weather forecasting in their day-to-day decision making, such as agriculture, energy or any other weather sensitive sector, have potentially much to benefit from accurate and reliable long range forecasts. Among potential users is of course the general public. The purpose of this study is to give an introduction to long range weather prediction and attempt to evaluate the performance of ECMWF’s SEAS5 seasonal model, which is one of the most well known and established S2S models, by using earlier research and ECMWF’s publicly available verification charts. This was done from the public’s perspective of what would be considered a “good” forecast, mainly from near surface air temperature but also precipitation, during winter and summer in Europe, on the aspects of skill (accuracy) and reliability (in the sense that a probabilistic forecast of 60% for an event also is observed around 60% of the time). SEAS5 overall doesn’t quite reach “good” skill levels for near surface temperature, if “good” is defined as synoptically significant. The skill level varies significantly though, depending on region and season, with southern/southeastern Europe during summer and parts of northern Europe during winter being notable “good” situations. Reliability is generally good, even if it is difficult to know how reliability varies spatially. However, precipitation shows very little skill and low reliability, no matter the season or region.

Ein stetig wachsender Anteil des Aufwands zum Entwurf digitaler Schaltungen entfällt auf die funktionale Verifikation. Der Verifikationsraum als Menge aller möglichen Kombinationen von Attributen einer Komponente, d. h. der Parameter und Eingangsdaten, ist oftmals sehr groß, wodurch die Verifikation aller Kombinationen unpraktikabel wird. Deshalb verwenden moderne Methoden der funktionalen Verifikation die zufallsgesteuerte Erzeugung von Stimuli in Verbindung mit manuell definierten Spezialfällen, sog. Corner Cases, um eine möglichst hohe funktionale Abdeckung in der angestrebten Verteilung zu erzielen. Als großer Nachteil diese Ansätze führen steigende Abdeckungsanforderungen zu exponentiell ansteigenden Laufzeiten. Um diesen Nachteil auszugleichen, wurden Generatoren propagiert, die nur solche Kombinationen erzeugen, die nicht bereits abgedeckt worden sind. Leider können die dabei verwendeten Verfahren das Problem nicht zufriedenstellend lösen, da auch sie im Allgemeinen zufällige Kombinationen erzeugen, um in einem zweiten Schritt zu prüfen, ob diese bereits abgedeckt sind. Im vorliegenden Beitrag werden Entscheidungsdiagramme zur Repräsentation aller zulässigen Kombinationen innerhalb des Verifikationsraums verwendet. Mit Hilfe dieses analytischen Modells kann jede beliebige Anzahl von Kombinationen in linearer Zeit erzeugt werden. Wird die vorgestellte Methode auf die Zufallserzeugung zur funktionalen Verifikation angewendet, kann diese um Größenordnungen beschleunigt werden.

The meet up between data, processes and structural knowledge in modeling complex enterprise systems is a challenging task that has led to the study of combining formalisms from knowledge representation, database theory, and process management. Moreover, to ensure system correctness, formal verification also comes into play as a promising approach that offers well-established techniques. In line with this, significant results have been obtained within the research on data-aware business processes, which studies the marriage between static and dynamic aspects of a system within a unified framework. However, several limitations are still present. Various formalisms for data-aware processes that have been studied typically use a simple mechanism for specifying the system dynamics. The majority of works also assume a rather simple treatment of inconsistency (i.e., reject inconsistent system states). Many researches in this area that consider structural domain knowledge typically also assume that such knowledge remains fixed along the system evolution (context-independent), and this might be too restrictive. Moreover, the information model of data-aware processes sometimes relies on relatively simple structures. This situation might cause an abstraction gap between the high-level conceptual view that business stakeholders have, and the low-level representation of information. When it comes to verification, taking into account all of the aspects above makes the problem more challenging. In this thesis, we investigate the verification of data-aware processes in the presence of ontologies while at the same time addressing all limitations above. Specifically, we provide the following contributions: (1) We propose a formal framework called Golog-KABs (GKABs), by leveraging on the state of the art formalisms for data-aware processes equipped with ontologies. GKABs enable us to specify semantically-rich data-aware business processes, where the system dynamics are specified using a high-level action language inspired by the Golog programming language. (2) We propose a parametric execution semantics for GKABs that is able to elegantly accommodate a plethora of inconsistency-aware semantics based on the well-known notion of repair, and this leads us to consider several variants of inconsistency-aware GKABs. (3) We enhance GKABs towards context-sensitive GKABs that take into account the contextual information during the system evolution. (4) We marry these two settings and introduce inconsistency-aware context-sensitive GKABs. (5) We introduce the so-called Alternating-GKABs that allow for a more fine-grained analysis over the evolution of inconsistency-aware context-sensitive systems. (6) In addition to GKABs, we introduce a novel framework called Semantically-Enhanced Data-Aware Processes (SEDAPs) that, by utilizing ontologies, enable us to have a high-level conceptual view over the evolution of the underlying system. We provide not only theoretical results, but have also implemented this concept of SEDAPs. We also provide numerous reductions for the verification of sophisticated first-order temporal properties over all of the settings above, and show that verification can be addressed using existing techniques developed for Data-Centric Dynamic Systems (which is a well-established data-aware processes framework), under suitable boundedness assumptions for the number of objects freshly introduced in the system while it evolves. Notably, all proposed GKAB extensions have no negative impact on computational complexity.

Der Scanning-Antastabweichung kommt in der Überprüfung und Bewertung von taktil-scannenden 3D-Koordinatenmessgeräten fortwährend eine große Bedeutung zu. Sie bildet unter anderem die Basis für die Geräteauswahl, die Messsystemanalyse und die Bestimmung von Messunsicherheiten. Dabei entscheiden spezifische Wirkbeziehungen innerhalb des Gesamtsystems aus Koordinatenmessgerät und Messobjekt über die Aussagekraft abgeleiteter Kennwerte sowie die Vereinbarkeit der Herausforderungen der Fertigungsmesstechnik in einer vorgegebenen Messaufgabe. In dieser Arbeit wird eine Vorgehensweise zur Bestimmung der spezifischen, oberflächenbedingten Scanning-Antastabweichung unter Berücksichtigung der Einflussgrößen Sensor, Scanning-Parameter, Tasterkonfiguration und Gestaltabweichungen des Messobjektes vorgestellt. Ziel dessen ist es, bestehende Kenntnisse zur Wirkungsweise definierter Einflussgrößen zu erweitern und einen neuen, erweiterten sowie anwendungsorientierten Ansatz für die Überprüfung und Bewertung von Koordinatenmessgeräten zu bieten. Dies bildet den Ausgangspunkt für die Vergleichbarkeit und Reproduzierbarkeit von Messergebnissen. Die Basis zugehöriger Untersuchungen bilden vorangegangene Forschungsprojekte sowie Empfehlungen und Hinweise aus Literatur und Herstellerinformationen. Daraus abgeleitete Haupteinflussgrößen definieren den Rahmen der Versuchsreihen zur Klärung formulierter zentraler Forschungs-fragen. Ausgehend von den Untersuchungen an einem festgelegten Basis-Koordinatenmessgerät wird die Übertragbarkeit erarbeiteter Erkenntnisse auf alternative Sensoren überprüft und Ergebnisse auf systematische und zufällige Abweichungsanteile hin analysiert. Durch den Vergleich „annähernd-idealer“ sowie „zielmarktorientierter“ Oberflächen zeigt sich, dass Wirkbeziehungen zwischen den untersuchten Haupteinflussgrößen, beispielsweise unter Variation der Scanning-Geschwindigkeit, erst durch das Vorhandensein nicht-idealer Oberflächeneigenschaften auftreten oder durch diese derart verstärkt werden, dass sie sich von zufälligen Messabweichungen abheben. Die Bewertung der erfassten Messdaten erfolgt dabei anhand der abgeleiteten Geradheitsabweichung in Bezug auf zugrundeliegende Referenzmessungen sowie vergleichender prozentualer Betrachtungen und abgeleiteter Grenzwerte. Zentrale Erkenntnis der Hauptuntersuchungen am Basis-Koordinatenmessgerät ist, dass durch verschiedene Tasterorientierungen klare und explizit unterschiedliche Wirkbeziehungen zwischen den Haupteinflussgrößen auftreten, was über bisherige Forschungsergebnisse weit hinausgeht. Dies konnte auch durch die Verifikationsmessungen bestätigt werden. Sensorübergreifend sind derartig klare Wirkbeziehungen nicht zu detektieren. Auch zum Basis-Koordinatenmessgerät vergleichbare sensorspezifische Abhängigkeiten sind anhand der durchgeführten Messreihen nicht formulierbar. Es ist allerdings auch zu konstatieren, dass jede der untersuchten Einflussgrößen, unter Ausnahme der Antastkraft, durch Messabweichungen belegbare Auswirkungen hat. Die Erkenntnisse und Potentiale dieser Arbeit bieten somit eine umfängliche Basis für die Weiterentwicklung der Bewertungs- und Entscheidungsgrundlagen der taktil-scannenden 3D-Koordninatenmesstechnik, welche durch eine verbesserte Vergleichbarkeit, ein umfassenderes Wissen zu Mess- beziehungsweise Antastabweichungen sowie gesteigerte Effizienz gekennzeichnet sind.