B MODEL ANIMATION FOR EXTERNAL VERIFICATION
WAESELYNCK ; BEHNIA
Type de document
COMMUNICATION ORALE SANS ACTES (COM)
Langue
anglais
Auteur
WAESELYNCK ; BEHNIA
Résumé / Abstract
LA METHODE FORMELLE B EST UNE APPROCHE ORIENTEE-MODELE QUI COUVRE TOUT LE PROCESSUS DE DEVELOPPEMENT DU LOGICIEL, DE LA SPECIFICATION JUSQU'A LA GENERATION DU CODE. LA VERIFICATION EXTERNE DES MODELES B VISE A DETERMINER SI CEUX-CI EXPRIMENT CORRECTEMENT LES BESOINS INFORMELS DE L'UTILISATEUR. NOUS PROPOSONS D'UTILISER DES TECHNIQUES TELLES QUE L'ANIMATION DE MODELES B OU LE TEST DU CODE, AFIN DE PERMETTRE DES RETOURS SUR LE SYSTEME EN COURS DE DEVELOPPEMENT FORMEL. NOUS PRESENTONS UN CADRE UNIFIE DE TEST, QUI EST INDEPENDANT DU FAIT QUE LES DONNEES D'ENTREES SOIENT EXECUTEES SUR LE CODE FINAL OU SUR LE MODELE FORMEL. LE PROCESSUS DE DEVELOPPEMENT EN B EST CONSIDERE COMME UNE SERIE D'ETAPES DURANT LESQUELLES DES MODELES DE PLUS EN PLUS CONCRETS SONT CONSTRUITS A PARTIR DES MODELES ABSTRAITS, LE CODE FINAL ETANT VU COMME UNE VERSION COMPILEE DU MODELE LE PLUS CONCRET. LA CORRECTION DU TEST EST DEFINIE EN RELATION AVEC LA NOTION DE RAFFINEMENT. ENFIN, NOUS DISCUTONS DES BESOINS REQUIS PAR CE CADRE UNIFIE EN TERME D'OUTILS D'ANIMATION.
