Systerel a utilisé la méthode formelle B et l’Atelier B pour le développement de sa solution open-source Safe and Secure Open Platform Communications (S2OPC), pour les communications OPC UA.
L’OPC UA est un standard supervisant l’interopérabilité et l’échange de données pour les communications industrielles. Elle fournit des moyens sûrs et sécurisés pour connecter des systèmes de supervision (SCADA), des automates programmables (PLC), avec des actionneurs et des systèmes de terrain. Il est particulièrement dédié à l’Internet industriel des objets (IOT).
Ce développement intègre la modélisation B de la gestion dynamique de la mémoire, incluant l’allocation, la désallocation de la mémoire et la validité des pointeurs.
Cette implémentation OPC UA confirme que le développement de logiciels avec la méthode B avec des capacités de certification EAL4 et SIL2 est faisable et fondé.