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.

Die Protonentherapie zeichnet sich durch steile Dosisgradienten und damit einen gut lokalisierbaren Energieübertrag aus. Um dieses Potential voll ausschöpfen zu können, werden weltweit Möglichkeiten erforscht, die Dosisdeposition und insbesondere die Reichweite der Protonen im Patienten zu verifizieren. Eine vielversprechende, erst im letzten Jahrzehnt entdeckte Methode ist das Prompt Gamma-Ray Timing (PGT), das auf der Abhängigkeit der detektierten Flugzeitverteilung prompter Gammastrahlung von der Transitzeit der Protonen im Patienten beruht. In dieser Arbeit wird eine Geant4-Simulation zur Vorhersage der PGT-Spektren bei Bestrahlung eines PMMA-Phantoms entwickelt und durch den Vergleich mit experimentellen Daten validiert. Sowohl die Emissionsausbeute prompter Gammastrahlung im Phantom als auch die Detektionsrate werden abhängig von der Protonenenergie analysiert. Zur Vergleichbarkeit mit den gemessenen Spektren wird eine mehrschrittige Prozessierung der Simulationsergebnisse vorgestellt. Schließlich wird die Simulation genutzt, um die Sensitivität der PGT-Methode auf Reichweitenänderungen zu demonstrieren. Dafür können in das Phantom Cavitäten unterschiedlicher Dicke und verschiedenen Materials eingefügt werden. Für geeignet gewählte Verteilungsparameter der simulierten PGT-Spektren wird deren detektierte Änderung mit der bekannten induzierten Reichweitenänderung ins Verhältnis gesetzt. Die so bestimmte Sensitivität ist mit früheren Ergebnissen für gemessene Spektren im Rahmen der Unsicherheiten in Übereinstimmung.:1 Einleitung und Motivation 1 2 Theoretische Grundlagen 5 2.1 Wechselwirkung von Protonen mit Materie 5 2.1.1 Bethe-Bloch-Gleichung 6 2.1.2 Reichweite im CSDA-Modell 9 2.1.3 Tiefendosiskurve und Bragg-Peak 10 2.2 Prompt Gamma-Ray Timing 11 2.2.1 Emission prompter Gammastrahlung 11 2.2.2 Korrelation zur Protonen-Reichweite und Dosisdeposition 11 2.2.3 Idee des Prompt Gamma-Ray Timings 14 3 Material und Methoden 17 3.1 Dresdner IBA-Protonentherapie 17 3.1.1 Beschleunigungsprinzip des Isochronzyklotrons 17 3.1.2 Zeitliche Struktur der Protonen-Pakete 18 3.2 Teilchentransportrechnungen mit Geant4 20 3.3 PLD-Format für Pencil-Beam-Scanning-Pläne 21 3.3.1 Geometrische Definition der Spots 21 3.3.2 Dosimetrische Definition der Spots 23 3.3.3 Verwendete Bestrahlungspläne 24 3.4 Messaufbau zur experimentellen Validierung 26 3.4.1 Target – PMMA-Phantom mit verschiedenen Cavitäten 27 3.4.2 Detektoren – CeBr3-Szintillatoren mit Photomultipliern 27 4 Ergebnisse und Diskussion 29 4.1 Simulierte Emission prompter Gammastrahlung 29 4.1.1 Simulierte Emissionsspektren 29 4.1.2 Simulierte Emissionsprofile 30 4.1.3 Totale Emissionsausbeute 31 4.2 Simulierte Detektion prompter Gammastrahlung 33 4.2.1 Detektionsrate und Raumwinkeleffekt 33 4.2.2 Simulierte PGT-Spektren 35 4.2.3 Simulierte Energiespektren 37 4.3 Vergleich simulierter und gemessener Spektren 39 4.3.1 Nachverarbeitung der Simulationsergebnisse 40 4.3.2 Auswahl des Energiefensters 45 4.3.3 Empirisches Modell zur Beschreibung der Zeitspektren 47 4.3.4 Diskussion systematischer Abweichungen 49 4.4 Sensitivität der Simulation gegenüber induzierten Reichweitenänderungen 51 5 Zusammenfassung und Ausblick 59 Anhang 61 A Parameter des Messaufbaus 61 B Angepasste Modellparameter aus Abbildung 4.12 62 C Sensitivität auf Reichweitenänderung bei 162 MeV 63 Literaturverzeichnis 69 / Proton therapy is characterized by steep dose gradients and thus a well-localizable energy transfer. To fully harness this potential, possibilities are being explored worldwide to verify the dose deposition and especially the range of protons in the patient. A promising method discovered only in the last decade is prompt gamma-ray timing (PGT), which relies on the dependence of the detected time-of-flight distribution of prompt gamma radiation on the transit time of protons in the patient. In this study, a Geant4 simulation is developed to predict PGT spectra during irradiation of a PMMA phantom and validated by comparison with experimental data. Both the emission yield of prompt gamma radiation in the phantom and the detection rate are analyzed depending on the proton energy. For comparability with the measured spectra, a multi-step processing of the simulated results is presented. Finally, the simulation is used to demonstrate the sensitivity of the PGT method to changes in range. For this purpose, cavities of different thicknesses and materials can be inserted into the phantom. For appropriately chosen distribution parameters of the simulated PGT spectra, their detected change is compared to the known induced change in range. The sensitivity determined in this way is consistent with previous results for measured spectra within the uncertainties.:1 Einleitung und Motivation 1 2 Theoretische Grundlagen 5 2.1 Wechselwirkung von Protonen mit Materie 5 2.1.1 Bethe-Bloch-Gleichung 6 2.1.2 Reichweite im CSDA-Modell 9 2.1.3 Tiefendosiskurve und Bragg-Peak 10 2.2 Prompt Gamma-Ray Timing 11 2.2.1 Emission prompter Gammastrahlung 11 2.2.2 Korrelation zur Protonen-Reichweite und Dosisdeposition 11 2.2.3 Idee des Prompt Gamma-Ray Timings 14 3 Material und Methoden 17 3.1 Dresdner IBA-Protonentherapie 17 3.1.1 Beschleunigungsprinzip des Isochronzyklotrons 17 3.1.2 Zeitliche Struktur der Protonen-Pakete 18 3.2 Teilchentransportrechnungen mit Geant4 20 3.3 PLD-Format für Pencil-Beam-Scanning-Pläne 21 3.3.1 Geometrische Definition der Spots 21 3.3.2 Dosimetrische Definition der Spots 23 3.3.3 Verwendete Bestrahlungspläne 24 3.4 Messaufbau zur experimentellen Validierung 26 3.4.1 Target – PMMA-Phantom mit verschiedenen Cavitäten 27 3.4.2 Detektoren – CeBr3-Szintillatoren mit Photomultipliern 27 4 Ergebnisse und Diskussion 29 4.1 Simulierte Emission prompter Gammastrahlung 29 4.1.1 Simulierte Emissionsspektren 29 4.1.2 Simulierte Emissionsprofile 30 4.1.3 Totale Emissionsausbeute 31 4.2 Simulierte Detektion prompter Gammastrahlung 33 4.2.1 Detektionsrate und Raumwinkeleffekt 33 4.2.2 Simulierte PGT-Spektren 35 4.2.3 Simulierte Energiespektren 37 4.3 Vergleich simulierter und gemessener Spektren 39 4.3.1 Nachverarbeitung der Simulationsergebnisse 40 4.3.2 Auswahl des Energiefensters 45 4.3.3 Empirisches Modell zur Beschreibung der Zeitspektren 47 4.3.4 Diskussion systematischer Abweichungen 49 4.4 Sensitivität der Simulation gegenüber induzierten Reichweitenänderungen 51 5 Zusammenfassung und Ausblick 59 Anhang 61 A Parameter des Messaufbaus 61 B Angepasste Modellparameter aus Abbildung 4.12 62 C Sensitivität auf Reichweitenänderung bei 162 MeV 63 Literaturverzeichnis 69

In der formalen Verifikation digitaler Schaltkreise hat sich die Methodik der vollständigen Verifikation anhand spezieller Operationseigenschaften bewährt. Operationseigenschaften beschreiben das Verhalten einer Schaltung in einem festen Zeitintervall und können sequentiell miteinander verknüpft werden, um so das Gesamtverhalten zu spezifizieren. Zusätzlich beweist eine formale Vollständigkeitsprüfung, dass die Menge der Eigenschaften für jede Folge von Eingangssignalwerten die Ausgänge der zu verifizierenden Schaltung eindeutig und lückenlos determiniert. In dieser Arbeit wird untersucht, wie aus Operationseigenschaften, deren Vollständigkeit erfolgreich bewiesen wurde, automatisiert eine Schaltungsbeschreibung abgeleitet werden kann. Gegenüber der traditionellen Entwurfsmethodik auf Register-Transfer-Ebene (RTL) bietet dieses Verfahren zwei Vorteile. Zum einen vermeidet der Vollständigkeitsbeweis viele Arten von Entwurfsfehlern, zum anderen ähnelt eine Beschreibung mit Hilfe von Operationseigenschaften den in Spezifikationen häufig genutzten Zeitdiagrammen, sodass die Entwurfsebene der Spezifikationsebene angenähert wird und Fehler durch manuelle Verfeinerungsschritte vermieden werden. Das Entwurfswerkzeug vhisyn führt die High-Level-Synthese (HLS) einer vollständigen Menge von Operationseigenschaften zu einer Beschreibung auf RTL durch. Die Ergebnisse zeigen, dass sowohl die verwendeten Synthesealgorithmen, als auch die erzeugten Schaltungen effizient sind und somit die Realisierung größerer Beispiele zulassen. Anhand zweier Fallstudien kann dies praktisch nachgewiesen werden. / The complete verification approach using special operation properties is an accepted methodology for the formal verification of digital circuits. Operation properties describe the behavior of a circuit during a certain time interval. They can be sequentially concatenated in order to specify the overall behavior. Additionally, a formal completeness check proves that the sequence of properties consistently determines the exact value of the output signals for every valid sequence of input signal values. This work examines how a circuit description can be automatically derived from a set of operation properties whose completeness has been proven. In contrast to the traditional design flow at register-transfer level (RTL), this method offers two advantages. First, the prove of completeness helps to avoid many design errors. Second, the design of operation properties resembles the design of timing diagrams often used in textual specifications. Therefore, the design level is closer to the specification level and errors caused by refinement steps are avoided. The design tool vhisyn performs the high-level synthesis from a complete set of operation properties to a description at RTL. The results show that both the synthesis algorithms and the generated circuit descriptions are efficient and allow the design of larger applications. This is demonstrated by means of two case studies.

Mit der steigenden Nachfrage nach Innovationen spielt Software in verschiedenenWirtschaftsbereichen eine wichtige Rolle, wie z.B. in der Automobilindustrie, bei intelligenten Systemen als auch bei Kommunikationssystemen. Daher ist die Qualität für die Softwareentwicklung von großer Bedeutung. Allerdings ändern sich die probabilistische Modelle (die Qualitätsbewertungsmodelle) angesichts der dynamischen Natur moderner Softwaresysteme. Dies führt dazu, dass ihre Übergangswahrscheinlichkeiten im Laufe der Zeit schwanken, welches zu erheblichen Problemen führt. Dahingehend werden probabilistische Modelle im Hinblick auf ihre Laufzeit kontinuierlich aktualisiert. Eine fortdauernde Neubewertung komplexer Wahrscheinlichkeitsmodelle ist jedoch teuer. In letzter Zeit haben sich inkrementelle Ansätze als vielversprechend für die Verifikation von adaptiven Systemen erwiesen. Trotzdem wurden bei der Bewertung struktureller Änderungen im Modell noch keine wesentlichen Verbesserungen erzielt. Wahrscheinlichkeitssysteme werden als Automaten modelliert, wie bei Markov-Modellen. Solche Modelle können in Matrixform dargestellt werden, um die Gleichungen basierend auf Zuständen und Übergangswahrscheinlichkeiten zu lösen. Laufzeitmodelle wie Matrizen sind nicht signifikant, um die Auswirkungen von Modellveränderungen erkennen zu können. In dieser Arbeit wird ein Framework unter Verwendung stochastischer Bäume mit regulären Ausdrücken entwickelt, welches modular aufgebaut ist und eine aktionshaltige sowie probabilistische Logik im Kontext der Modellprüfung aufweist. Ein solches modulares Framework ermöglicht dem Menschen die Entwicklung der Änderungsoperationen für die inkrementelle Berechnung lokaler Änderungen, die im Modell auftreten können. Darüber hinaus werden probabilistische Änderungsmuster beschrieben, um eine effiziente inkrementelle Verifizierung, unter Verwendung von Bäumen mit regulären Ausdrücken, anwenden zu können. Durch die Bewertung der Ergebnisse wird der Vorgang abgeschlossen. / Software plays an innovative role in many different domains, such as car industry, autonomous and smart systems, and communication. Hence, the quality of the software is of utmost importance and needs to be properly addressed during software evolution. Several approaches have been developed to evaluate systems’ quality attributes, such as reliability, safety, and performance of software. Due to the dynamic nature of modern software systems, probabilistic models representing the quality of the software and their transition probabilities change over time and fluctuate, leading to a significant problem that needs to be solved to obtain correct evaluation results of quantitative properties. Probabilistic models need to be continually updated at run-time to solve this issue. However, continuous re-evaluation of complex probabilistic models is expensive. Recently, incremental approaches have been found to be promising for the verification of evolving and self-adaptive systems. Nevertheless, substantial improvements have not yet been achieved for evaluating structural changes in the model. Probabilistic systems are usually represented in a matrix form to solve the equations based on states and transition probabilities. On the other side, evolutionary changes can create various effects on theese models and force them to re-verify the whole system. Run-time models, such as matrices or graph representations, lack the expressiveness to identify the change effect on the model. In this thesis, we develop a framework using stochastic regular expression trees, which are modular, with action-based probabilistic logic in the model checking context. Such a modular framework enables us to develop change operations for the incremental computation of local changes that can occur in the model. Furthermore, we describe probabilistic change patterns to apply efficient incremental quantitative verification using stochastic regular expression trees and evaluate our results.

Verification of knowledge-bases is a critical step to ensure the quality of a knowledge-based system. The success of these systems depends heavily on how qualitative the knowledge is. Manual verification is however cumbersome and error prone, especially for large knowledge-bases. This thesis provides a design theory, based upon the suggested framework by Gregor and Jones (2007). The theory proposes a general design of automated verification tools, which have the abilities of verifying heuristic knowledge in rule-based systems utilizing certainty factors. Included is a verification of completeness and consistency technique customized to this class of knowledge-based systems. The design theory is instantiated in a real-world verification tool development project at Uppsala University. Considerable attention is given to the design and implementation of this artifact – uncovering issues and considerations involved in the development process. For the knowledge management practitioner, this thesis offers guidance and recommendations for automated verification tool development projects. For the IS research community, the thesis contributes with extensions of existing design theory, and reveals some of the complexity involved with verification of a specific rule-based system utilizing certainty factors.

Model Driven Development is used to improve software quality and efficiency by automatically transforming abstract and formal models into software implementations. This is particularly sensible if the model’s integrity can be proven formally and is preserved during the model’s transformation. A standard to specify software model integrity is the Object Constraint Language (OCL). Another topic of research is the dynamic development of software components, enabling software system composition at component run-time. As a consequence, the system’s verification must be realized during system run-time (and not during transformation or compile time). Many established verification techniques cannot be used for run-time verification. A method to enable model-based run-time verification will be developed during this work. How OCL constraints can be transformed into executable software artifacts and how they can be used in the component-based system Treaty will be the major task of this diploma thesis. / Modellgetriebene Entwicklung dient der Verbesserung von Qualität und Effizienz in der Software-Entwicklung durch Automatisierung der notwendigen Transformationen von abstrakten bzw. formalen Modellen bis zur Implementierung. Dies ist insbesondere dann sinnvoll, wenn die Integrität der ursprünglichen Modelle formal bewiesen werden kann und durch die Transformation gewährleistet wird. Ein Standard zur Spezifikation der Integrität von Softwaremodellen ist die Object Constraint Language (OCL). Eine weitere Forschungsrichtung im Software-Engineering ist die Entwicklung von dynamischen Komponenten-Modellen, die die Komposition von Softwaresystemen im laufenden Betrieb ermöglichen. Dies bedeutet, dass die Systemverifikation im laufenden Betrieb realisiert werden muss. Die meisten der etablierten Verifikationstechniken sind dazu nicht geeignet. In der Diplomarbeit soll ausgehend von diesem Stand der Technik eine Methode zur modellbasierten Verifikation zur Laufzeit entwickelt werden. Insbesondere soll untersucht werden, wie OCL-Constraints zur Laufzeit in ausführbare Software-Artefakte übersetzt und in dem komponentenbasierten System Treaty verwendet werden können.

In the recent trends, automated systems are increasingly seen to be embedded in human life with the increase of human dependence on software to perform safetycritical tasks like airbag deployment in automobiles to real-time mission planning in UAVs (Unmanned Aircraft Vehicles). The safety-critical nature of the aerospace domain demands for a software without any errors to perform these tasks. Therefore the field of computer science needs to address these challenges by providing necessary formalisms, techniques, and tools that will ensure the correctness of systems despite their complexity. DO-178C/EC-12C is a standard that governs the certification of software for airborne systems in commercial aircraft. The additional supplement DO- 333 enables us to use the formal methods in our technique of verifying the autonomous behaviour of UAV’s. The Mission Manager system is primarily responsible for the execution of behaviour sequence in online and offline mission planning of UAV. This work presents the process of software verification by making use of formal modelling using model checking of the Mission Manager component of ARTIS (Autonomous Rotorcraft Testbed for Intelligent Systems) UAV by gaining advantages from a generic modelling approach. The main idea is to make use of the designed generic models into specific cases like ARTIS in our case. The generic models are designed using the ALFU(R)S (Autonomy Levels For Unmanned Rotorcraft System) framework that delineates the commonalities of several UAVs considered around the world which also includes the ARTIS UAV. Furthermore this work walks through every process involved in model checking like requirements extraction and documentation using a template based method, requirements specification using the temporal logics like LTL and CTL, developing a formal model using NuSMV as a model checking tool to analyze the requirements against the model for the Mission Manager component of MiPlEx (Mission Planning and Execution). Additionally as a validation approach, test sequences are generated by using trap properties or negation properties. This aids for a test generation approach by harnessing counterexample generating capabilities of the NuSMV Model Checker.