Présentation

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

Preuve de programmes. Processus IDM
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 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.

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

1. Preuve de programmes. Processus IDM

Apprendre les langages de programmation est a priori évident et très facile quand on utilise des langages et des environnements de programmation de très haut niveau et tant qu'on en reste à développer et tester des programmes pour des applications relativement ponctuelles.

Dans ce paragraphe, on montre les raisons pour lesquelles concevoir et écrire des programmes en milieu industriel devient rapidement très difficile, voire impossible.

Programmer nécessite, en fait, l'implication de plusieurs équipes de spécialistes intervenant tout au long du processus de développement des logiciels et pour assurer la maintenance corrective et évolutive des applications. Des démarches ont été suggérées et proposées pour organiser et planifier l'implication de ces spécialistes dans le processus. Cependant, dans cet article, on s'intéresse aux techniques de preuves de programmes qui amènent les programmeurs à raisonner directement sur les codes pour vérifier et prouver qu'ils sont corrects. Ces techniques sont alors appliquées aux langages de modélisation pour raisonner sur les modèles et sur la cohérence entre les modèles et les programmes définis et créés au cours d'un processus de développement.

1.1 Spécifier, concevoir, implémenter...

Programmer ne se limite pas à transcrire, dans un langage de programmation aussi évolué soit-il, les spécifications issues des exigences d'une application à développer et à tester le bon fonctionnement des logiciels ainsi obtenus. Programmer, c'est faire appel à diverses activités très variées telles que spécifier, concevoir, implémenter, lire, comprendre, documenter, apprécier, critiquer, tester, qualifier, mettre au point, maintenir, adapter, optimiser, porter, améliorer les programmes...

HAUT DE PAGE

1.1.1 Processus de développement et démarche

Dans le cadre de l'Ingénierie Dirigée par les Modèles IDM, toutes les activités de la programmation sont regroupées autour des modèles qui sont au centre du développement logiciel vu donc comme une succession de transformations de modèles organisée méthodologiquement selon les entreprises, depuis la prise en compte des exigences des applications jusqu'à la génération...

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

Lecture en cours
Preuve de programmes. Processus IDM
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 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.

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