We consider a statistical theory as being invariant when the results of two statisticians' independent data analyses, based upon the same statistical theory and using effectively the same statistical ingredients, are the same. We discuss three aspects of invariant statistical theories. Both model checking and checking for prior-data conflict are assessments of single null hypothesis without any specific alternative hypothesis. Hence, we conduct these assessments using a measure of surprise based on a discrepancy statistic. For the discrete case, it is natural to use the probability of obtaining a data point that is less probable than the observed data. For the continuous case, the natural analog of this is not invariant under equivalent choices of discrepancies. A new method is developed to obtain an invariant assessment. This approach also allows several discrepancies to be combined into one discrepancy via a single P-value. Second, Bayesians developed many noninformative priors that are supposed to contain no information concerning the true parameter value. Any of these are data dependent or improper which can lead to a variety of difficulties. Gelman (2006) introduced the notion of the weak informativity as a comprimise between informative and noninformative priors without a precise definition. We give a precise definition of weak informativity using a measure of prior-data conflict that assesses whether or not a prior places its mass around the parameter values having relatively high likelihood. In particular, we say a prior Pi_2 is weakly informative relative to another prior Pi_1 whenever Pi_2 leads to fewer prior-data conflicts a priori than Pi_1. This leads to a precise quantitative measure of how much less informative a weakly informative prior is. In Bayesian data analysis, highest posterior density inference is a commonly used method. This approach is not invariant to the choice of dominating measure or reparametrizations. We explore properties of relative surprise inferences suggested by Evans (1997). Relative surprise inferences which compare the belief changes from a priori to a posteriori are invariant under reparametrizations. We mainly focus on the connection of relative surprise inferences to classical Bayesian decision theory as well as important optimalities.

We consider a statistical theory as being invariant when the results of two statisticians' independent data analyses, based upon the same statistical theory and using effectively the same statistical ingredients, are the same. We discuss three aspects of invariant statistical theories. Both model checking and checking for prior-data conflict are assessments of single null hypothesis without any specific alternative hypothesis. Hence, we conduct these assessments using a measure of surprise based on a discrepancy statistic. For the discrete case, it is natural to use the probability of obtaining a data point that is less probable than the observed data. For the continuous case, the natural analog of this is not invariant under equivalent choices of discrepancies. A new method is developed to obtain an invariant assessment. This approach also allows several discrepancies to be combined into one discrepancy via a single P-value. Second, Bayesians developed many noninformative priors that are supposed to contain no information concerning the true parameter value. Any of these are data dependent or improper which can lead to a variety of difficulties. Gelman (2006) introduced the notion of the weak informativity as a comprimise between informative and noninformative priors without a precise definition. We give a precise definition of weak informativity using a measure of prior-data conflict that assesses whether or not a prior places its mass around the parameter values having relatively high likelihood. In particular, we say a prior Pi_2 is weakly informative relative to another prior Pi_1 whenever Pi_2 leads to fewer prior-data conflicts a priori than Pi_1. This leads to a precise quantitative measure of how much less informative a weakly informative prior is. In Bayesian data analysis, highest posterior density inference is a commonly used method. This approach is not invariant to the choice of dominating measure or reparametrizations. We explore properties of relative surprise inferences suggested by Evans (1997). Relative surprise inferences which compare the belief changes from a priori to a posteriori are invariant under reparametrizations. We mainly focus on the connection of relative surprise inferences to classical Bayesian decision theory as well as important optimalities.

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.

Model checking is a formal verification technique which is widely used in different areas for automated verification and analysis. In this study, we applied a Model Checking method to a biological system. Firstly we constructed a single-cell, Boolean network model for the signaling pathways of apoptosis (programmed cell death) in lung cancers by combining the intrinsic and extrinsic Apoptosis pathways, p53 signaling pathway and p53 - DAP Kinase pathway in Lung cancers. We translated this model to the NuSMV input language. Then we converted known experimental results to CTL properties and checked the conformance of our model with respect to biological experimental results. We examined the dynamics of the apoptosis in lung cancer using NuSMV symbolic model checker and identified the relationship between apoptosis and lung cancer. Finally we generalized the whole process by introducing translation rules and CTL property patterns for biological queries so that model checking any signaling pathway can be automated.

<p>Model checking is a formal verification method where one tries to prove or disprove properties of a formal system. Typical systems one might want to prove properties within are network protocols and digital circuits. Typical properties to check for are safety (nothing bad ever happens) and liveness (something good eventually happens).</p><p>This thesis describes an implementation of a sound and complete model checker for Computation Tree Logic (CTL) using Constraint Logic Programming over Finite Domains (CLP(FD)). The implementation described uses tabled resolution to remember earlier computations, is parameterised by choices of computation strategies and can with slight modification support different constraint domains. Soundness under negation is maintained through a restricted form of constructive negation.</p><p>The computation process amounts to a fixpoint search, where a fixpoint is reached when no more extension operations has any effect. As results show, the choice of strategies does influence the efficiency of the computation. Soundness and completeness are of course independent of the choice of strategies. Strategies include how to choose the extension operation for the next step and whether to perform global or local rule instantiations, resulting in bottom-up or top-down computations respectively.</p>