Master of Science / Department of Computing and Information Sciences / John Hatcliff / Like all businesses, clinical care groups and facilities are under a range of pressures to enhance the efficacy of their operations. Though there are a number of ways to go about these improvements, one exciting methodology involves the documentation and analysis of clinical workflows. Unfortunately, there is no industry standard tool which supports this, and many available workflow documentation technologies are not only proprietary, but technologically insufficient as well. Ideally, these workflows would be documented at a formal enough level to support their execution; this would allow the partial automation of documented clinical procedures. However, the difficulty involved in this automation effort is substantial: not only is there the irreducible complexity inherent to automation, but a number of the solutions presented so far layer on additional complication. To solve this, the author introduces Kinerja, a state-of-the-art execution environment for formally specified workflows. Operating on a subset of the academically and industrially proven workflow language YAWL, Kinerja allows for both human guided governance and computer guided verification of workflows, and allows for a seamless switching between modalities. Though the base of Kinerja is essentially an integrated framework allowing for considerable extensibility, a number of modules have already been developed to support the checking and executing of clinical workflows. One such module integrates symbolic execution which greatly optimizes the time and space necessary for a complete exploration of a workflow's state space.

Le model checking est une technique établie pour vérifier automatiquement qu’un modèle vérifie une propriété temporelle donnée. Lorsque le modèle viole la propriété, le model checker retourne un contre-exemple, i.e., une séquence d’actions menant à un état où la propriété n’est pas satisfaite. Comprendre ce contre-exemple pour le débogage de la spécification est une tâche compliquée pour plusieurs raisons: (i) le contre-exemple peut contenir un grand nombre d’actions; (ii) la tâche de débogage est principalement réalisée manuellement; (iii) le contre-exemple n’indique pas explicitement la source du bogue qui est caché dans le modèle; (iv) les actions les plus pertinentes ne sont pas mises en évidence dans le contre-exemple; (v) le contre-exemple ne donne pas une vue globale du problème.Ce travail présente une nouvelle approche qui rend plus accessible le model checking en simplifiant la compréhension des contre-exemples. Notre solution vise à ne garder que des actions dans des contre-exemples pertinents à des fins de débogage. Pour y parvenir, on détecte dans les modèles des choix spécifiques entre les transitions conduisant à un comportement correct ou à une partie du modèle erroné. Ces choix, que nous appelons neighbourhoods, se révèlent être de grande importance pour la compréhension du bogue à travers le contre-exemple. Pour extraire de tels choix, nous proposons deux méthodes différentes. La première méthode concerne le débogage des contre-exemples pour la violations de propriétés de sûreté. Pour ce faire, elle construit un nouveau modèle de l’original contenant tous les contre-exemples, puis compare les deux modèles pour identifier les neighbourhoods. La deuxième méthode concerne le débogage des contre-exemples pour la violations de propriétés de vivacité. À partir d’une propriété de vivacité, elle étend le modèle avec des informations de préfixe / suffixe correspondants à cette propriété. Ce modèle enrichi est ensuite analysé pour identifier les neighbourhoods.Un modèle annoté avec les neighbourhoods peut être exploité de deux manières. Tout d’abord, la partie erronée du modèle peut être visualisée en se focalisant sur les neighbourhoods, afin d’avoir une vue globale du comportement du bogue. Deuxièmement, un ensemble de techniques d’abstraction que nous avons développées peut être utilisé pour extraire les actions plus pertinentes à partir de contre-exemples, ce qui facilite leur compréhension. Notre approche est entièrement automatisée par un outil que nous avons implémenté et qui a été validé sur des études de cas réels dans différents domaines d’application. / Model checking is an established technique for automatically verifying that a model satisfies a given temporal property. When the model violates the property, the model checker returns a counterexample, which is a sequence of actions leading to a state where the property is not satisfied. Understanding this counterexample for debugging the specification is a complicated task for several reasons: (i) the counterexample can contain a large number of actions; (ii) the debugging task is mostly achieved manually; (iii) the counterexample does not explicitly point out the source of the bug that is hidden in the model; (iv) the most relevant actions are not highlighted in the counterexample; (v) the counterexample does not give a global view of the problem.This work presents a new approach that improves the usability of model checking by simplifying the comprehension of counterexamples. Our solution aims at keeping only actions in counterexamples that are relevant for debugging purposes. This is achieved by detecting in the models some specific choices between transitions leading to a correct behaviour or falling into an erroneous part of the model. These choices, which we call "neighbourhoods", turn out to be of major importance for the understanding of the bug behind the counterexample. To extract such choices we propose two different methods. One method aims at supporting the debugging of counterexamples for safety properties violations. To do so, it builds a new model from the original one containing all the counterexamples, and then compares the two models to identify neighbourhoods. The other method supports the debugging of counterexamples for liveness properties violations. Given a liveness property, it extends the model with prefix / suffix information w.r.t. that property. This enriched model is then analysed to identify neighbourhoods.A model annotated with neighbourhoods can be exploited in two ways. First, the erroneous part of the model can be visualized with a specific focus on neighbourhoods, in order to have a global view of the bug behaviour. Second, a set of abstraction techniques we developed can be used to extract relevant actions from counterexamples, which makes easier their comprehension. Our approach is fully automated by a tool we implemented and that has been validated on real-world case studies from various application areas.

Les systèmes distribués sont au coeur des technologies de l'information.Il est devenu classique de s'appuyer sur multiples unités distribuées pour améliorer la performance d'une application, la tolérance aux pannes, ou pour traiter problèmes dépassant les capacités d'une seule unité de traitement. La conception d'algorithmes adaptés au contexte distribué est particulièrement difficile en raison de l'asynchronisme et du non-déterminisme qui caractérisent ces systèmes. La simulation offre la possibilité d'étudier les performances des applications distribuées sans la complexité et le coût des plates-formes d'exécution réelles. Par ailleurs, le model checking permet d'évaluer la correction de ces systèmes de manière entièrement automatique. Dans cette thèse, nous explorons l'idée d'intégrer au sein d'un même outil un model checker et un simulateur de systèmes distribués. Nous souhaitons ainsi pouvoir évaluer la performance et la correction des applications distribuées. Pour faire face au problème de l'explosion combinatoire des états, nous présentons un algorithme de réduction dynamique par ordre partiel (DPOR), qui effectue une exploration basée sur un ensemble réduit de primitives de réseau. Cette approche permet de vérifier les programmes écrits avec n'importe laquelle des interfaces de communication proposées par le simulateur. Nous avons pour cela développé une spécification formelle complète de la sémantique de ces primitives réseau qui permet de raisonner sur l'indépendance des actions de communication nécessaire à la DPOR. Nous montrons au travers de résultats expérimentaux que notre approche est capable de traiter des programmes C non triviaux et non modifiés, écrits pour le simulateur SimGrid. Par ailleurs, nous proposons une solution au problème du passage à l'échelle des simulations limitées pour le CPU, ce qui permet d'envisager la simulation d'applications pair-à-pair comportant plusieurs millions de noeuds. Contrairement aux approches classiques de parallélisation, nous proposons une parallélisation des étapes internes de la simulation, tout en gardant l'ensemble du processus séquentiel. Nous présentons une analyse de la complexité de l'algorithme de simulation parallèle, et nous la comparons à l'algorithme classique séquentiel pour obtenir un critère qui caractérise les situations où un gain de performances peut être attendu avec notre approche. Un résultat important est l'observation de la relation entre la précision numérique des modèles utilisés pour simuler les ressources matérielles, avec le degré potentiel de parallélisation atteignables avec cette approche. Nous présentons plusieurs cas d'étude bénéficiant de la simulation parallèle, et nous détaillons les résultats d'une simulation à une échelle sans précédent du protocole pair-à-pair Chord avec deux millions de noeuds, exécutée sur une seule machine avec un modèle précis du réseau / Distributed systems are in the mainstream of information technology. It has become standard to rely on multiple distributed units to improve the performance of the application, help tolerate component failures, or handle problems too large to fit in a single processing unit. The design of algorithms adapted to the distributed context is particularly difficult due to the asynchrony and the nondeterminism that characterize distributed systems. Simulation offers the ability to study the performance of distributed applications without the complexity and cost of the real execution platforms. On the other hand, model checking allows to assess the correctness of such systems in a fully automatic manner. In this thesis, we explore the idea of integrating a model checker with a simulator for distributed systems in a single framework to gain performance and correctness assessment capabilities. To deal with the state explosion problem, we present a dynamic partial order reduction algorithm that performs the exploration based on a reduced set of networking primitives, that allows to verify programs written for any of the communication APIs offered by the simulator. This is only possible after the development of a full formal specification with the semantics of these networking primitives, that allows to reason about the independency of the communication actions as required by the DPOR algorithm. We show through experimental results that our approach is capable of dealing with non trivial unmodified C programs written for the SimGrid simulator. Moreover, we propose a solution to the problem of scalability for CPU bound simulations, envisioning the simulation of Peer-to-Peer applications with millions of participating nodes. Contrary to classical parallelization approaches, we propose parallelizing some internal steps of the simulation, while keeping the whole process sequential. We present a complexity analysis of the simulation algorithm, and we compare it to the classical sequential algorithm to obtain a criteria that describes in what situations a speed up can be expected. An important result is the observation of the relation between the precision of the models used to simulate the hardware resources, and the potential degree of parallelization attainable with this approach. We present several case studies that benefit from the parallel simulation, and we show the results of a simulation at unprecedented scale of the Chord Peer-to-Peer protocol with two millions nodes executed in a single machine

"Timing diagrams are used in industrial practice as a specification language of circuit components. They have been formalized for efficient use in model checking. This formalization is often more succinct and convenient than the use of temporal logic. We explore the relationship between timing diagrams and temporal logic formulas by showing that closure under disjunction does not hold for timing diagrams. We give an algorithm that returns a disjunction (if any) of two given timing diagrams. We also give algorithms that decide satisfiability of a timing diagram and return exact time separations between events in a timing diagram. An Alloy specification for timing diagrams with one waveform has also been built."

Task parallel programming languages provide a way for creating asynchronous tasks that can run concurrently. The advantage of using task parallelism is that the programmer can write code that is independent of the underlying hardware. The runtime determines the number of processor cores that are available and the most efficient way to execute the tasks. When two or more concurrently executing tasks access a shared memory location and if at least one of the accesses is for writing, data race is observed in the program. Data races can introduce non-determinism in the program output making it important to have data race detection tools. To detect data races in task parallel programs, a new Sound and Complete technique based on computation graphs is presented in this work. The data race detection algorithm runs in O(N2) time where N is number of nodes in the graph. A computation graph is a directed acyclic graph that represents the execution of the program. For detecting data races, the computation graph stores shared heap locations accessed by the tasks. An algorithm for creating computation graphs augmented with memory locations accessed by the tasks is also described here. This algorithm runs in O(N) time where N is the number of operations performed in the tasks. This work also presents an implementation of this technique for the Java implementation of the Habanero programming model. The results of this data race detector are compared to Java Pathfinder's precise race detector extension and permission regions based race detector extension. The results show a significant reduction in the time required for data race detection using this technique.

Cette thèse se situe dans la problématique de la conduite en convoi de véhicules autonomes : des ensembles de véhicules qui se déplacent en conservant une configuration spatiale, sans aucune accroche matérielle. Ses objectifs sont d'abord, la définition d'une approche de prise de décision pour les systèmes de convois de véhicules, puis, la définition d'une approche de vérification, adaptée à la preuve de propriétés relatives aux convois de véhicules, avec une attention particulière envers les propriétés de sûreté.L'approche pour la prise de décision est décentralisée et auto organisée : chaque véhicule détermine son comportement de façon locale, à partir de ses propres capacités de perception, sans avoir recours à une communication explicite, de telle sorte que l'organisation du convoi, son maintien et son évolution soient le résultat émergeant du comportement de chaque véhicule. L'approche proposée s'applique a des convois suivant plusieurs types de configuration, et permet des changements dynamiques de configuration.L'approche proposée pour la vérification de propriétés de sûreté des convois de véhicules, adopte le model-checking comme technique de preuve. Pour contourner le problème de l'explosion combinatoire, rencontré dans la vérification des systèmes complexes, nous avons proposé une méthode compositionnelle de vérification, qui consiste a décomposer le système en sous systèmes et à associer une propriété auxiliaire à chacun des sous systèmes. La propriété globale sera ensuite déduite de l'ensemble des propriétés auxiliaires, par l'application d'une règle de déduction compositionnelle. La complexité calculatoire est mieux maîtrisée car le model-checking s'applique aux sous-systèmes. Nous proposons une règle de déduction adaptée aux systèmes de conduite en convoi, en particulier ceux qui sont basés sur des approches décentralisées. La règle considère chaque véhicule comme un composant. Elle est consistante sous la condition que l'ajout d'un nouveau composant au système n'a pas d'influence sur le comportement du reste du système. L'approche décentralisée proposée pour la conduite en convoi satisfait cette condition. Deux propriétés de sûreté ont été vérifiées : absence de collision et évolution confortable pour les passagers / This thesis places in the framework of Platoons, sets of autonomous vehicles that move together while keeping a spatial configuration, without any material coupling. Goals of the thesis are: first, the definition of a decision making approach for platoon systems. Second, the definition of a method for the verification of safety properties associated to the platoon system.The proposed decision making approach is decentralized and self-organized. Platoon vehicles are autonomous, they act based only on their perception capabilities. The configuration emerges as a result of the individual behavior of each of the platoon vehicle. The proposed approach can be applied to platoon with different configurations, and allows for dynamic change of configuration.The proposed verification method uses the model-checking technique. Model checking of complex system can lead to the combinatory explosion problem. To deal with this problem, we choose to use a compositional verification method. Compositional methods decompose system models into different components and associate to each component an auxiliary property. The global property can then be deduced from the set of all the auxiliary properties, by applying a compositional deduction rule. We define a deduction rule suitable for decentralised platoon systems. The deduction rule considers each vehicle as a component. It is applicable under the assumption that adding a new component to an instance of the system does not modify behavior of the instance. Two safety properties have been verified : collision avoidance.

Im Rahmen dieser Arbeit werden die Nebenläufigkeit, Konsistenz und Latenz in asynchronen Interaktiven Echtzeitsystemen durch die Techniken des Profilings und des Model Checkings untersucht. Zu Beginn wird erläutert, warum das asynchrone Modell das vielversprechendste für die Nebenläufigkeit in einem Interaktiven Echtzeitsystem ist. Hierzu wird ein Vergleich zu anderen Modellen gezogen. Darüber hinaus wird ein detaillierter Vergleich von Synchronisationstechnologien, welche die Grundlage für Konsistenz schaffen, durchgeführt. Auf der Grundlage dieser beiden Vergleiche und der Betrachtung anderer Systeme wird ein Synchronisationskonzept entwickelt. Auf dieser Basis wird die Nebenläufigkeit, Konsistenz und Latenz mit zwei Verfahren untersucht. Die erste Technik ist das Profiling, wobei einige neue Darstellungsformen von gemessenen Daten entwickelt werden. Diese neu entwickelten Darstellungsformen werden in der Implementierung eines Profilers verwendet. Als zweite Technik wird das Model Checking analysiert, welches bisher noch nicht im Kontext von Interaktiven Echtzeitsystemen verwendet wurde. Model Checking dient dazu, die Verhaltensweise eines Interaktiven Echtzeitsystems vorherzusagen. Diese Vorhersagen werden mit den Messungen aus dem Profiler verglichen. / In this thesis the concurrency, latency, and consistency of asynchronous Realtime Interactive Systems (RIS) are analyzed using profiling and model checking. At the beginning, it is described why the Asynchronous Model is the most promising model to increase concurrency in a RIS. Therefore, it is compared to several other models. Furthermore, synchronization techniques are compared, which are used to provide consistency in a concurrent application. Upon both results, a synchronization concept is created. Using this concept, the concurrency, latency, and consistency are analyzed using two techniques. The first technique is profiling. New visualizations are developed to visualize profiling data measured by profiling. The second technique is model checking. In this thesis, model checking is used for the first time in context of a RIS. Model checking is used to predict the behavior of a RIS. The predicition and the measurement from the profiling are compared.

Today, information and communication systems are ubiquitous and consist very often of several interacting and communicating components. One reason is the widespread use of multi-core processors and the increasing amount of concurrent software for the efficient usage of multi-core processors. Also, the dissemination of distributed emergent technologies like sensor networks or the internet of things is growing. Additionally, a lot of internet protocols are client-server architectures with clients which execute computations in parallel and servers that can handle requests of several clients in parallel. Systems which consist of several interacting and communicating components are often very complex and due to their complexity also prone to errors. Errors in systems can have dramatic consequenses, especially in safety-critical areas where human life can be endangered by incorrect system behavior. Hence, it is inevitable to have methods that ensure the proper functioning of such systems. This thesis aims on improving the verifiability of asynchronous concurrent systems using symbolic model checking based on Binary Decision Diagrams (BDDs). An asynchronous concurrent system is a system that consists of several components, from which only one component can execute a transition at a time. Model checking is a formal verification technique. For a given system description and a set of desired properties, the validity of the properties for the system is decided in model checking automatically by software tools called model checkers. The main problem of model checking is the state-space explosion problem. One approach to reduce this problem is the use of symbolic model checking. There, system states and transitions are not stored explicitely as in explicit model checking. Instead, in symbolic model checking sets of states and sets of transitions are stored and also manipulated together. The data structure which is used in this thesis to store those sets are BDDs. BDD-based symbolic model checking has already been used successful in industry for several times. Nevertheless, BDD-based symbolic model checking still suffers from the state-space explosion problem and further improvements are necessary to improve its applicability. Central operations in BDD-based symbolic model checking are the computation of successor and predecessor states of a given set of states. Those computations are called image computations. They are applied repeatedly in BDD-based symbolic model checking to decide the validity of properties for a given system description. Hence, their efficient execution is crucial for the memory and runtime requirements of a model checker. In an image computation a BDD for a set of transitions and a BDD for a set of states are combined to compute a set of successor or predecessor states. Often, also the size of the BDDs to represent the transition relation is critical for the successful use of model checking. To further improve the applicability of symbolic model checking, we present in this thesis new data structures to store the transition relation of asynchronous concurrent systems. Additionally, we present new image computation algorithms. Both can lead to large runtime and memory reductions for BDD-based symbolic model checking. Asynchronous concurrent systems often contain symmetries. A technique to exploit those symmetries to diminish the state-space explosion problem is symmetry reduction. In this thesis we also present a new efficient algorithm for symmetry reduction in BDD-based symbolic model checking. / In unserem Alltag kommen wir heute ständig mit Systemen der Informations- und Kommunikationstechnik in Kontakt. Diese bestehen häufig aus mehreren interagierenden und kommunizierenden Komponenten, wie zum Beispiel nebenläufige Software zur effizienten Nutzung von Mehrkernprozessoren oder Sensornetzwerke. Systeme, die aus mehreren interagierenden und kommunizierenden Komponenten bestehen sind häufig komplex und dadurch sehr fehleranfällig. Daher ist es wichtig zuverlässige Methoden, die helfen die korrekte Funktionsweise solcher Systeme sicherzustellen, zu besitzen. Im Rahmen dieser Doktorarbeit wurden neue Methoden zur Verbesserung der Verifizierbarkeit von asynchronen nebenläufigen Systemen durch Anwendung der symbolischen Modellprüfung mit binären Entscheidungsdiagrammen (BDDs) entwickelt. Ein asynchrones nebenläufiges System besteht aus mehreren Komponenten, von denen zu einem Zeitpunkt jeweils nur eine Komponente Transitionen ausführen kann. Die Modellprüfung ist eine Technik zur formalen Verifikation, bei der die Gültigkeit einer Menge von zu prüfenden Eigenschaften für eine gegebene Systembeschreibung automatisch durch Softwarewerkzeuge, die Modellprüfer genannt werden, entschieden wird. Das Hauptproblem der symbolischen Modellprüfung ist das Problem der Zustandsraumexplosion und es sind weitere Verbesserungen notwendig, um die symbolische Modellprüfung häufiger erfolgreich durchführen zu können. Bei der BDD-basierten symbolischen Modellprüfung werden Mengen von Systemzuständen und Mengen von Transitionen jeweils durch BDDs repräsentiert. Zentrale Operationen bei ihr sind die Berechnung von Nachfolger- und Vorgängerzuständen von gegebenen Zustandsmengen, welche Bildberechnungen genannt werden. Um die Gültigkeit von Eigenschaften für eine gegebene Systembeschreibung zu überprüfen, werden wiederholt Bildberechnungen durchgeführt. Daher ist ihre effiziente Berechnung entscheidend für eine geringe Laufzeit und einen niedrigen Speicherbedarf der Modellprüfung. In einer Bildberechnung werden ein BDD zur Repräsentation einer Menge von Transitionen und ein BDD für eine Menge von Zuständen kombiniert, um eine Menge von Nachfolger- oder Vorgängerzuständen zu berechnen. Oft ist auch die Größe von BDDs zur Repräsentation der Transitionsrelation von Systemen entscheidend für die erfolgreiche Anwendbarkeit der Modellprüfung. In der vorliegenden Arbeit werden neue Datenstrukturen zur Repräsentation der Transitionsrelation von asynchronen nebenläufigen Systemen bei der BDD-basierten symbolischen Modellprüfung vorgestellt. Zusätzlich werden neue Algorithmen zur Durchführung von Bildberechnungen präsentiert. Beides kann zu großen Reduktionen der Laufzeit und des Speicherbedarfs führen. Asynchrone nebenläufige Systeme besitzen häufig Symmetrien. Eine Technik zur Reduktion des Problems der Zustandsraumexplosion ist die Symmetriereduktion. In dieser Arbeit wird ebenfalls ein neuer effizienter Algorithmus zur Symmetriereduktion bei der symbolischen Modellprüfung mit BDDs aufgeführt.

<p>Embedded systems are becoming increasingly common in our everyday lives. As techonology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components (Intellectual Property blocks). At the same time, the systems must still fulfill strict requirements on reliability and correctness.</p><p>This thesis proposes a formal verification methodology which smoothly integrates with component-based system-level design using a divide and conquer approach. The methodology assumes that the system consists of several reusable components. Each of these components are already formally verified by their designers and are considered correct given that the environment satisfies certain properties imposed by the component. What remains to be verified is the glue logic inserted between the components. Each such glue logic is verified one at a time using model checking techniques.</p><p>The verification methodology as well as the underlying theoretical framework and algorithms are presented in the thesis.</p><p>Experimental results have shown the efficiency of the proposed methodology and demonstrated that it is feasible to apply it on real-life examples.</p> / Report code: LiU-Tek-Lic-2003:57.

Within the context of the verification of infinite-state systems, 'Regular model checking' is the name of a family of techniques in which states are represented by words or trees, sets of states by finite automata on these objects, and transitions by finite automata operating on pairs of state encodings, i.e. finite-state transducers. In this context, the problem of computing the set of reachable states of a system can be reduced to the one of computing the iterative closure of the finite-state transducer representing its transition relation. This thesis provides several techniques to computing the transitive closure of a finite-state transducer. One of the motivations of the thesis is to show the feasibility and usefulness of this approach through a combination of the necessary theoretical developments, implementation, and experimentation. For systems whose states are encoded by words, the iteration technique proceeds by comparing a finite sequence of successive powers of the transducer, detecting an 'increment' that is added to move from one power to the next, and extrapolating the sequence by allowing arbitrary repetitions of this increment. For systems whose states are represented by trees, the iteration technique proceeds by computing the powers of the transducer and progressively collapsing their states according to an equivalence relation until a fixed point is reached. The proposed iteration techniques can just as well be exploited to compute the closure of a given set of states by repeated applications of the transducer, which has proven to be a very effective way of using the technique. Various examples have been handled completely within the automata-theoretic setting. Another applications of the techniques are the verification of linear temporal properties as well as the computation of the convex hull of a finite set of integer vectors.