Conception formellement prouvée de postes d’enclenchement
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
- Conception générique d’un poste d’enclenchement basée sur un paradigme objet autour des diagrammes de classes et de machines à états
- Instanciation du modèle à partir des données de configuration importées
- Évaluation formelle de la sécurité du modèle instancié
- Validation du modèle par une simulation hôte
- Génération et certification du code
- 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
É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
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