La méthode SCODE

Grâce à la méthode SCODE, qui est prise en charge et mise en œuvre par SCODE-ANALYZER, une vérification formelle dans l'outil permet d'afficher les erreurs de conception du système, qui peuvent être corrigées sans tarder. Les développeurs peuvent ainsi toujours travailler sur un système ayant été soumis à une vérification formelle. Les experts peuvent utiliser les résultats pour optimiser des logiciels existants ou en concevoir de nouveaux, et améliorer la testabilité.

Tous les résultats peuvent être ensuite traités par d’autres outils, sous diverses formes. Cela inclut la génération automatique de code programme.

La méthode SCODE

Espace de problème d'un frein électromécanique (exemple)

La méthode SCODE est un processus itératif à trois niveaux qui permet de représenter un système de manière simple et de l'analyser. L'objectif de la méthode est de décomposer un grand problème en plus petits problèmes pouvant être résolus indépendamment les uns des autres, afin de parvenir à résoudre le grand problème en résolvant les petits. SCODE-ANALYZER guide l'utilisateur tout au long du processus et l'assiste activement.

Etape 1 – Définition de l'espace de problème

La première étape consiste à définir l'espace de problème, en prenant en considération tous les aspects du système ou de l'environnement du système qui entraînent une modification au sein du système (par ex. interventions de l'utilisateur, résultats des mesures de capteurs). Les données de sortie sont constituées des modifications occasionnées dans le système (par ex. modification des variables ou signaux).

Etape 2 – Définition des modes

Définition du mode "Fermer l'étrier de frein" (exemple)

La deuxième étape porte sur la description des modes valides et des modes invalides du système. Un mode est défini par la combinaison des alternatives sélectionnées pour chaque dimension.

Règles d'entrée différentes avec des règles de sortie identiques

Des combinaisons différentes dans les dimensions d'entrée peuvent aboutir à des combinaisons identiques dans les dimensions de sortie, ce qui signifie que des données d'entrée différentes entraînent les mêmes modifications du système.

SCODE-ANALYZER fournit une aide en contrôlant que toutes les combinaisons ont bien été prises en compte, afin de ne pas laisser de côté des cas exceptionnels. Cela permet d'éviter de coûteuses surprises ultérieures, dues par exemple au fait que toutes les exigences n'avaient pas été définies. Le logiciel vérifie par ailleurs que chaque combinaison de l'espace de problème est affectée avec précision à un mode et qu'il n'y a pas de chevauchements au niveau de la définition des modes.

Etape 3

Tableau et représentation graphique des transitions entre les modes

La troisième étape vise à définir la façon dont le système doit réagir en matière de transitions entre les modes. A l'aide d'un tableau ou d'une interface graphique, les développeurs définissent quel événement déclenche le passage d'un mode à un autre. Il est également possible de définir que les transitions entre certains modes ne sont pas autorisées. Tout comme les modes, les événements définis font l'objet de contrôles portant sur l'intégrité, les blocages ainsi que d'autres caractéristiques.