Modélisation et vérification formelle des performances des systèmes de réseau

The demand for faster performance, increased accessibility, mobility and securecommunications has driven significant advancements in Internet architectures, protocols and applications. Whether Internet usage relates to businesses or entertainment, its performance and security are two of the highest orders. Recent advances in modern technology and network innovations have driven the desire to move away from manual error-prone methods of testing network components and evolve from the ad-hoc tools and simulation based testing which are, traditionally, used in assessing the performance of networking components but fail to achieve high accuracy results and obtain trustworthy analysis.Despite the criticism that formal verification (FV) methods have been receivingand lack of appreciation, they have achieved undeniable results and made great contributions in this field and other mature fields. For this reason, we investigate a FV methodology for analyzing the performance aspect of networking systems. We rely on a model-based approach that is based on building a rich faithful stochastic model of a system, then apply statistical model checking to assess its performance against a specified requirement. We explain that the stochastic behavior of the model is captured by introducing probabilistic variables which are updated via probability distributions. The latter are, typically, obtained by collecting and analyzing measurements from the system’s execution using traditional statistical tests to select the best fit distribution (i.e., process of distribution fitting). Unfortunately, distribution fitting requires a good statistical background and familiarity with several distributions which is beyond the expertise of some analysts.As such, we developed a tool called DeepFit that combines traditional statisticaltests and deep learning to automate the distribution fitting task. DeepFit is thenintegrated into the workflow of our FV methodology for rigorous modeling andperformance assessment of networking systems.L'auteur n'a pas fourni de résumé en français.The demand for faster performance, increased accessibility, mobility and securecommunications has driven significant advancements in Internet architectures, protocols and applications. Whether Internet usage relates to businesses or entertainment, its performance and security are two of the highest orders. Recent advances in modern technology and network innovations have driven the desire to move away from manual error-prone methods of testing network components and evolve from the ad-hoc tools and simulation based testing which are, traditionally, used in assessing the performance of networking components but fail to achieve high accuracy results and obtain trustworthy analysis.Despite the criticism that formal verification (FV) methods have been receivingand lack of appreciation, they have achieved undeniable results and made great contributions in this field and other mature fields. For this reason, we investigate a FV methodology for analyzing the performance aspect of networking systems. We rely on a model-based approach that is based on building a rich faithful stochastic model of a system, then apply statistical model checking to assess its performance against a specified requirement. We explain that the stochastic behavior of the model is captured by introducing probabilistic variables which are updated via probability distributions. The latter are, typically, obtained by collecting and analyzing measurements from the system’s execution using traditional statistical tests to select the best fit distribution (i.e., process of distribution fitting). Unfortunately, distribution fitting requires a good statistical background and familiarity with several distributions which is beyond the expertise of some analysts.As such, we developed a tool called DeepFit that combines traditional statisticaltests and deep learning to automate the distribution fitting task. DeepFit is thenintegrated into the workflow of our FV methodology for rigorous modeling andperformance assessment of networking systems