| Summary: | Les réseaux logiciels (connus sous l'éppellation: Software Defined Networking, SDN), qui s'appuient sur le paradigme de séparation du plan de contrôle et du plan d'acheminement, ont fortement progressé ces dernières années pour permettre la programmabilité des réseaux et faciliter leur gestion. Reconnu aujourd'hui comme des architectures logicielles pilotées par des applications, offrant plus de programmabilité, de flexibilité et de simplification des infrastructures, les réseaux logiciels sont de plus en plus largement adoptés et graduellement déployés par l'ensemble des fournisseurs. Néanmoins, l'émergence de ce type d'architectures pose un ensemble de questions fondamentales sur la manière de garantir leur correct fonctionnement. L'architecture logicielle SDN est elle-même un système complexe à plusieurs composants vulnérable aux erreurs. Il est essentiel d'en assurer le bon fonctionnement avant déploiement et intégration dans les infrastructures.Dans la littérature, la manière de réaliser cette tâche n'a été étudiée de manière approfondie qu'à l'aide de vérification formelle. Les méthodes de tests s'appuyant sur des modèles n'ont guère retenu l'attention de la communauté scientifique bien que leur pertinence et l'efficacité des tests associés ont été largement demontrés dans le domaine du développement logiciel. La création d'approches de test efficaces et réutilisables basées sur des modèles nous semble une approche appropriée avant tout déploiement de réseaux virtuels et de leurs composants. Le problème abordé dans cette thèse concerne l'utilisation de modèles formels pour garantir un comportement fonctionnel correct des architectures SDN ainsi que de leurs composants. Des approches formelles, structurées et efficaces de génération de tests sont les principale contributions de la thèse. En outre, l'automatisation du processus de test est mis en relief car elle peut en réduire considérablement les efforts et le coût.La première contribution consiste en une méthode reposant sur l'énumération de graphes et qui vise le test fonctionnel des architectures SDN. En second lieu, une méthode basée sur un circuit logique est développée pour tester la fonctionnalité de transmission d'un commutateur SDN. Plus loin, cette dernière méthode est étendue pour tester une application d'un contrôleur SDN. De plus, une technique basée sur une machine à états finis étendus est introduite pour tester la communication commutateur-contrôleur.Comme la qualité d'une suite de tests est généralement mesurée par sa couverture de fautes, les méthodes de test proposées introduisent différents modèles de fautes et génèrent des suites de tests avec une couverture de fautes guarantie. === Having gained momentum from its concept of decoupling the traffic control from the underlying traffic transmission, Software Defined Networking (SDN) is a new networking paradigm that is progressing rapidly addressing some of the long-standing challenges in computer networks. Since they are valuable and crucial for networking, SDN architectures are subject to be widely deployed and are expected to have the greatest impact in the near future. The emergence of SDN architectures raises a set of fundamental questions about how to guarantee their correctness. Although their goal is to simplify the management of networks, the challenge is that the SDN software architecture itself is a complex and multi-component system which is failure-prone. Therefore, assuring the correct functional behaviour of such architectures and related SDN components is a task of paramount importance, yet, decidedly challenging.How to achieve this task, however, has only been intensively investigated using formal verification, with little attention paid to model based testing methods. Furthermore, the relevance of models and the efficiency of model based testing have been demonstrated for software engineering and particularly for network protocols. Thus, the creation of efficient and reusable model based testing approaches becomes an important stage before the deployment of virtual networks and related components. The problem addressed in this thesis relates to the use of formal models for guaranteeing the correct functional behaviour of SDN architectures and their corresponding components. Formal, and effective test generation approaches are in the primary focus of the thesis. In addition, automation of the test process is targeted as it can considerably cut the efforts and cost of testing.The main contributions of the thesis relate to model based techniques for deriving high quality test suites. Firstly, a method relying on graph enumeration is proposed for the functional testing of SDN architectures. Secondly, a method based on logic circuit is developed for testing the forwarding functionality of an SDN switch. Further on, the latter method is extended to test an application of an SDN controller. Additionally, a technique based on an extended finite state machine is introduced for testing the switch-to-controller communication. As the quality of a test suite is usually measured by its fault coverage, the proposed testing methods introduce different fault models and seek for test suites with guaranteed fault coverage that can be stated as sufficient conditions for a test suite completeness / exhaustiveness.
|
|---|
