D'une manière générale, la vérification de modèles (model-checking), basée sur des approches formelles pour définir des spécifications rigoureuses, a pour objectif de garantir que les modèles possèdent toutes les qualités que l'on exige d'eux surtout lorsqu'ils ont en charge de modéliser la fabrication de systèmes critiques ayant des composantes logicielles développées dans des secteurs comme les transports ferroviaires, l'avionique, les télécommunications ou l'énergie. 

Chaque modèle, plus ou moins abstrait, correspond à une vision partielle du logiciel, et généralement à des points de vue ou à des métiers différents. L'ingénierie dirigée par les modèles correspond à un nouveau paradigme dans lequel le code source n'est plus considéré comme un élément central, mais au contraire comme un élément dérivé à partir de la fusion et du " tissage " d'éléments de modélisation. L'intérêt suscité par cette nouvelle approche est très important, notamment suite à l'apparition de standards basés sur les architectures dirigées par les modèles tel que MDA (Model Driven Architecture). La transformation de modèles, un des aspects essentiels de l'ingénierie dirigée par les modèles, consiste à automatiser la transformation de modèles : il s'agit de transformer le code d'un langage en un autre, une modélisation graphique en un environnement de classes pour un langage à objets, ou encore un modèle de données en un autre modèle, tout en assurant que les propriétés des données sont conservées lors de la transformation.

Dans ce contexte, la vérification de modèles prend une nouvelle dimension puisqu'elle va s'intégrer dans le processus d'automatisation des transformations de modèles s'assurant ainsi qu'à chaque étape de transformation, les modèles intermédiaires obtenus ont les qualités requises.

Cette conférence a pour objectif de faire le point sur les méthodes et les techniques concernant la vérification de modèles. Des retours d'expérience sur des applications de systèmes critiques permettront de mieux montrer les évolutions des méthodes et des techniques concernant la vérification de modèles. Ce séminaire montrera la place de la vérification des modèles dans cette nouvelle approche des architectures dirigées par les modèles.


Organisée conjointement par CS, l'IRIT et le CNAM, la présente journée, qui se tiendra le jeudi 24 juin 2004 à Paris au Conservatoire National des Arts et Métiers, a le triple but :

     1- de faire le point sur les multiples aspects de ces techniques, leurs approches et leurs stratégies d'utilisation,
     2- de présenter un panorama de l'offre actuelle,
     3- d'en montrer les intérêts technique et économique au travers de la description d'applications.


Copyright (C) CNAM-CMSL 2004, Tous droits réservés.