This work deals with evaluating the effectiveness of a new verification algorithm called slice--n--dice. In order to evaluate the effectiveness of slice--n--dice, a vector clock POR was implemented to compare it against. The first paper contained in this work was published in ACM SIGSOFT Software Engineering Notes and discusses the implementation of the vector clock POR. The results of this paper show the vector clock POR performing better than the POR in Java Pathfinder by at least a factor of two. The second paper discusses the implementation of slice--n--dice and compares it against other verification techniques. The results show that slice--n--dice performs better than the other verification methods in terms of states explored and runtime when there is no error in the program or little thread interaction is needed in order for the error to manifest.

No description available.

No description available.

La simplification syntaxique, ou slicing, est une technique permettant d’extraire, à partir d’un programme et d’un critère consistant en une ou plusieurs instructions de ce programme, un programme plus simple, appelé slice, ayant le même comportement que le programme initial vis-à-vis de ce critère. Les méthodes d’analyse de code permettent d’établir les propriétés d’un programme. Ces méthodes sont souvent coûteuses, et leur complexité augmente rapidement avec la taille du code. Il serait donc souhaitable d’appliquer ces techniques sur des slices plutôt que sur le programme initial, mais cela nécessite de pouvoir justifier théoriquement l’interprétation des résultats obtenus sur les slices. Cette thèse apporte cette justification pour le cas de la recherche d’erreurs à l’exécution. Dans ce cadre, deux questions se posent. Si une erreur est détectée dans une slice, cela veut-il dire qu’elle se déclenchera aussi dans le programme initial ? Et inversement, si l’absence d’erreurs est prouvée dans une slice, cela veut-il dire que le programme initial en est lui aussi exempt ? Nous modélisons ce problème sur un mini-langage impératif représentatif, autorisant les erreurs et la non-terminaison, et montrons le lien entre la sémantique du programme initial et la sémantique de sa slice, ce qui nous permet de répondre aux deux questions précédentes. Pour généraliser ces résultats, nous nous intéressons à la première brique d’un slicer indépendant du langage : le calcul générique des dépendances de contrôle. Nous formalisons une théorie élégante de dépendances de contrôle sur des graphes orientés finis arbitraires prise dans la littérature et améliorons l’algorithme de calcul proposé.Pour garantir un maximum de confiance dans les résultats, tous ces travaux sont prouvés dans l’assistant de preuve Coq ou dans l’outil de preuve Why3. / Program slicing is a technique that extracts, given a program and a criterion that is one or several instructions in this program, a simpler program, called a slice, that has the same behavior as the initial program with respect to the criterion. Program analysis techniques focus on establishing the properties of a program. These techniques are costly, and their complexity increases with the size of the program. Therefore, it would be interesting to apply these techniques on slices rather than the initial program, but it requires theoretical foundations to interpret the results obtained on the slices. This thesis provides this justification for runtime error detection. In this context, two questions arise. If an error is detected in the slice, does this mean that it can also be triggered in the initial program? On the contrary, if the slice is proved to be error-free, does this mean that the initial program is error-free too? We model this problem using a small representative imperative language containing errors and non-termination, and establish the link between the semantics of the initial program and of its slice, which allows to give a precise answer to the two questions raised above. To apply these results in a more general context, we focus on the first step towards a language-independent slicer: an algorithm computing control dependence. We formalize an elegant theory of control dependence on arbitrary finite directed graphs taken from the literature and improve the proposed algorithm. To ensure a high confidence in the results, we prove them in the Coq proof assistant or in the Why3 proof plateform.

The concept of network slicing has been introduced in order to enable mobile networks to accommodate multiple heterogeneous use cases that are anticipated to be served within a single physical infrastructure. The slices are end-to-end virtual networks that share the resources of a physical network, spanning the core network (CN) and the radio access network (RAN). RAN slicing can be more challenging than CN slicing as the former deals with the distribution of radio resources, where the capacity is not constant over time and is hard to extend. The main challenge in RAN slicing is to simultaneously improve multiplexing gains while assuring enough isolation between slices, meaning one of the slices cannot negatively influence other slices. In this work, a flexible and configurable framework for RAN slicing is provided, where diverse requirements of slices are taken into account, and slice management algorithms adjust the control parameters of different radio resource management (RRM) mechanisms to satisfy the slices' service level agreements (SLAs). A new entity that translates the key performance indicator (KPI) targets of the SLAs to the control parameters is introduced and is called RAN slice orchestrator. Diverse algorithms governing this entity are introduced, which range from heuristics-based to model-free methods. Besides, a protection mechanism is constructed to prevent the negative influences of slices on each other's performances. The simulation-based analysis demonstrates the feasibility of slicing the RAN with multiplexing gains and slice isolation.

En raison de la complexité croissante des systèmes réactifs, le test est devenu un des éléments essentiels dans le processus de leur développement. Les tests de conformité avec des méthodes formelles concernent la correction du contrôle fonctionnel, par le biais des tests d'un système en boîte noire avec une spécification formelle du système. Les techniques passives de test sont utilisées lorsque l’exécution des systèmes testés ne peut pas être perturbée ou l'interface du système n'est pas fournie. Les techniques passives de test sont fondées sur l'observation et la vérification des propriétés du comportement d'un système sans interférer avec son fonctionnement normal. Les tests contribuent également à établir les comportements anormaux pendant l’exécution sur la base de l'observation de toute déviation d'un comportement prédéterminé. L'objectif principal de cette thèse est de présenter une nouvelle approche pour la mise en place des tests passifs fondés sur l'analyse des parties contrôle et données du système sous test. Au cours des dernières décennies, de nombreuses théories et outils ont été développés pour effectuer les tests de conformité. De fait, les spécifications ou les propriétés des systèmes réactifs sont souvent modélisés par différentes variantes de Labeled Transition Systems (LTS). Toutefois, ces méthodes ne prennent pas explicitement en compte les parties données du système, étant donné que le modèle sous-jacent de LTS n’est pas en mesure de le faire. Par conséquent, avec ces approches il est nécessaire d'énumérer les valeurs des données avant la modélisation du système. Cela conduit souvent au problème de l'explosion combinatoire de l'état-espace. Pour palier à cette limitation, nous avons étudié un modèle appelé Input-Output Symbolic Transition Systems (IOSTS) qui inclut explicitement toutes les données d'un système réactif. De nombreuses techniques de tests passives prennent uniquement en considération la partie du contrôle du système en négligeant les données, ou elles sont confrontées à une quantité énorme de données du processus. Dans notre approche, nous prenons en compte la partie contrôle et données en intégrant les concepts d'exécution symbolique et nous améliorons l'analyse de traces en introduisant des techniques de slicing des traces d’exécution. Les propriétés sont décrites à l'aide d'IOSTS et nous illustrons dans notre approche comment elles peuvent être testées sur l'exécution réelle des traces en optimisant l'analyse. Ces propriétés peuvent être conçues pour tester la conformité fonctionnelle d'un protocole ainsi que des propriétés de sécurité. Au-delà de l'approche théorique, nous avons développé un outil logiciel qui implémente les algorithmes présentés dans nos travaux. Enfin, comme preuve de concept de notre approche et de l'outil logiciel, nous avons appliqué les techniques à deux études de cas réels : le protocole SIP et le protocole Bluetooth / Due to the increasing complexity of reactive systems, testing has become an important part in the process of the development of such systems. Conformance testing with formal methods refers to checking functional correctness, by means of testing, of a black-box system under test with respect to a formal system specification, i.e., a specification given in a language with a formal semantics. In this aspect, passive testing techniques are used when the implementation under test cannot be disturbed or the system interface is not provided. Passive testing techniques are based on the observation and verification of properties on the behavior of a system without interfering with its normal operation, it also helps to observe abnormal behavior in the implementation under test on the basis of observing any deviation from the predefined behavior. The main objective of this thesis is to present a new approach to perform passive testing based on the analysis of the control and data part of the system under test. During the last decades, many theories and tools have been developed to perform conformance testing. However, in these theories, the specifications or properties of reactive systems are often modeled by different variants of Labeled Transition Systems (LTS). However, these methodologies do not explicitly take into account the system's data, since the underlying model of LTS are not able to do that. Hence, it is mandatory to enumerate the values of the data before modeling the system. This often results in the state-space explosion problem. To overcome this limitation, we have studied a model called Input-Output Symbolic Transition Systems (IOSTS) which explicitly includes all the data of a reactive system. Many passive testing techniques consider only the control part of the system and neglect data, or are confronted with an overwhelming amount of data values to process. In our approach, we consider control and data parts by integrating the concepts of symbolic execution and we improve trace analysis by introducing trace slicing techniques. Properties are described using Input Output Symbolic Transition Systems (IOSTSs) and we illustrate in our approach how they can be tested on real execution traces optimizing the trace analysis. These properties can be designed to test the functional conformance of a protocol as well as security properties. In addition to the theoretical approach, we have developed a software tool that implements the algorithms presented in this paper. Finally, as a proof of concept of our approach and tool we have applied the techniques to two real-life case studies: the SIP and Bluetooth protocol

To solve the bottleneck problem of resource utilization and user experience quality in mobile communication networks, 5G introduces network slicing to cope with the huge resource demand of users. To further improve the quality of service for users with different needs, a new fairness definition based on service level objective is introduced. On this basis, a network slicing dynamic resource scheduling strategy based on the greedy algorithm is designed, and the actual application scenarios of slicing scheduling and user scheduling are simplified into a two-layer model, namely the slicing-user model, and combined with the greedy algorithm to make the service weight value. Combine the largest slice and the user with the highest priority, and complete the matching service. The advantage of this method is various system resources can be fairly allocated according to the same proportion to users. Through the optimal combination of each slice and user, the resources of the entire system can be fairly allocated to users with different needs. Python simulation results showed that the newly proposed network slicing dynamic resource scheduling mechanism based on the greedy algorithm can meet the different needs of users and achieve short term fairness, where the users get a fair share of the resource by each missing their SLO by a similar percentage, so as to better meet the needs of users. / För att lösa flaskhalsproblemet med resursanvändning och användarupplevelsekvalitet i mobilkommunikationsnät introducerar 5G nätverksskivning för att klara användarnas enorma resursbehov. För att ytterligare förbättra servicekvaliteten för användare med olika behov införs en ny rättvisedefinition baserad på servicenivåmål. På grundval av detta utformas en dynamisk resursplaneringsstrategi för nätverksskivning baserad på den giriga algoritmen, och de faktiska applikationsscenarierna för skivningsplanering och användarschemaläggning förenklas till en tvåskiktsmodell, nämligen skivningsanvändarmodellen, och kombineras med girig algoritm för att göra tjänstens viktvärde. Kombinera den största delen och användaren med högsta prioritet och slutför motsvarande tjänst. Fördelen med denna metod är att olika systemresurser kan fördelas rättvist enligt samma andel, och genom den bästa kombinationen av varje segment och användare kan hela systemets resurser fördelas rättvist till användare med olika behov. Pythons simuleringsresultat visar att den nyligen föreslagna nätverksskärningsdynamiska resursplaneringsmekanismen baserad på den giriga algoritmen kan tillgodose användarnas olika behov och uppnå kortsiktig rättvisa där användarna får en rättvis andel av resursen genom att var och en saknar sin SLO med en liknande procentsats , för att bättre möta användarnas behov.

Matter on a length scale comparable to that of a chemical bond is governed by the theory of quantum mechanics, but quantum mechanics is a many body theory, hence for the sake of chemistry or solid state physics, finding solutions to the governing equation, Schrodinger's equation, is hopeless for all but the smallest of systems. As the number of electrons increases, the complexity of solving the equations grows rapidly without bound. One way to make progress is to treat the electrons in a system as independent particles and to attempt to capture the many-body effects in a functional of the electrons' density distribution. When this approximation is made, the resulting equation is called the Kohn-Sham equation, and instead of requiring solving for one function of many variables, it requires solving for many functions of the three spatial variables. This problem turns out to be easier than the many body problem, but it still scales cubically in the number of electrons. In this work we will explore ways of obtaining the solutions to the Kohn-Sham equation in the framework of real-space pseudopotential density functional theory. The Kohn-Sham equation itself is an eigenvalue problem, just as Schrodinger's equation. For each electron in the system, there is a corresponding eigenvector. So the task of solving the equation is to compute many eigenpairs of a large Hermitian matrix. In order to mitigate the problem of cubic scaling, we develop an algorithm to slice the spectrum into disjoint segments. This allows a smaller eigenproblem to be solved in each segment where a post-processing step combines the results from each segment and prevents double counting of the eigenpairs. The efficacy of this method depends on the use of high order polynomial filters that enhance only a segment of the spectrum. The order of the filter is the number of matrix-vector multiplication operations that must be done with the Hamiltonian. Therefore the performance of these operations is critical. We develop a scalable algorithm for computing these multiplications and introduce a new density functional theory code implementing the algorithm. / text

The Real-Time Specification for Java (RTSJ) introduces a new memory management model which avoids interfering with the garbage collection process and achieves better deterministic behaviour. In addition to the heap memory, two types of memory areas are provided - immortal and scoped. The research presented in this Thesis aims to optimize the use of the scoped and immortal memory model in RTSJ applications. Firstly, it provides an empirical study of the impact of scoped memory on execution time and memory consumption with different data objects allocated in scoped memory areas. It highlights different characteristics for the scoped memory model related to one of the RTSJ implementations (SUN RTS 2.2). Secondly, a new RTSJ case study which integrates scoped and immortal memory techniques to apply different memory models is presented. A simulation tool for a real-time Java application is developed which is the first in the literature that shows scoped memory and immortal memory consumption of an RTSJ application over a period of time. The simulation tool helps developers to choose the most appropriate scoped memory model by monitoring memory consumption and application execution time. The simulation demonstrates that a developer is able to compare and choose the most appropriate scoped memory design model that achieves the least memory footprint. Results showed that the memory design model with a higher number of scopes achieved the least memory footprint. However, the number of scopes per se does not always indicate a satisfactory memory footprint; choosing the right objects/threads to be allocated into scopes is an important factor to be considered. Recommendations and guidelines for developing RTSJ applications which use a scoped memory model are also provided. Finally, monitoring scoped and immortal memory at runtime may help in catching possible memory leaks. The case study with the simulation tool developed showed a space overhead incurred by immortal memory. In this research, dynamic code slicing is also employed as a debugging technique to explore constant increases in immortal memory. Two programming design patterns are presented for decreasing immortal memory overheads generated by specific data structures. Experimental results showed a significant decrease in immortal memory consumption at runtime.

<div>Modern Java application frameworks present significant challenges for existing static analysis algorithms. Such challenges include large-scale code bases, heap-carried dependency, and asynchronous control flow caused by message passing.</div><div>Existing analysis algorithms are not suitable to deal with these challenges. One reason is that analyses are typically designed to operate homogeneously on the whole program. This leads to scalability problems when the analysis algorithms are used on applications built as plug-ins of large frameworks, since the framework code is analyzed together with the application code. Moreover, the asynchronous message passing of the actor model adopted by most modern frameworks leads to control flows which are not modeled by existing analyses.</div><div>This thesis presents several techniques for more powerful debugging and program understanding tools based on slicing. In general, slicing-based techniques aim to discover interesting properties of a large program by only reasoning about the relevant part of the program (typically a small amount of code) precisely, abstracting away the behavior of the rest of the program.</div><div>The key contribution of this thesis is a demand-driven framework to enable precise and scalable analyses on programs built on large frameworks. A slicing algorithm, which can handle heap-carried dependence, is used to identify the program elements relevant to an analysis query. We instantiated the framework to infer correlations between registration call sites and callback methods, and resolve asynchronous control flows caused by asynchronous message passing.</div>