OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Vérifications d'exclusions mutuelles par analyse statique de modèles SysML.

Apvrille, Ludovic and Saqui-Sannes, Pierre de Vérifications d'exclusions mutuelles par analyse statique de modèles SysML. (2013) Revue Génie Logiciel, 105. 40-44. ISSN 0295-6322

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
376kB

Abstract

Le langage SysML couplé à des outils de vérification formelle permet d’analyser un modèle de systèmes temps réel pour détecter les erreurs de conception au plus tôt dans le cycle de vie. Dans cet esprit, l’outil TTool met en œuvre trois approches de vérification formelle complémentaires : la détection de comportements non désirés et de violation temporelles, la mise en évidence de failles de sécurité et la recherche d’invariants. Cet article insiste sur la troisième approche et expose les principes d’une analyse statique de modèles SysML ciblée sur la détection d’états ou d’événements en exclusion mutuelle. A partir des diagrammes de blocs et de machines à états du modèle SysML, TTool construit un réseau de Petri et sa matrice d’incidence, point de départ de la résolution d’un système d’équations et d’identification d’invariants. L’optimisation de l’algorithme de Farkas par des heuristiques et la remontée du réseau de Petri au modèle SysML font l’objet d’une attention particulière. L’exemple d’un four à micro-ondes montre que la recherche d’invariants par ce type d’analyse statique peut amener à détecter des problèmes de conception non identifiées par les méthodes de vérification que TTool proposait jusqu’alors. Ajoutons à ceci que TTool est un outil en accès libre qui implante entièrement la recherche d’invariants et d’éléments en exclusion mutuelle sans intervention d’aucun outil externe.

Item Type:Article
Audience (journal):National peer-reviewed journal
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
Other partners > Institut Eurécom (FRANCE)
Other partners > Telecom ParisTech (FRANCE)
Laboratory name:
Statistics:download
Deposited By: Pierre de Saqui-Sannes
Deposited On:16 Jul 2013 09:31

Repository Staff Only: item control page