Vérification Formelle Des Diagrammes D'activité Sysml
Résumé: SysML (System Modeling Language) est un langage graphique largement répandu pour la spécification des systèmes complexes. Cependant, ce langage est semi-formel et sa sémantique n’est pas formellement définie. Par conséquent, il n’est pas possible de vérifier de manière exhaustive les spécifications du SysML. L’objectif de ce projet est de proposer une approche de vérification formelle d’une partie de la vue dynamique du langage SysML, à savoir, les diagrammes d’activités (SysML-AD). Afin de réaliser cet objectif, nous avons passé du langage SysML à des spécifications formelles en se basant sur une extension des réseaux de Petri, appelée RECATNet. Cette extension est très connue par son pouvoir d’expression, sa sémantique, et le fait qu’elle peut être définie facilement en termes de la logique de réécriture. Cette dernière permet d’utiliser le système Maude lors des phases d’analyse et de vérification. Pour implémenter ce projet, nous avons développé un outil JAVA permettant de vérifier les propriétés fonctionnelles, décrites par les diagrammes d'exigences, sur des diagrammes d’activités SysML.
Mots-clès:
Nos services universitaires et académiques
Thèses-Algérie vous propose ses divers services d’édition: mise en page, révision, correction, traduction, analyse du plagiat, ainsi que la réalisation des supports graphiques et de présentation (Slideshows).
Obtenez dès à présent et en toute facilité votre devis gratuit et une estimation de la durée de réalisation et bénéficiez d'une qualité de travail irréprochable et d'un temps de livraison imbattable!
Aucun fichier associé
Si le fichier est volumineux, l'affichage peut échouer. Vous pouvez obtenir le fichier directement en cliquant sur le bouton "Télécharger".
