Model Checking et systèmes complexes

Model Checking et systèmes complexes, quelques réussites, par Fabrice Kordon, LIP6/MoVe, Université Pierre & Marie CurieDans cet exposé, nous présenterons, au travers de quelques études de cas menées ces dernières années (vérification d’un middleware, vérification d’algorithmes dans une base de données répartie, vérification d’un protocole de certification dans un DTH, vérification d’un body area network), un aperçu des techniques de vérification par Model Checking développées au LIP6. Ces techniques sont intégrées dans une plate-forme logicielle libre, développée conjointement avec le LSV et le LIPN : CosyVerif.