Article

1 - PREUVE DE PROGRAMMES. PROCESSUS IDM

2 - LOGIQUE DE HOARE

3 - PROCESSUS IDM. DIAGRAMME D'ACTIVITÉ UML ET SAM

4 - CONCLUSION. PERSPECTIVES

Article de référence | Réf : H3882 v1

Validation des algorithmes en UML et OCL

Auteur(s) : Pierre BAZEX, Agusti CANALS

Date de publication : 10 août 2013

Pour explorer cet article
Télécharger l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !

Sommaire

Présentation

RÉSUMÉ

Cet article traite de propriétés formelles des langages de programmation dont le but est de vérifier, voire prouver, que les programmes fonctionnent correctement. Dans un contexte de processus centré sur les modèles (processus IDM), ces propriétés peuvent être appliquées à des langages de modélisation pour garantir la qualité attendue de la part des modèles, et la cohérence entre les modèles et les programmes. Mais ces techniques de preuve, basées sur la logique des prédicats, peuvent-elles s'appliquer à des langages métiers tels que le langage «Structured Analysis Model» (SAM) développé pour modéliser des applications du domaine de l'aéronautique ?

Lire cet article issu d'une ressource documentaire complète, actualisée et validée par des comités scientifiques.

Lire l’article

ABSTRACT

UML/OCL standard applied to algorithm validation

This article deals with the formal properties of programming languages whose purpose is to verify or even prove that the programs work correctly. Within an MDE process, these properties can be applied to modeling languages in order the quality expected from models and consistency between models and programs be guaranteed. However, can this technical evidence based on predicate logic be applied to modeling languages such as the "Structured Analysis Model “(SAM) developed in order to model applications in the field of aeronautics?

Auteur(s)

  • Pierre BAZEX : Professeur émérite de l'Université Paul Sabatier, Toulouse

  • Agusti CANALS : Directeur d'unité fonctionnelle (technique), CS Communication & Systèmes

INTRODUCTION

Placée en phase terminale d'un processus de développement IDM où les modèles représentent une certaine abstraction des exigences des applications à développer, la programmation est souvent considérée comme une simple activité de génération de codes issus des modèles.

Comment, dans ces conditions, peut-on prouver que tout programme fonctionne correctement et que les exigences des applications ont été bien prises en compte ?

Cette étude traite de propriétés formelles des langages de programmation dont le but est de raisonner sur des programmes pour chercher à vérifier et prouver qu'ils fonctionnent correctement. Le rajout de propriétés axiomatiques au niveau des langages de modélisation permet ainsi de vérifier que les modèles ont toutes les qualités que l'on peut en attendre de leur part. Les propriétés axiomatiques, appliquées dans le contexte d'un processus IDM vu comme une succession de transformations de modèles permettent donc de vérifier la cohérence de l'ensemble des modèles et des programmes.

Cette étude se situe dans la continuité de la sémantique opérationnelle des langages de programmation décrivant de manière précise et rigoureuse les aspects comportementaux de leurs constructions syntaxiques spécifiées à l'aide d'une grammaire. Elle prend donc toute son importance pour des applications ayant des exigences très critiques, telles qu'on en trouve aujourd'hui dans des domaines d'activités très variés, de l'aéronautique et de l'espace par exemple, ou pour des applications « grand public » de l'administration et de la banque devant gérer des masses de données personnelles et privées. La confiance que l'on doit accorder à ces logiciels est d'autant plus importante qu'ils doivent fonctionner comme des automates pour être réactifs en temps réel aux différents environnements qu'ils sont chargés de contrôler, de gérer et de superviser et pour être disponibles 24 h sur 24 aux sollicitations des usagers au travers de téléprocédures.

Après avoir rappelé comment on peut raisonner sur des programmes à l'aide de propriétés basées sur la logique (propriétés axiomatiques) pour vérifier et prouver qu'ils ont un fonctionnement correct, nous montrons ensuite comment on peut définir et appliquer de telles propriétés pour vérifier que les modèles situés en amont d'un processus de développement ont bien les qualités attendues. Comment, dès lors, appliquer de telles propriétés lors de la spécification des traitements d'un système ou d'un sous-système décrits à l'aide de langages de modélisation métier, tel que SAM dédié au développement d'applications de l'aéronautique ?

Peut-on contribuer à obtenir une meilleure continuité entre les modèles et les programmes d'un processus de développement en proposant d'appliquer les mêmes approches de raisonnement et de preuve basées sur la logique des prédicats ? C'est la question qui est en fait posée dans cet article.

Cet article est réservé aux abonnés.
Il vous reste 94% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

KEYWORDS

axiomatic properties   |   proof of programms   |   UML   |   MDE process   |   programming   |   modeling

DOI (Digital Object Identifier)

https://doi.org/10.51257/a-v1-h3882


Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes

(233 articles en ce moment)

Cette offre vous donne accès à :

Une base complète d’articles

Actualisée et enrichie d’articles validés par nos comités scientifiques

Des services

Un ensemble d'outils exclusifs en complément des ressources

Un Parcours Pratique

Opérationnel et didactique, pour garantir l'acquisition des compétences transverses

Doc & Quiz

Des articles interactifs avec des quiz, pour une lecture constructive

ABONNEZ-VOUS

Lecture en cours
Présentation

Cet article est réservé aux abonnés.
Il vous reste 95% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes

(233 articles en ce moment)

Cette offre vous donne accès à :

Une base complète d’articles

Actualisée et enrichie d’articles validés par nos comités scientifiques

Des services

Un ensemble d'outils exclusifs en complément des ressources

Un Parcours Pratique

Opérationnel et didactique, pour garantir l'acquisition des compétences transverses

Doc & Quiz

Des articles interactifs avec des quiz, pour une lecture constructive

ABONNEZ-VOUS

Sommaire
Sommaire

BIBLIOGRAPHIE

  • (1) - AHO (A.), SETHI (S.), ULLMAN (J.) -   Compilateurs. Principes, techniques et outils.  -  InterÉditions (1989).

  • (2) - AHO (A.), ULLMAN (J.) -   Concepts fondamentaux de l'informatique.  -  Dunod (1993).

  • (3) - BLANC (X.) -   MDA en action. Ingénierie logicielle guidée par les modèles.  -  Eyrolles (2005).

  • (4) - BLANC (X.) -   UML2 pour les développeurs.  -  Eyrolles (2006).

  • (5) - BOOCH (G.), RUMBAUGH (J.), JACOBSON (I.) -   Le guide de l'utilisateur de UML.  -  Eyrolles (2001).

  • (6) - CANALS (A.), GABEL (G.), GAUFILLET (P.) -   Les composants SAM et OCL « Checker » du projet TOPCASED.  -   

  • ...

Cet article est réservé aux abonnés.
Il vous reste 92% à découvrir.

Pour explorer cet article
Téléchargez l'extrait gratuit

Vous êtes déjà abonné ?Connectez-vous !


L'expertise technique et scientifique de référence

La plus importante ressource documentaire technique et scientifique en langue française, avec + de 1 200 auteurs et 100 conseillers scientifiques.
+ de 10 000 articles et 1 000 fiches pratiques opérationnelles, + de 800 articles nouveaux ou mis à jours chaque année.
De la conception au prototypage, jusqu'à l'industrialisation, la référence pour sécuriser le développement de vos projets industriels.

Cet article fait partie de l’offre

Technologies logicielles Architectures des systèmes

(233 articles en ce moment)

Cette offre vous donne accès à :

Une base complète d’articles

Actualisée et enrichie d’articles validés par nos comités scientifiques

Des services

Un ensemble d'outils exclusifs en complément des ressources

Un Parcours Pratique

Opérationnel et didactique, pour garantir l'acquisition des compétences transverses

Doc & Quiz

Des articles interactifs avec des quiz, pour une lecture constructive

ABONNEZ-VOUS