- / -

Predicate abstraction is a key enabling technology for applying model checkers to programs written in mainstream languages. It has been used very successfully for debugging sequential system-level C code. Although model checking was originally designed for analysing concurrent systems, there is little evidence of fruitful applications of predicate abstraction to shared-variable concurrent software. The goal of the present thesis is to close this gap. We propose an algorithmic solution implementing predicate abstraction that targets safety properties in non-recursive programs executed by an unbounded number of threads, which communicate via shared memory or higher-level mechanisms, such as mutexes and broadcasts. As system-level code makes frequent use of such primitives, their correct usage is critical to ensure reliability. Monotonicity - the property that thread actions remain executable when other threads are added to the current global state - is a natural and common feature of human-written concurrent software. It is also useful: if every thread’s memory is finite, monotonicity often guarantees the decidability of safety properties even when the number of running threads is unspecified. In this thesis, we show that the process of obtaining finite-data thread abstrac tions for model checking is not always compatible with monotonicity. Predicate-abstracting certain mainstream asynchronous software such as the ticket busy-wait lock algorithm results in non-monotone multi-threaded Boolean programs, despite the monotonicity of the input program: the monotonicity is lost in the abstraction. As a result, the unbounded thread Boolean programs do not give rise to well quasi-ordered systems [1], for which sound and complete safety checking algorithms are available. In fact, safety checking turns out to be undecidable for the obtained class of abstract programs, despite the finiteness of the individual threads’ state spaces. Our solution is to restore the monotonicity in the abstract program, using an inexpensive closure operator that precisely preserves all safety properties from the (non-monotone) abstract program without the closure. As a second contribution, we present a novel, sound and complete, yet empirically much improved algorithm for verifying abstractions, applicable to general well quasi-ordered systems. Our approach is to gradually widen the set of safety queries during the search by program states that involve fewer threads and are thus easier to decide, and are likely to finalise the decision on earlier queries. To counter the negative impact of "bad guesses", i.e. program states that turn out feasible, the search is supported by a parallel engine that generates such states; these are never selected for widening. We present an implementation of our techniques and extensive experiments on multi-threaded C programs, including device driver code from FreeBSD and Solaris. The experiments demonstrate that by exploiting monotonicity, model checking techniques - enabled by predicate abstraction - scale to realistic programs even of a few thousands of multi-threaded C code lines.

Alors que l'informatique est devenue omniprésente dans notre société actuelle, assurer la qualité d'un logiciel revêt une importance grandissante. Pour accroître cette qualité, l'une des conditions à respecter est la correction du système. Dans cette thèse, nous nous intéressons plus particulièrement aux systèmes distribués mettant en œuvre un ou plusieurs programmes exécutés sur plusieurs machines qui communiquent entre elles à travers le réseau. Dans ce contexte, assurer leur correction est rendu plus difficile par leur hétérogénéité mais également par leurs spécificités communes. Les algorithmes correspondants sont parfois complexes et la prédiction de leur comportement difficilement réalisable sans une étude avancée. Les travaux réalisés au cours de cette thèse mettent en œuvre la vérification dynamique formelle de propriétés temporelles sur des applications distribuées. Cette approche consiste à vérifier l'implémentation réelle d'une application à travers son exécution. L'enjeu majeur est de réussir à appliquer les techniques associées au Model checking dans le cadre d'une vérification sur des implémentations réelles d'applications distribuées et non plus sur des modèles abstraits. Pour cela, nous proposons dans un premier temps une analyse sémantique dynamique par introspection mémoire d'un état système permettant de détecter des états sémantiquement identiques. Puis, nous mettons en œuvre la vérification dynamique formelle de certaines propriétés temporelles : les propriétés de vivacité, formulées à l'aide de la logique LTL_X, et le déterminisme des communications dans les applications MPI. Une évaluation de chacune de ces contributions est réalisée à travers plusieurs expériences / While computers have become ubiquitous in our current society, ensuring the software quality takes on an increasing importance. One of the requirements to enhance this quality is the system correctness. In this thesis, we are particularly interested in distributed systems implementing one or more programs executed on several machines which communicate with each other through a network. Ensuring the system correctness is more difficult in this context, due to their heterogeneity but also their common characteristics. Corresponding algorithms are sometimes complex and the prediction of their behavior may be difficult to realize without an advanced study. The work done during this thesis implement the dynamic formal verification of some temporal properties on legacy distributed applications. This approach consists of checking the real implementation of an application by its systematic execution. The challenge in this approach is how to apply the methods derived from Model checking in the context of the verification of legacy distributed applications (without access to source code) and no longer on abstract models. For that, we propose in a first step a dynamic semantic analysis of a system state permitting the detection of identical states. Then, we implement the dynamic formal verification of some temporal properties: liveness properties, specified with the LTL_X logic, and the communications determinism in MPI applications. These contributions are experimentaly validated and evaluated with different series of experiments

Software quality ensures that applications that are developed are failure free. Some modern systems are intricate, due to the complexity of their information processes. Software fault prediction is an important quality assurance activity, since it is a mechanism that correctly predicts the defect proneness of modules and classifies modules that saves resources, time and developers’ efforts. In this study, a model that selects relevant features that can be used in defect prediction was proposed. The literature was reviewed and it revealed that process metrics are better predictors of defects in version systems and are based on historic source code over time. These metrics are extracted from the source-code module and include, for example, the number of additions and deletions from the source code, the number of distinct committers and the number of modified lines. In this research, defect prediction was conducted using open source software (OSS) of software product line(s) (SPL), hence process metrics were chosen. Data sets that are used in defect prediction may contain non-significant and redundant attributes that may affect the accuracy of machine-learning algorithms. In order to improve the prediction accuracy of classification models, features that are significant in the defect prediction process are utilised. In machine learning, feature selection techniques are applied in the identification of the relevant data. Feature selection is a pre-processing step that helps to reduce the dimensionality of data in machine learning. Feature selection techniques include information theoretic methods that are based on the entropy concept. This study experimented the efficiency of the feature selection techniques. It was realised that software defect prediction using significant attributes improves the prediction accuracy. A novel MICFastCR model, which is based on the Maximal Information Coefficient (MIC) was developed to select significant attributes and Fast Correlation Based Filter (FCBF) to eliminate redundant attributes. Machine learning algorithms were then run to predict software defects. The MICFastCR achieved the highest prediction accuracy as reported by various performance measures. / School of Computing / Ph. D. (Computer Science)

The focus of the dissertation is on software quality assurance for object-oriented information systems development. A Quality Assurance Reference Model is proposed with aspects dealing with technical and managerial issues. A revised Spiral life cycle model is adopted as well as the Object Modelling Technique. The Quality Assurance Reference Model associates quality factors at various levels, quality criteria and metrics into a matrix framework that may be used to achieve quality assurance for all cycles of the Spiral Model. / Computing / M. Sc. (Information Systems)

The focus of the dissertation is on software quality assurance for object-oriented information systems development. A Quality Assurance Reference Model is proposed with aspects dealing with technical and managerial issues. A revised Spiral life cycle model is adopted as well as the Object Modelling Technique. The Quality Assurance Reference Model associates quality factors at various levels, quality criteria and metrics into a matrix framework that may be used to achieve quality assurance for all cycles of the Spiral Model. / Computing / M. Sc. (Information Systems)