Brevet FR3039908A1 (20170210)
REVENDICATIONS1. Procédé pour la conception, à partir de modèles, d'un logiciel essentiel pour la sûreté, le procédé comportant : la réception (132) d'exigences de logiciel en langage naturel ; l'élaboration (133) d'un modèle de spécifications de logiciel dans un langage naturel structuré en mettant en oeuvre une modélisation sémantique (150) et/ou une modélisation graphique (152) des exigences de logiciel en langage naturel ; l'application d'une analyse formelle d'exigences au modèle de spécifications de logiciel ; l'élaboration d'un modèle de conception de logiciel reposant sur le modèle de spécifications ; l'application, au modèle de conception de logiciel, de cas de tests de robustesse et reposant sur les exigences créées automatiquement ; la réalisation d'une analyse formelle du modèle de conception de logiciel ; la création automatisée (136) d'un code source à l'aide du modèle de conception de logiciel ; la vérification de la couverture et du comportement du code source par l'application de cas de tests créés automatiquement (148) et d'une technologie d'analyse statique ; la compilation d'un code objet exécutable à partir du code source vérifié ; et la vérification de la couverture et du comportement du code objet exécutable par l'application des cas de tests créés automatiquement. 3039908 15\n<CLM>\1\tProcédé selon la revendication 1, comportant une unité de création automatisée de cas de tests et de procédures créant automatiquement les cas de tests à partir du modèle de spécifications de logiciel. 5\n<CLM>\1\tProcédé selon la revendication 1, comportant une unité de démonstration automatisée de théorèmes mettant en oeuvre des techniques de démonstration automatisée de théorèmes pour analyser et vérifier une cohérence et/ou une justesse et/ou une exhaustivité du modèle de spécification de logiciel. 10\n<CLM>\1\tProcédé selon la revendication 1, comportant, si un résultat de l'analyse du modèle de spécifications de logiciel n'est pas satisfaisant, l'ajustement du modèle de spécifications de logiciel afin de corriger toute incohérence avec les exigences de logiciel en langage naturel. 15\n<CLM>\1\tProcédé selon la revendication 4, comportant l'application de l'analyse d'exigences au module de spécifications de logiciel ajusté.\n<CLM>\1\tProcédé selon la revendication 1, comportant une unité de création automatisée de cas de tests de robustesse et reposant sur 20 des exigences, et de procédures créant automatiquement les cas de tests appliqués au modèle de conception de logiciel.\n<CLM>\1\tProcédé selon la revendication 1, comportant l'utilisation d'une technologie de contrôle de modèle afin de créer les cas de tests de robustesse et reposant sur des exigences appliqués au 25 modèle de conception de logiciel.\n<CLM>\1\tProcédé selon la revendication 1, comportant, si un résultat de l'analyse du modèle de conception de logiciel n'est pas satisfaisant, l'ajustement du modèle de conception de logiciel afin de corriger toute incohérence avec le modèle de spécifications de logiciel. 3039908 16\n<CLM>\1\tProcédé selon la revendication 8, comportant l'application des cas de tests au modèle de conception de logiciel ajusté.