AVATAR/TTool : un environnement en mode libre pour SysML temps réel

Abstract

Cet article partage une expérience de modélisation de systèmes temps réel s’appuyant sur le langage AVA- TAR dérivé de SysML, l’outil en mode libre TTool et la méthode associée. AVATAR enrichit SysML par son lan- gage TEPE d’expression de propriétés. Sa sémantique formelle, par traduction vers les automates temporisés, autorise les preuves de sûreté et celle obtenue par traduction vers le pi-calcul rend possible les preuves de sécurité. Exé- cutable sur Linux, MacOS et Windows, l’outil en mode libre TTool mise quant à lui sur l’accessibilité aux non spé- cialistes pour offrir un éditeur de diagrammes, un simulateur de modèles, une interface aux outils de vérification formelle UPPAAL et ProVerif, et un générateur de code C Posix. L’article illustre l’approche AVATAR sur une étude de cas pédagogique et recense les projets académiques et industriels qui font appel à TTool.