Vérification dynamique formelle de propriétés temporelles sur des applications distribuées réelles

While computers have become ubiquitous in our current society,ensuring the software quality takes on an increasing importance. Oneof the requirements to enhance this quality is the system correctness.However, a compromise is often made between the quality and thedevelopment costs. Moreover, some of those systems may be crucial, asa failure may lead to important outcomes from a material, financial orhuman point of view. Consequently, the quality must prevail over theoptimization of the development costs.In this thesis, we are particularly interested in distributed systemsthrough a joint study of their performance and their correctness. Adistributed system implements one or more programs executed on severalmachines which communicate with each other through a network. Ensuringthe system correctness is more difficult in this context, due to theirheterogeneity but also their common characteristics. Correspondingalgorithms are sometimes complex and the prediction of their behaviormay be difficult to realize without an advanced study.We present the dynamic formal verification of some temporal propertieson typical distributed applications. It checks the real implementationof an application by its systematic execution. Based on Software ModelChekcking and Dynamic testing, the challenge in this approach is howto apply the methods derived from Model checking in the context of theverification of typical distributed applications and no longer onmodels. For that, we propose in a first step a dynamicsemantic analysis of a system state permitting the detection ofidentical states. Then, we implement the dynamic formal verificationof some properties specified with the temporal logicsLTL_X and CTL.Tandis que l'informatique est devenue omniprésente dans notre sociétéactuelle, assurer la qualité d'un logiciel revêt une importancegrandissante. Pour accroître cette qualité, l'une des conditions àrespecter est la correction du système. Toutefois, de par leur taille, leurcomplexité et leurs nombreux domaines d'applications, un compromisentre la qualité et le coup de développement des systèmes est souventréalisé. Cependant, certains systèmes peuvent se révéler critiques, ausens où leur défaillance peut avoir des conséquences dramatiques tantdu point de vue matériel, financier ou humain, dans certains cas. Dèslors, la qualité doit primer même si l'on souhaite contenir les coûtsde développement.Dans cette thèse, nous nous intéressons plus particulièrement auxsystèmes distribués à travers une étude conjointe de leursperformances et de leur correction. Un système distribué met en œuvreun ou plusieurs programmes exécutés sur plusieurs machines quicommuniquent entre elles à travers le réseau. Dans ce contexte,assurer leur correction est plus difficile, de par leurhétérogénéité mais également leurs spécificités communes. Lesalgorithmes correspondants sont parfois complexes et la prédiction deleur comportement difficile sans une étude avancée.Nous présentons la vérification dynamique formelle de propriétéstemporelles sur des applications distribuées réelles. Celle-ciconsiste à vérifier l'implémentation réelle d'une application àtravers son exécution. Basée sur les techniques du SoftwareModel Checking et de la Vérification Dynamique, l'enjeu danscette approche est d'appliquer les techniques associées auModel checking dans le cadre d'une vérification sur desimplémentations réelles d'applications distribuées et non plus sur desmodèles. Pour cela, nous proposons dans un premier tempsune analyse sémantique dynamique par introspection mémoire d'un étatsystème permettant de détecter des états sémantiquementidentiques. Puis, nous mettons en œuvre la vérification dynamiqueformelle de propriétés formulées à l'aide des logiques temporellesLTL_X et CTL