Les services Web sont des applications distribuées qui sont conçus pour atteindre une tâche spécifique de l'entreprise sur le web. Afin d'augmenter la qualité et d'élever la sécurité des services Web, la vérification de BPEL, un service web langage de composition est considérée. Dans ce contexte, le model checking est une des techniques de vérification les plus utilisés en raison de son exhaustivité, son application facile et automatique. Cependant, un inconvénient majeur du model checking est l'explosion combinatoire en cas de grands modèles. Le raffinement est une des techniques utilisées pour combattre au problème d'explosion. Dans cette thèse, nous étudions le raffinement des systèmes temporisés et son application à des situations réelles, à savoir les modèles BPEL. Pour cela, nous proposons d'abord une technique automatique pour la vérification de la simulation faible temporisée entre des systèmes de transitions temporisé basée sur des modèles issus d'un langage de spécification formelle, FIACRE. La technique est une méthode basée sur l'observation, dans laquelle deux systèmes de transitions temporisés sont composées avec un observateur temporisé. Une propriété de mu-calcul qui capte la simulation faible temporisée est ensuite vérifiée sur le résultat de la composition. En deuxième étape, afin de valider les modèles BPEL, nous proposons une technique qui consiste dans les étapes suivantes: premièrement, les activités BPEL qui ont besoin d'être abstrait sont fournis avec leurs abstractions. Deuxièmement, la source BPEL est transformé en FIACRE en fonction des choix précédents. Troisièmement, les propriétés d'exigences sont vérifiées sur le modèle de FIACRE abstrait. Enfin, les relations de simulation sont prouvés entre les composants concrets et abstraits du modèle.
展开▼
