Conception formellement prouvée de postes d’enclenchement

interlockingenclenchement

La conception et la validation de systèmes de postes de manœuvres nécessitent de maîtriser la sécurité avec efficacité.

IXL Builder est la solution Systerel pour le design de postes d’enclenchement informatiques.

Cette solution met en œuvre un processus de conception et de déploiement certifiable basé sur une large utilisation des
méthodes formelles.

 

Systerel IXL builder aide à l’automatisation de la conception, l’évaluation de la sécurité et la validation fonctionnelle.

Processus

  1. Conception générique d’un poste d’enclenchement basée sur un paradigme objet autour des diagrammes de classes et de machines à états
  2. Instanciation du modèle à partir des données de configuration importées
  3. Évaluation formelle de la sécurité du modèle instancié
  4. Validation du modèle par une simulation hôte
  5. Génération et certification du code
  6. Rejeu de la validation avec l’équipement cible (Hardware in the loop)

Fonctionnalités

Conception

Conception générique

  • Modélisation générique d’un enclenchement basée sur un paradigme objet autour des diagrammes de classes et de machines à états
  • Export de la documentation du modèle

Études de déploiement

  • Import de données depuis des outils de préparation de données externes
  • Éditeur de plan de voie non sécuritaire permettant la définition de topologie de voie pour les tests

interlocking
UML State Machine modeling environment

Évaluation de la sécurité

  • Traduction des exigences de sécurité sous forme d’obligations de preuve portant sur des éléments de modélisation
  • Réalisation de la preuve de la conception
    • Analyse des contre exemples
    • Identification des défauts de conception vis-à-vis de la sécurité
    • Mise au point des obligations de preuves et contraintes d’environnement

 

enclenchement
Animating signaling rules

Validation fonctionnelle

  • Tests fonctionnels des designs instanciés sur machine hôte
  • Animation des diagrammes de machines d’états et des plans de voie
  • Export de scénarios de validation pour des tests de validation cible (Hardware In The Loop)
  • Export de la documentation de tests

Génération de code

  • Prise en compte des contraintes de codage exportées par des plateformes calculateur de sécurité via des mécanismes d’extensions
  • Génération de code

 

 

Avantages

Environnement  graphique intégré

  • Conception générique sous forme de machines à états à partir des exigences fonctionnelles et de sécurité.
  • Animation de contre-exemples sur les diagrammes instanciés
  • Visualisation des traces de simulation
  • Export de la documentation du modèle et des tests

Conception formelle assistée

  • Interprétation des contre-exemples
  • Identification des défauts de conception
  • Preuve formelle de la conception instanciée
  • Justifiable T2/T3 EN50128

Adaptabilité

  • Plugin d’import pour des formats spécifiques de données
  • Plugin de génération de code respectant les contraintes de la plate-forme d’exécution sécuritaire

Contactez-nous