Document ID: /fineweb-2-swissfilter-quality_10-filterrobots/filtered/06914.jsonl.gz/375

Résumé développement basé sur modèle, les propriétés de qualité tels que la cohérence des exigences de sécurité sont souvent vérifiés avant la génération de code. Modèles modifiés doivent être re-vérifié avant de re-génération. Si plusieurs évolutions possibles d’un modèle sont possibles, chaque solution doit être modélisé et vérifié pour trouver le meilleur modèle pour le développement ultérieur.
Nous présentons une stratégie de vérification pour analyser si l’évolution préserve les propriétés de sécurité donnés. Le profil de UMLchange est utilisé pour spécifier les évolutions potentielles d’un modèle donné simultanément. Nous présentons un outil qui lit ces annotations et calcule un delta contenant tous les chemins d’évolution possibles. Les chemins peuvent être vérifiées WRT. propriétés de sécurité, et pour chaque trajet vérifié avec succès une nouvelle version du modèle est généré automatiquement …. Faits saillants Nous présentons une démarche de vérification de la sécurité qui peut faire face à l’évolution des logiciels.
Il comprend des outils pour analyser si l’évolution préserve une propriété de sécurité.L’outil peut calculer toutes les voies d’évolution possibles du modèle donné.Nous présentons également le profil UML UMLchange utilisé pour spécifier les évolutions potentielles. UMLchange rend notre approche indépendante des outils de modélisation spécifiques.