Acronyme : «acronyme»

Répartition hebdomadaire ou semestrielle

(CM: 3h00)(TD/TME: 1h00)

Contenu Le but de cette UE est de présenter trois techniques complémentaires de vérification formelle de systèmes répartis : la vérification structurelle, le model-checking et le test. Chacune de ces techniques sera étudiée et ses avantages et inconvénients seront présentés.

Expérience du responsable dans le domaine de l’UE Recherches sur la vérification de systèmes répartis (réseaux de Petri, model-checking) depuis 1991. Enseignements dans le domaine depuis 1996 en DEA puis en Master.

Réalisations du responsable dans le domaine de l’UE F. Bréant, J.-M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. Paviot-Adet, D. Poitrenaud, D. Regep, G. Sutre : "Modeling and Verifying Behavioral Aspects", in Formal Methods for Embedded Distributed Systems - How to master the complexity, F. Kordon, M. Lemoine, Eds.: Kluwer Academic Publishers, pp. 171-211. C. Dutheillet, J.-M. Ilié, D. Poitrenaud, I. Vernier-Mounier : "State-Space-Based Methods and Model Checking", in Petri nets for Systems Engineering : A Guide to Modeling, Verification, and Applications, C. Girault, R. Valk, Eds.: Springer-Verlag, pp. 201-275. Y. Thierry-Mieg, C. Dutheillet, I. Mounier : "Automatic Symmetry Detection in Well-Formed Nets", 28th International Conference on Theory and Application of Petri Nets. I. Vernier, E. Paviot-Adet : "Modélisation et vérification de l'interopérabilité de services de télécommunication", in Vérification et mise en oeuvre de réseaux de Petri, M. Diaz, Ed. Paris: Hermès Science, pp. 233-252. M. Doche, I. Vernier-Mounier, F. Kordon : "Modular approach to specify and validate an Electrical Fligh Control System", Formal Method Europe (FME'2001), pp. 590-610.

Acronyme : vln	Spécialité : STL	3 ECTS	Niveau : 500	Semestre : S3
Titre : Validation des logiciels numériques
Responsable : Jean-Marie CHESNEAUX