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.
Formal methods to control the compliance of software implementations
Back-to-back testing (B2BT) techniques are used to verify that two products of a software development process are equivalent. By running the two products “back to back” on a set of test cases, it is verified that they produce the same output. If the scenarios are chosen carefully and the two runs produce the same results, it can be inferred that the two products are equivalent with some level of confidence.
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.