Gagner en productivité sans compromettre la sécurité
Garantir la sécurité des Postes d’enclenchement et des Postes d’Aiguillage Informatiques (PAI) implique des campagnes de tests longues et coûteuses qui deviennent incompatibles avec les objectifs de réduction de coût et de délai qui portent sur le développement et le déploiement de tels systèmes.
Toute amélioration potentielle du processus et des outils associés est donc à saisir, dès lors que le niveau de sécurité des postes n’est pas remis en cause.
Consciente de la situation, Systerel développe depuis une dizaine d’années sa propre gamme d'outils dédiés à la modélisation et la vérification formelle de systèmes de signalisation, en particulier les postes à enclenchements ou Interlocking.
Systerel Smart Solver, qui en est le pivot, permet de déployer une solution complète de preuve automatisée depuis la fourniture des données d’un poste (principes et instanciation) jusqu’à la production de la preuve de sa sécurité ou d’un ensemble de contre-exemples pour les propriétés réfutées.
L’architecture de la solution proposée apporte toutes les garanties nécessaires à l’obtention d’un niveau SIL4 au sens de la norme EN50128:2011, classiquement visé pour ce type de développement.
Basées sur la logique mathématique, les méthodes formelles constituent un moyen efficace de démontrer le respect des propriétés de sécurité :
- Confiance accrue par l’exploration exhaustive des états d’un système
-Traitement accéléré de la démonstration de sécurité, des évolutions de paramétrage ou du fonctionnel
Systerel Smart Solver est une solution de preuve performante. Elle permet d’accroître la confiance dans le niveau de sécurité d’un système tout en réduisant considérablement le temps et le coût de validation associés.
Les différentes mesures réalisées sur des projets de taille industrielle montrent des gains en performance significatifs sur la validation de propriétés de sécurité : des activités de validation qui demandaient plusieurs mois auparavant se font désormais en quelques heures.
L’application à une échelle industrielle de Systerel Smart Solver par de grands acteurs du ferroviaire (Hitachi, Alstom, RATP, SNCF…), et la démonstration, sur des cas représentatifs, de sa capacité à adresser la grande majorité du parc des postes actuellement déployés par la SNCF par exemple, confirment la maturité de mise en œuvre de la vérification formelle pour le développement et le déploiement de systèmes d’enclenchement opérationnels.