Sémantique Formelle Pour Un Modèle Objet/relationnel: Cas D’étude De Vérification D’un Système À Base De Profil Uml

Résumé: Les systèmes informatiques sont présents au cœur de domaines variés, de l’industrie, des entreprises, des métiers et des produits. Ils sont caractérisés par des structures de données complexes manipulées via des traitements impliquant des volumes de données importants. Ceci augmente, de plus en plus, la complexité et le risque d’erreurs et les rendent critiques face aux exigences de fiabilité et de sécurité. Devant cette situation, les méthodes formelles sont employées afin de décrire précisément les structures des systèmes et leurs comportements, et de les vérifier à la base de ces descriptions. Les méthodes formelles, combinant des techniques de modélisation et d'analyse, visent ainsi à la spécification et la vérification des systèmes. Une spécification formelle permet de définir les caractéristiques souhaitées et le comportement attendu d'un système. Cette spécification peut servir de directives pour la conception, et dans certains cas, pour l’implémentation, résultante d’une génération automatique de code. Une vérification formelle vise à garantir que ces caractéristiques sont préservées à travers des comportements différents. Dans les systèmes critiques et réactifs, des méthodes d’analyses sont utilisées pour vérifier des propriétés et des exigences sur des logiciels embarqués. La technique du “model checking” est très répandu pour modéliser et vérifier leur comportement dynamique. Par ailleurs, avec la croissance des SGBDs actuels, en taille et fonctionnalités, des énormes masses de données sont manipulées. Ces données sont de plus en plus couteuses en termes d’exactitude et de cohérence. Des méthodes formelles sont utilisées pour vérifier ces propriétés. Une approche très prometteuse consiste en l’utilisation des assistants de preuve. La théorie relationnelle a fait ses preuves dans les applications de bases de données. Or, elle est limitée pour l’exploitation des données complexes, ce qui justifie son extension par des concepts objets. Ainsi, les orientations principales du modèle dit objet/relationnel sont le renforcement de typage et la construction des SGBDs ayant la capacité de manipuler des objets complexes. Nous proposons une base théorique pour l’intégration des concepts objets dans le contexte relationnel dans le cadre d’une théorie types. L’assistant de preuve Coq est utilisé pour la spécification du modèle de données en vue d’une vérification formelle des propriétés sur ce dernier. Le travail réalisé est une ébauche vers une utilisation plus large des méthodes formelles dans le processus de développement des systèmes de gestion de bases de données dits vérifiés. La croissance des systèmes embarqués les rend de plus en plus vulnérables à la moindre erreur. Malgré l’efficacité des techniques d’analyse de modèles « model-checking » dans ce domaine, leur utilisation en industrie demeure limitée. La cause principale est, d’une part, la complexité des modèles manipulés et d’autre part, la difficulté de construire des représentations formelles exploitables sur les outils de vérification existants. Nos travaux contribuent au développement d’un volet méthodologique définissant les activités conduisant à l’obtention des artefacts formels générés à partir des exigences informelles. Nous s’appuyions sur la modélisation des scénarios sous forme de contextes spécifiés dans un DSL. L’approche OBP/CDL est au cœur de ces travaux dont l’objectif est d’assister les ingénieurs de spécifications dans leurs missions et ainsi améliorer le processus de la vérification formelle.

Publié dans la revue: