Dynamic formal verification of temporal properties on legacy distributed applications
Vérification dynamique formelle de propriétés temporelles sur des applications distribuées réelles
Résumé
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.
However, a compromise is often made between the quality and the
development costs. Moreover, some of those systems may be crucial, as
a failure may lead to important outcomes from a material, financial or
human point of view. Consequently, the quality must prevail over the
optimization of the development costs.
In this thesis, we are particularly interested in distributed systems
through a joint study of their performance and their correctness. A
distributed system implements 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.
We present the dynamic formal verification of some temporal properties
on typical distributed applications. It checks the real implementation
of an application by its systematic execution. Based on Software Model
Chekcking and Dynamic testing, the challenge in this approach is how
to apply the methods derived from Model checking in the context of the
verification of typical distributed applications and no longer on
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 properties specified with the temporal logics
LTL_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 importance
grandissante. Pour accroître cette qualité, l'une des conditions à
respecter est la correction du système. Toutefois, de par leur taille, leur
complexité et leurs nombreux domaines d'applications, un compromis
entre la qualité et le coup de développement des systèmes est souvent
réalisé. Cependant, certains systèmes peuvent se révéler critiques, au
sens où leur défaillance peut avoir des conséquences dramatiques tant
du point de vue matériel, financier ou humain, dans certains cas. Dès
lors, la qualité doit primer même si l'on souhaite contenir les coûts
de développement.
Dans cette thèse, nous nous intéressons plus particulièrement aux
systèmes distribués à travers une étude conjointe de leurs
performances et de leur correction. Un système distribué met 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 plus difficile, de par leur
hétérogénéité mais également leurs spécificités communes. Les
algorithmes correspondants sont parfois complexes et la prédiction de
leur comportement difficile sans une étude avancée.
Nous présentons la vérification dynamique formelle de propriétés
temporelles sur des applications distribuées réelles. Celle-ci
consiste à vérifier l'implémentation réelle d'une application à
travers son exécution. Basée sur les techniques du Software
Model Checking et de la Vérification Dynamique, l'enjeu dans
cette approche est d'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. 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 propriétés formulées à l'aide des logiques temporelles
LTL_X et CTL.
Fichier principal
manuscrit.pdf (871.09 Ko)
Télécharger le fichier
annexe-soutenance.pdf (2.82 Mo)
Télécharger le fichier