Retour à la liste des ateliers
Retour à la thématique
Retour au programme
Retour à la liste des thématiques

Ludovic Apvrille - Télécom ParisTech

• Date : Juillet
• Heure : Mercredi matin
• Salle : P162

• Autre(s) Thématique(s) :

• Débutant, intermédiaire, Avancé

L'atelier est progressif et accessible à toute personne sachant utiliser un ordinateur et une interface graphique. Le public avancé trouvera son bonheur dans la modélisation de mécanismes de sécurité, et dans la preuve de propriétés de sécurité. Les débutants arriveront à simuler un premier modèle. Et les intermediaires, entre les deux

• Avoir des notions d'UML/SysML est un plus, mais ce n'est pas obligatoire

• Informaticien
• Nombre maximum de personne : 24 places assises

Vous savez concevoir des logiciels à peu près sûrs ? Mais vos logiciels sont-ils aussi sécurisés ? Ou vous ne savez même pas faire un logiciel sûr ? Ou alors, vous aimez bien dessiner des boites avec des traits entre les boites (modèle UML !) ? Alors, cet atelier est fait pour vous ?

Cet atelier vous apprendra à modéliser des logiciels à la fois sûrs et sécurisés, et à vérifier facilement qu'ils sont effectivement sûrs et sécurisés !

Vous ferez tout cela avec l'outil “TTool” et le langage “AVATAR” supporté par TTool. Avatar est construit autour de UML/SysML.

1. Dans un premier temps, j'expliciterai les différentes étapes méthodologiques associées à TTool/Avatar : exigences, analyse, conception logicielle, generation de code et prototypage virtuel
2. Dans un deuxième temps, je me focaliserai sur la conception logicielle : principales operateurs de modélisation, et preuve de propriété de sûreté de fonctionnement et de sécurité. Il n'y aura pas trop de slides rébarbatives : je ferai avant tout des démonstrations sur des exemples simples pour montrer cela.
3. Après, c'est vous qui travaillez : l'on commencera sur un petit modèle, et chacun pourra aller à son rythme pour l'enrichir. L'idée sera que vous puissiez tous avoir un modèle simulable. Les intermédiaires pourront faire de la preuve de sûreté de fonctionnement sur leur modèle. Et les experts auront un modèle qui contiendra des mécanismes de sécurité prouvés.

• OS : tout OS convient, tant qu'il supporte java 1.6 ou plus
• Logiciels: TTool. A télécharger depuis https://ttool.telecom-paristech.fr/ . Il faut avant tout installer TTool. Si vous voulez faire de la preuve, il vaut mieux aussi installer UPPAAL (preuve de sûreté) et ProVerif (preuve de sécurité). Le site Internet de TTool explique comment installer les deux. Je mettrai en ligne qq jours avant une archive qui contient tout les logiciels nécessaires pré-installés.
• Un site Interet sera disponible qq jours avant avec les slides
• Nbre de personnes maximum: 24 places assises. Je ne sais pas si les places debout sont autorisées ou non.

• ttool.telecom-paristech.fr

Si vous voulez préparer un peu avant, il faut aller voir la section “avatar” du site de TTool : http://ttool.telecom-paristech.fr/avatar.html