DSpace Collection:
http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/48
2024-03-28T13:25:21ZLa formalisation du graphe MDG dans l'assistant d'aide à la preuve COQ et la preuve de correction de ses algorithmes
http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/2133
Titre: La formalisation du graphe MDG dans l'assistant d'aide à la preuve COQ et la preuve de correction de ses algorithmes
Auteur(s): Iza, Lyla
Résumé: La vérification formelle des systèmes critiques est réalisée, en utilisant une de ces deux approches : les modèle checking ou les assistants d'aide à la preuve. Ces approches ont des inconvénients et des avantages complémentaires. La vérification par modèle checking est un ensemble destechniques de vérification automatique. Il s'agit de vérifier par l'usage algorithmes si un modèle donné, satisfait une propriété. Le critère le plus intéressant du modèle checking est sa possibilité de générer un contre exemple si la propriété n'est pas vérifiée. Cependant, le modèle checking est limité par le problème de l'explosion de nombre d'états, malgré toutes les améliorations apportées à cette approche. Les assistants d'aide à la preuve permettent la spécification formelle de programmes, leurs implémentations et leurs certifications par des preuves formelles. Ces assistants de preuves sont connus pour leurs capacités d'expression de structures de données illimitées, mais les méthodes inductives ne permettent pas de données de contre-exemple. En effet, la combinaison de ces deux approches permet de surmonter leurs limitations et augmente les possibilités de chacune d'elle. Notre approche consiste à créer un lien entre l'assistant d'aide à la preuve coq et le modèle checking utilisant les MDGs, ceci est fait par la formalisation du graph MDG dans coq et la preuve de correction de ses algorithmes
Description: 93 p. : ill. ; 30 cm2014-01-01T00:00:00ZLa géstion de la cohérence sémantique lors de l'évolution des modéles appliquée aux ADLs
http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/2103
Titre: La géstion de la cohérence sémantique lors de l'évolution des modéles appliquée aux ADLs
Auteur(s): Sami, Sihem
Résumé: Ce travail s'inscrit dans le domaine de l'évolution des modèles et la problématique liée à la gestion de l'évolution des modèles indépendamment de leurs Méta Modèle, en assurant leurs cohérences sémantiques. Les systèmes sont amenés à évoluer soit pour ajouter de nouvelles fonctionnalités, pour modifier les fonctionnalités existantes ou bien pour s'adapter aux nouveaux besoins technologiques. Ce qui implique un cout de maintenance et de développement très élevé. Afin de rendre l'évolution des systèmes moins complexe, il est nécessaire d'élever le niveau d'abstraction dans la spécification du système en utilisant le Modèle. Un modèle est une description et une spécification partielle d'un système, comme exemple les modèles relationnels, qui permettent de spécifier la structure des bases de données. Le modèle sert à expliquer un système, ainsi l'évolution de ce dernier implique celle du modèle. Cependant, la question qui se pose est: après une évolution, notre modèle est-il encore cohérentÀ. Notre principale problématique est liée à l'évolution statique et structurelle au niveau modèle. Proposer une solution automatique afin de gérer l'impact engendré par les changements, établir le lien entre le modèle de départ et le modèle d'arrivé et assurer une cohérence sémantique indépendamment de tout méta modèle. Un modèle nommé IMoSCM (Independent Model Sémantique Consistency Management) est proposé pour une gestion automatique de la cohérence sémantique indépendamment de tout méta modèle lors de l'évolution des modèles. Cette contribution est validée par une application développée en JAVA en utilisant ECLIPS. Une illustration est présentée au travers de deux ADL ACME et xADL
Description: 146 p. : ill. ; 30 cm2015-01-01T00:00:00ZFormalisation du système elambda
http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/2080
Titre: Formalisation du système elambda
Auteur(s): Brahimi, Farida
Résumé: Dans ce mémoire, on a définit un nouveau système Elambda qu'est une extension de lambda calcul classique par l'ajout de deux constantes P et À qui représentent respectivement l'implication et la quantification universelle. Le système obtenu est assez riche, dans le sens où les deux constantes introduites sont suffisantes pour exprimer et définir le reste des connecteurs et quantificateurs logiques. La consistance du système Elambda est garantie grâce à l'affection d'un nouvel attribut appelé " niveau du terme " ; qui nous a permet d'avoir une nouvelle définition de la substitution, où le terme (M [N/x]) est définit uniquement quand le niveau du terme " N " est inférieur ou égal à celui de " x ". Cette restriction nécessite une définition propre du mécanisme de réduction, appelé Ebeta_reduc, qui vérifié la propriété de Church-Rosser (la preuve du théorème de Church-Rosser est donnée en utilisant l'assistant de preuve Coq) et offre un moyen pour éviter le paradoxe de Curry
Description: Bibliogr. p. 100-102. Annexes2015-01-01T00:00:00ZUne machine abstraite pour le système XcB+ -calcul
http://dlibrary.univ-boumerdes.dz:8080/handle/123456789/920
Titre: Une machine abstraite pour le système XcB+ -calcul
Auteur(s): Korso, Lila
Description: 71 p. : ill. ; 30 cm2004-01-01T00:00:00Z