LEIA : Intelligence Artificielle pour S3
A quoi sert LEIA ? Quel rapport entre la preuve formelle et l’intelligence artificielle ? En très résumé : la recherche d’éléments de lemmes permettant d’accélérer la preuve…
A quoi sert LEIA ? Quel rapport entre la preuve formelle et l’intelligence artificielle ? En très résumé : la recherche d’éléments de lemmes permettant d’accélérer la preuve…
Cet article a pour objectif d’évoquer brièvement certains outils de création et visualisation de plans de lignes de chemin de fer, et les contributions importantes de Systerel à ce sujet.
Cet article a pour objectif d’expliciter la notion de couverture de code et de montrer comment tout un chacun peut mettre en œuvre des métriques inclues dans gitlab sur son projet à Systerel.
In the Industry 4.0 context, data are a valuable asset that must be protected. OPC UA PubSub enables secure and interoperable solutions, but authentication of IIoT devices remains a sensitive issue. This article presents a novel approach based on open source software, using a Trusted Platform Module to protect secrets on devices, and evaluate the security level on a predictive maintenance use case.
The OVADO²®1 tool has been used for more than a decade to formally check whether system configuration data comply with their rules in the context of railway systems2. OVADO²® is currently deployed in SIL4 processes compliant with the safety requirements of the CENELEC EN 50128 standard. In these processes, it is considered a T2-class tool since it only helps to verify the system. This article describes how the OVADO²® tool has been used, for the first time, by Systerel to formally generate equipment configuration data derived from the system configuration data.
Après la présentation des images docker et de leur fabrication dans le billet précédent sur les Conteneurs et Docker, il est temps de voir comment utiliser les conteneurs en dehors de l’Intégration continue à Systerel.
La technique de « conteneurisation » a de nombreux avantages. Elle est notamment souvent utilisée dans le cadre de l’intégration continue pour sa capacité à définir un environnement reproductible d’un run à l’autre, quelle que soit la machine sur laquelle elle est exécutée. Cet article se propose d’exposer les intérêts et limites de cette technique dans le cas de Docker et de donner des bonnes pratiques de création d’images de conteneurs.
Méthodes formelles pour maîtriser la conformité des implémentations logicielles
Les techniques de Back-to-back Testing (B2BT) permettent de vérifier que deux produits des étapes d’un processus de développement logiciels sont équivalents. En exécutant « dos à dos » (back to back en anglais) les deux produits sur un ensemble de scénarios de test, on vérifie qu’ils produisent les mêmes sorties. Si les scénarios sont choisis avec soin, et que les deux exécutions donnent les mêmes résultats, il est possible d’en déduire que les deux produits sont équivalents avec un certain niveau de confiance.
Dans le cadre d’un projet réalisé pour l’un de ses clients, Systerel a dû trouver et mettre en œuvre une solution permettant d’intégrer au sein d’une application Ada2012 un mécanisme permettant de modifier simplement et à la volée le comportement de cette dernière sans avoir à modifier et donc à recompiler le code Ada2012 mis en œuvre.