In der Dissertation werden neue Entwurfsmethoden für Kompaktoren für die Ausgänge von digitalen Schaltungen beschrieben, die die Anzahl der zu testenden Ausgänge drastisch verkleinern und dabei die Testbarkeit der Schaltungen nur wenig oder gar nicht verschlechtern. <br>Der erste Teil der Arbeit behandelt für kombinatorische Schaltungen Methoden, die die Struktur der Schaltungen beim Entwurf der Kompaktoren berücksichtigen. Verschiedene Algorithmen zur Analyse von Schaltungsstrukturen werden zum ersten Mal vorgestellt und untersucht. Die Komplexität der vorgestellten Verfahren zur Erzeugung von Kompaktoren ist linear bezüglich der Anzahl der Gatter in der Schaltung und ist damit auf sehr große Schaltungen anwendbar. <br>Im zweiten Teil wird erstmals ein solches Verfahren für sequentielle Schaltkreise beschrieben. Dieses Verfahren baut im wesentlichen auf das erste auf. <br>Der dritte Teil beschreibt eine Entwurfsmethode, die keine Informationen über die interne Struktur der Schaltung oder über das zugrundeliegende Fehlermodell benötigt. Der Entwurf basiert alleine auf einem vorgegebenen Satz von Testvektoren und die dazugehörenden Testantworten der fehlerfreien Schaltung. Ein nach diesem Verfahren erzeugter Kompaktor maskiert keinen der Fehler, die durch das Testen mit den vorgegebenen Vektoren an den Ausgängen der Schaltung beobachtbar sind. / The objective of this thesis is to provide new space compaction techniques for testing or concurrent checking of digital circuits. In particular, the work focuses on the design of space compactors that achieve high compaction ratio and minimal loss of testability of the circuits. <br>In the first part, the compactors are designed for combinational circuits based on the knowledge of the circuit structure. Several algorithms for analyzing circuit structures are introduced and discussed for the first time. The complexity of each design procedure is linear with respect to the number of gates of the circuit. Thus, the procedures are applicable to large circuits. <br>In the second part, the first structural approach for output compaction for sequential circuits is introduced. Essentially, it enhances the first part. <br>For the approach introduced in the third part it is assumed that the structure of the circuit and the underlying fault model are unknown. The space compaction approach requires only the knowledge of the fault-free test responses for a precomputed test set. The proposed compactor design guarantees zero-aliasing with respect to the precomputed test set.

Pyrosequencing is a DNA sequencing method based on thedetection of released pyrophosphate (PPi) during DNA synthesis.In a cascade of enzymatic reactions, visible light isgenerated, which is proportional to the number of nucleotidesincorporated into the DNA template. When dNTP(s) areincorporated into the DNA template, inorganic PPi is released.The released PPi is converted to ATP by ATP sulfurylase, whichprovides the energy to luciferase to oxidize luciferin andgenerate light. The excess of dNTP(s) and the ATP produced areremoved by the nucleotide degrading enzyme apyrase. The commercially available enzymes, isolated from nativesources, show batch-tobatch variations in activity and quality,which decrease the efficiency of the Pyrosequencing reaction.Therefore, the aim of the research presented in this thesis wasto develop methods to recombinantly produce the enzymes used inthe Pyrosequencing method. Production of the nucleotidedegrading enzyme apyrase by Pichia pastoris expression system,both in small-scale and in an optimized large-scale bioreactor,is described. ATP sulfurylase, the second enzyme in thePyrosequencing reaction, was produced inEscherichia coli. The protein was purified and utilizedin the Pyrosequencing method. Problems associated with enzymecontamination (NDP kinase) and batch-to-batch variations wereeliminated by the use of the recombinant ATP sulfurylase. As a first step towards sequencing on chip-format,SSB-(single-strand DNA binding protein)-luciferase and KlenowDNA polymerase-luciferase fusion proteins were generated inorder to immobilize the luciferase onto the DNA template. The application field for the Pyrosequencing technology wasexpanded by introduction of a new method for clone checking anda new method for template preparation prior the Pyrosequencingreaction. Keywords:apyrase, Pyrosequencing technology, Zbasictag fusion, luciferase, ATP sulfurylase, dsDNAsequencing, clone checking, Klenow-luciferase, SSB-luciferase,Pichia pastoris, Echerichia coli.

Embedded systems are becoming increasingly common in our everyday lives. As technology progresses, these systems become more and more complex. Designers handle this increasing complexity by reusing existing components. At the same time, the systems must fulfill strict functional and non-functional requirements. This thesis presents novel and efficient techniques for the verification of component-based embedded system designs. As a common basis, these techniques have been developed using a Petri net based modelling approach, called PRES+. Two complementary problems are addressed: component verification and integration verification. With component verification the providers verify their components so that they function correctly if given inputs conforming to the assumptions imposed by the components on their environment. Two techniques for component verification are proposed in the thesis. The first technique enables formal verification of SystemC designs by translating them into the PRES+ representation. The second technique involves a simulation based approach into which formal methods are injected to boost verification efficiency. Provided that each individual component is verified and is guaranteed to function correctly, the components are interconnected to form a complete system. What remains to be verified is the interface logic, also called glue logic, and the interaction between components. Each glue logic and interface cannot be verified in isolation. It must be put into the context in which it is supposed to work. An appropriate environment must thus be derived from the components to which the glue logic is connected. This environment must capture the essential properties of the whole system with respect to the properties being verified. In this way, both the glue logic and the interaction of components through the glue logic are verified. The thesis presents algorithms for automatically creating such environments as well as the underlying theoretical framework and a step-by-step roadmap on how to apply these algorithms.

Today's EDA (Electronic Design Automation) industry faces enormous challenges. Their primary cause is the tremendous increase of the complexity of modern digital designs. Graph algorithms are widely applied to solve various EDA problems. In particular, graph dominators, which provide information about the origin and the end of reconverging paths in a circuit graph, proved to be useful in various CAD (Computer Aided Design) applications such as equivalence checking, ATPG, technology mapping, and power optimization. This thesis provides a study on graph dominators in logic synthesis and verification. The thesis contributes a set of algorithms for computing dominators in circuit graphs. An algorithm is proposed for finding absolute dominators in circuit graphs. The achieved speedup of three orders of magnitude on several designs enables the computation of absolute dominators in large industrial designs in a few seconds. Moreover, the computation of single-vertex dominators in large multiple-output circuit graphs is considerably improved. The proposed algorithm reduces the overall runtime by efficiently recognizing and re-using isomorphic structures in dominator trees rooted at different outputs of the circuit graph. Finally, common multiple-vertex dominators are introduced. The algorithm to compute them is faster and finds more multiple-vertex dominators than previous approaches. The thesis also proposes new dominator-based algorithms in the area of decomposition and combinational equivalence checking. A structural decomposition technique is introduced, which finds all simple-disjoint decompositions of a Boolean function which are reflected in the circuit graph. The experimental results demonstrate that the proposed technique outperforms state-of-the-art functional decomposition techniques. Finally, an approach to check the equivalence of two Boolean functions probabilistically is investigated. The proposed algorithm partitions the equivalence check employing dominators in the circuit graph. The experimental results confirm that, in comparison to traditional BDD-based equivalence checking methods, the memory consumption is considerably reduced by using the proposed technique. / QC 20100804

Message Passing Interface (MPI) is a standard library interface for writing parallel programs. The MPI specification is broadly used for solving engineering and scientific problems on parallel computers, and MPICH2 is a popular MPI implementation developed at Argonne National Laboratory. The scalability of MPI implementations is very important for building high performance parallel computing applications. The initial TCP (Transmission Control Protocol) network module developed for Nemesis communication sub-system in the MPICH2 library, however, was not scalable in how it established connections: pairwise connections between all of an application's processes were established during the initialization of the application (the library call to MPI_Init), regardless of whether the connections were eventually needed or not. In this work, we have developed a new TCP network module for Nemesis that establishes connections on-demand. The on-demand connection establishment scheme is designed to improve the scalability of the TCP network module in MPICH2 library, aiming to reduce the initialization time and the use of operating system resources of MPI applications. Our performance benchmark results show that MPI_Init in the on-demand connection establishment scheme becomes a fast constant time operation, and the additional cost of establishing connections later is negligible. The on-demand connection establishment between two processes, especially when two processes attempt to connect to each other simultaneously, is a complex task due to race-conditions and thus prone to hard-to-reproduce defects. To assure ourselves of the correctness of the TCP network module, we modeled its design using the SPIN model checker, and verified safety and liveness properties stated as Linear Temporal Logic claims.

Malgré de nombreuses lacunes au niveau sécurité, les équipements sans-fil deviennent omniprésents: au travail, au café, à la maison, etc. Malheureusement, pour des raisons de convivialité, de simplicité ou par simple ignorance, ces équipements sont souvent configurés sans aucun service de sécurité, sinon un service minimal extrêmement vulnérable. Avec de telles configurations de base, plusieurs attaques sont facilement réalisables avec des moyens financiers négligeables et des connaissances techniques élémentaires. Les techniques de détection d'intrusions peuvent aider les administrateurs systèmes à détecter des comportements suspects et à prévenir les tentatives d'intrusions. Nous avons modifié et étendu un outil existant (Orchids), basé sur la vérification de modèles, pour détecter des intrusions dans les réseaux sans-fil. Les attaques sont décrites de façon déclarative, à l'aide de signatures en logique temporelle. Nous avons tout d'abord développé et intégré, dans Orchids, notre propre module spécialisé dans l'analyse des événements survenant sur un réseau sans-fil 802.11. Par la suite, nous avons décrit, à l'aide de signatures, un certain nombre d'attaques, notamment, ChopChop - à notre connaissance, nous somme les premiers à détecter cette attaque -, ARP Replay, et la deauthentication flooding. Ces attaques ont ensuite été mises en oeuvre, puis détectées avec succès dans un environnement réel (trois machines: client, pirate et détecteur d'intrusion, plus un point d'accès). ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Sécurité, Détection d'intrusions, Réseaux sans-fil, Vérification de modèles.

L'objectif de notre travail de recherche est de vérifier si un processus BPEL satisfait sa spécification d'interface représentant son comportement externe en utilisant la vérification de modèles. Dans ce mémoire, nous présentons essentiellement l'approche de notre logiciel qui permet dans un premier temps de traduire un processus BPEL en modèle Promela et une expression d'interface en assertion de traces, et par la suite, il lance la vérification en utilisant l'outil Spin. Cette vérification du comportement du processus concret se fait par rapport à une spécification abstraite de son interface comportementale, c'est-à-dire, nous vérifions uniquement ce qui est visible à l'exterieur du processus. Nous expliquons les étapes franchies pour atteindre notre objectif et nous montrons à l'aide d'exemples que notre logiciel est fonctionnel.

Many important software systems, including communication protocols and concurrent and distributed algorithms generate infinite state-spaces. Model-checking which is the most prominent algorithmic technique for the verification of concurrent systems is restricted to the analysis of finite-state models. Algorithmic analysis of infinite-state models is complicated--most interesting properties are undecidable for sufficiently expressive classes of infinite-state models. In this thesis, we focus on the development of algorithmic analysis techniques for two important classes of infinite-state models: FIFO Systems and Parameterized Systems. FIFO systems consisting of a set of finite-state machines that communicate via unbounded, perfect, FIFO channels arise naturally in the analysis of distributed protocols. We study the problem of computing the set of reachable states of a FIFO system composed of piecewise components. This problem is closely related to calculating the set of all possible channel contents, i.e. the limit language. We present new algorithms for calculating the limit language of a system with a single communication channel and important subclasses of multi-channel systems. We also discuss the complexity of these algorithms. Furthermore, we present a procedure that translates a piecewise FIFO system to an abridged structure, representing an expressive abstraction of the system. We show that we can analyze the infinite computations of the more concrete model by analyzing the computations of the finite, abridged model. Parameterized systems are a common model of computation for concurrent systems consisting of an arbitrary number of homogenous processes. We study the reachability problem in parameterized systems of infinite-state processes. We describe a framework that combines Abstract Interpretation with a backward-reachability algorithm. Our key idea is to create an abstract domain in which each element (a) represents the lower bound on the number of processes at a control location and (b) employs a numeric abstract domain to capture arithmetic relations among variables of the processes. We also provide an extrapolation operator for the domain to guarantee sound termination of the backward-reachability algorithm.

Many important software systems, including communication protocols and concurrent and distributed algorithms generate infinite state-spaces. Model-checking which is the most prominent algorithmic technique for the verification of concurrent systems is restricted to the analysis of finite-state models. Algorithmic analysis of infinite-state models is complicated--most interesting properties are undecidable for sufficiently expressive classes of infinite-state models. In this thesis, we focus on the development of algorithmic analysis techniques for two important classes of infinite-state models: FIFO Systems and Parameterized Systems. FIFO systems consisting of a set of finite-state machines that communicate via unbounded, perfect, FIFO channels arise naturally in the analysis of distributed protocols. We study the problem of computing the set of reachable states of a FIFO system composed of piecewise components. This problem is closely related to calculating the set of all possible channel contents, i.e. the limit language. We present new algorithms for calculating the limit language of a system with a single communication channel and important subclasses of multi-channel systems. We also discuss the complexity of these algorithms. Furthermore, we present a procedure that translates a piecewise FIFO system to an abridged structure, representing an expressive abstraction of the system. We show that we can analyze the infinite computations of the more concrete model by analyzing the computations of the finite, abridged model. Parameterized systems are a common model of computation for concurrent systems consisting of an arbitrary number of homogenous processes. We study the reachability problem in parameterized systems of infinite-state processes. We describe a framework that combines Abstract Interpretation with a backward-reachability algorithm. Our key idea is to create an abstract domain in which each element (a) represents the lower bound on the number of processes at a control location and (b) employs a numeric abstract domain to capture arithmetic relations among variables of the processes. We also provide an extrapolation operator for the domain to guarantee sound termination of the backward-reachability algorithm.

With the introduction of software into cars, many functions are now realized with reduced cost, weight and energy. The development of these software systems is done in a distributed manner independently by suppliers, following the traditional approach of the automotive industry, while the car maker takes care of the integration. However, the integration can lead to unexpected and unintended interactions among software systems, a phenomena regarded as feature interaction. This dissertation addresses the problem of the automatic detection of feature interactions for automotive active safety features. Active safety features control the vehicle's motion control systems independently from the driver's request, with the intention of increasing passengers' safety (e.g., by applying hard braking in the case of an identified imminent collision), but their unintended interactions could instead endanger the passengers (e.g., simultaneous throttle increase and sharp narrow steering, causing the vehicle to roll over). My method decomposes the problem into three parts: (I) creation of a definition of feature interactions based on the set of actuators and domain expert knowledge; (II) translation of automotive active safety features designed using a subset of Matlab's Stateflow into the input language of the model checker SMV; (III) analysis using model checking at design time to detect a representation of all feature interactions based on partitioning the counterexamples into equivalence classes. The key novel characteristic of my work is exploiting domain-specific information about the feature interaction problem and the structure of the model to produce a method that finds a representation of all different feature interactions for automotive active safety features at design time. My method is validated by a case study with the set of non-proprietary automotive feature design models I created. The method generates a set of counterexamples that represent the whole set of feature interactions in the case study.By showing only a set of representative feature interaction cases, the information is concise and useful for feature designers. Moreover, by generating these results from feature models designed in Matlab's Stateflow translated into SMV models, the feature designers can trace the counterexamples generated by SMV and understand the results in terms of the Stateflow model. I believe that my results and techniques will have relevance to the solution of the feature interaction problem in other cyber-physical systems, and have a direct impact in assessing the safety of automotive systems.