FORMATION SUR L'OUTIL BART


MODALITÉS DE LA FORMATION BART


OBJECTIFS :

> Apprendre à raffiner automatiquement un modèle B en utilisant BART.

PERSONNES CONCERNÉES :

> Toute personne désirant produire efficacement des logiciels en utilisant la méthode formelle B.

PRÉ-REQUIS :

> Formation B Niveau 2
> Avoir fait la formation Niveau 3 est un plus.

ORGANISATION :

> 10 personnes au maximum par formation.
> La formation se déroule dans les locaux de CLEARSY à Aix ou à Paris (Sauf dispositions exceptionnelles).
> Contactez CLEARSY pour connaître les dates des prochaines formations.

DURÉE :

3 jours.

TARIFS :

Une réduction de 15% est accordée pour un groupe de 3 personnes au moins, du même organisme.

PROGRAMME


1 – RAPPEL DES PRINCIPES DU RAFFINEMENT

> Description des principes de l’activité de raffinement d’un modèle abstrait en un modèle concert :
– raffinement de données,
– raffinement de substitution.
> Comment et pourquoi l’automatisation de ces principes est-elle possible ?

2 – LES PRINCIPES DE L’OUTIL BART

> Comment raffiner un modèle abstrait : quels sont les pré-requis à un raffinement automatique, comment écrire des règles de raffinement :
– règles de raffinement de variables,
– règles de raffinement d’opération.
> Présentation des pièges à éviter lors du raffinement, comment obtenir des modèles efficaces tout en limitant l’effort de preuve ?

3 – UTILISATION DE L’INTERFACE GRAPHIQUE

> Description de l’interface et mise en œuvre sur des exemples.

4 – ORGANISATION PRATIQUE

> Plus des deux tiers de la formation se déroule sous la forme de Travaux Pratiques.