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.

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.

The ability to provide succinct information about why a property does, or does not, hold in a given system is a key feature in the context of formal verification and model checking. It can be used both to explain the behavior of the system to a user of verification software, and as a tool to aid automated abstraction and synthesis procedures. Counterexample traces, which are executions of the system that do not satisfy the desired specification, are a classical example. Specifications of systems with probabilistic behavior usually require that an event happens with sufficiently high (or low) probability. In general, single executions of the system are not enough to demonstrate that such a specification holds. Rather, standard witnesses in this setting are sets of executions which in sum exceed the required probability bound. In this thesis we consider methods to certify and witness that probabilistic reachability constraints hold in Markov decision processes (MDPs) and probabilistic timed automata (PTA). Probabilistic reachability constraints are threshold conditions on the maximal or minimal probability of reaching a set of target-states in the system. The threshold condition may represent an upper or lower bound and be strict or non-strict. We show that the model-checking problem for each type of constraint can be formulated as a satisfiability problem of a system of linear inequalities. These inequalities correspond closely to the probabilistic transition matrix of the MDP. Solutions of the inequalities are called Farkas certificates for the corresponding property, as they can indeed be used to easily validate that the property holds. By themselves, Farkas certificates do not explain why the corresponding probabilistic reachability constraint holds in the considered MDP. To demonstrate that the maximal reachability probability in an MDP is above a certain threshold, a commonly used notion are witnessing subsystems. A subsystem is a witness if the MDP satisfies the lower bound on the optimal reachability probability even if all states not included in the subsystem are made rejecting trap states. Hence, a subsystem is a part of the MDP which by itself satisfies the lower-bounded threshold constraint on the optimal probability of reaching the target-states. We consider witnessing subsystems for lower bounds on both the maximal and minimal reachability probabilities, and show that Farkas certificates and witnessing subsystems are related. More precisely, the support (i.e., the indices with a non-zero entry) of a Farkas certificate induces the state-space of a witnessing subsystem for the corresponding property. Vice versa, given a witnessing subsystem one can compute a Farkas certificate whose support corresponds to the state-space of the witness. This insight yields novel algorithms and heuristics to compute small and minimal witnessing subsystems. To compute minimal witnesses, we propose mixed-integer linear programming formulations whose solutions are Farkas certificates with minimal support. We show that the corresponding decision problem is NP-complete even for acyclic Markov chains, which supports the use of integer programs to solve it. As this approach does not scale well to large instances, we introduce the quotient-sum heuristic, which is based on iteratively solving a sequence of linear programs. The solutions of these linear programs are also Farkas certificates. In an experimental evaluation we show that the quotient-sum heuristic is competitive with state-of-the-art methods. A large part of the algorithms proposed in this thesis are implemented in the tool SWITSS. We study the complexity of computing minimal witnessing subsystems for probabilistic systems that are similar to trees or paths. Formally, this is captured by the notions of tree width and path width. Our main result here is that the problem of computing minimal witnessing subsystems remains NP-complete even for Markov chains with bounded path width. The hardness proof identifies a new source of combinatorial hardness in the corresponding decision problem. Probabilistic timed automata generalize MDPs by including a set of clocks whose values determine which transitions are enabled. They are widely used to model and verify real-time systems. Due to the continuously-valued clocks, their underlying state-space is inherently uncountable. Hence, the methods that we describe for finite-state MDPs do not carry over directly to PTA. Furthermore, a good notion of witness for PTA should also take into account timing aspects. We define two kinds of subsystems for PTA, one for maximal and one for minimal reachability probabilities, respectively. As for MDPs, a subsystem of a PTA is called a witness for a lower-bounded constraint on the (maximal or minimal) reachability probability, if it itself satisfies this constraint. Then, we show that witnessing subsystems of PTA induce Farkas certificates in certain finite-state quotients of the PTA. Vice versa, Farkas certificates of such a quotient induce witnesses of the PTA. Again, the support of the Farkas certificates corresponds to the states included in the subsystem. These insights are used to describe algorithms for the computation of minimal witnessing subsystems for PTA, with respect to three different notions of size. One of them counts the number of locations in the subsystem, while the other two take into account the possible clock valuations in the subsystem.:1 Introduction 2 Preliminaries 3 Farkas certificates 4 New techniques for witnessing subsystems 5 Probabilistic systems with low tree width 6 Explications for probabilistic timed automata 7 Conclusion

This thesis explores synergies between deductive verification and model checking, by using the existing model checker TriCera to automatically infer specifications for the deductive verifier Frama-C. To accomplish this, a formal semantics is defined for a subset of ANSI C, extended with assume statements, called Csmall. Then, it is shown how a Hoare logic contract can be translated into statements in Csmall, and the defined formal semantics is used to prove that the translation is correct. Furthermore, it is shown that the translation can be applied also to a real specification language. This is done by defining a subset of ACSL, called ACSLsmall, and giving a formal semantics also for this. Lastly, two examples are provided showing that the theory developed in this thesis can be applied to automatically infer ACSL function contracts. / Den här avhandlingen studerar synergier mellan deduktiv verifikation och modelprovning, genom att använda Tricera, ett verktyg för modellprovning, för att automatiskt generera specifikationer för Frama-C, ett verktyg för deduktiv verifikation. Detta uppnås genom att definiera en formell semantik för en delmängd av ANSI-C, utökat med assume satser, som kallas förCsmall. Sedan visas hur kontrakt kan översättas till satser i Csmall samt att översättningen är korrekt. Därefter visas att översättningen också kan tillämpas på ett verkligt specifikationsspråk, genom att definiera en delmängd av ACSL, som kallas ACSLsmall, och definiera en formell semantik också för detta. Slutligen visas med två exempel hur teorin från uppsatsen kan appliceras för att automatiskt generera funktionskontrakt i ACSL.

Model checking is a formal verification technique for verifying temporal properties in state-transition models. The main problem with using model checking is the state explosion problem, where the number of states in the model can grow exponentially, making verification infeasible. Previous work has tried to mitigate the state explosion problem by representing code blocks as Hoare-logic contracts in an abstract state-transition model using the temporal logic TLA. This is achieved by treating the block as atomic. In order to ensure that the abstract state-transition model is faithful with respect to the temporal properties you want to verify, only some code blocks can be considered atomic. This thesis aims to answer how atomic code blocks can be identified atomically and evaluate their potential for reducing state space during model checking. We give a theoretical foundation of what it means for a code block to be considered as atomic in TLA. Moreover, we introduce a property that characterizes these atomic code blocks and presents an algorithm to identify them for sequential programs written in a subset of C. Experimental results demonstrate that the identification of atomic code blocks using our algorithm can be used to significantly reduce the state space during model checking, with an average reduction factor of 62. The potential of this verification approach is promising, however, further case studies are necessary to better understand the extent of this reduction across different program types and properties. / Modellkontroll är en formell verifieringsteknik för att bekräfta tidsrelaterade egenskaper i tillståndsövergångsmodeller. Huvudproblemet med modellkontroll är problemet med tillståndsexplosion, där antalet tillstånd i modellen kan öka exponentiellt och göra verifieringen ogenomförbar. Tidigare arbete har försökt mildra problemet med tillståndsexplosion genom att representera kodblock som Hoare-logiska kontrakt i en abstrakt tillståndsövergångsmodell med hjälp av tidslogiken TLA. Detta uppnås genom att behandla blocket som atomiskt. För att säkerställa att den abstrakta tillståndsövergångsmodellen är trogen med avseende på de tidsrelaterade egenskaper du vill verifiera kan endast vissa kodblock betraktas som atomiska. Denna avhandling syftar till att besvara hur atomiska kodblock kan identifieras automatiskt och utvärdera deras potential för att minska tillståndsutrymmet under modellkontroll. Vi ger en teoretisk grund för vad det innebär för ett kodblock att betraktas som atomiskt inom TLA. Dessutom introducerar vi en egenskap som karaktäriserar dessa atomiska kodblock och presenterar en algoritm för att identifiera dem för sekventiella program skrivna i en delmängd av C. Experimentella resultat visar att identifieringen av atomiska kodblock med hjälp av vår algoritm kan användas för att betydligt minska tillståndsutrymmet under modellkontroll, med en genomsnittlig reduktionsfaktor på 62. Potentialen för denna verifieringsmetod är lovande, men ytterligare fallstudier krävs för att bättre förstå omfattningen av denna reduktion över olika typer av program och egenskaper.