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.