Ada et le système de fichiers

Un vaste répertoire

Introduction

Depuis sa création, l’environnement prédéfini du langage Ada n’a cessé de s’enrichir. Même si les implémentations des compilateurs proposaient des librairies dédiées, il était par exemple peu aisé d’interagir avec le système de fichiers et ce de manière pérenne et portable. C’est pour cela qu’Ada₂₀₀₅ a introduit la hiérarchie Ada.Directories.

Au travers d’un exemple, nous allons faire un bref aperçu des possibilités offertes par cette hiérarchie.

S2OPC 1.7.3 release

The S2OPC team is proud to announce the 1.7.3 release of S2OPC.

This is mainly a security release. It fixes two vulnerabilities related to certificate trust and revocation checking, and we strongly recommend all users to upgrade. It also brings a new feature completing the Cyclone library wrapper, along with several enhancements and bug fixes.

S3 v2.0 — Une avancée majeure dans le monde de la vérification formelle

Introduction

La nouvelle version du moteur de preuve S3 arrive … et avec elle, une amélioration significative de ses performances ! De quelle manière et comment, embarquez avec nous pour découvrir un monde de nouvelles opportunités.

S2OPC 1.7.2 release

The S2OPC team is proud to announce the 1.7.2 release of S2OPC.

This release introduces several improvements including:

Alarms and Conditions: first support of the OPC UA AlarmConditionType
Optional structure fields: support for OPC UA Unions and Structures with optional fields
Thread-safe dictionary: a new thread safe dictionary API
Session management: the server wrapper can now terminate sessions (except one)

Pourquoi financer l’Open Source ?

Jérémie Barjhoux

Une utilisation libre …

Par la nature même de l’Open Source, l’utilisation d’un produit sous ce régime est gratuite et peut offrir une grande liberté en fonction de la licence à laquelle il est soumis. Selon les cas, il est même possible de le modifier ou l’inclure dans des offres payantes.

Les objets protégés en Ada

ou « Ada LoveRace condition »

(Image générée par IA)

Introduction

Dans un article précédent, Tâches et rendez-vous en Ada, nous avions présenté succinctement ce qu’était le tasking Ada et plus particulièrement le mécanisme de rendez-vous. Le fait que des tâches puissent s’exécuter en parallèle implique qu’elles puissent aussi accéder de façon concurrente à une donnée. Si nous n’y prenons pas garde, cette donnée peut alors devenir incohérente.

S2OPC 1.7.1 release

The S2OPC team is proud to announce the 1.7.1 release of S2OPC.

This is a maintenance release following the 1.7.0 version. It brings a few enhancements and a security-related bug fix that adds a check for a buffer over-read while verifying the signature of secure channel message chunks (see issue #1704).

Fuzzing tests

Cinthya Kouamou

Principle of fuzz testing. (Source: cybermatters.info)

Introduction

In the development of industrial software, it is common to manipulate complex binary protocols, specific data formats. These components are traditionally validated using unit tests, an effective approach to verify expected and well-defined behaviors.

Analyse Préliminaire des Risques : intérêt et méthodologie

Noemane Amanchar

(bionet, licensed under BY-SA)

L’Analyse Préliminaire des Risques (APR) est une méthode d’analyse déductive qui vise à repérer et évaluer les dangers dès les premières étapes de conception d’un système, d’un produit ou d’un processus. Son objectif principal est d’identifier en amont les situations dangereuses potentielles, afin de définir des mesures de sécurité, des exigences à respecter ou encore des dispositions de prévention et de protection. L’APR permet ainsi soit d’éviter la survenue de ces situations, soit d’en réduire les conséquences.

S2OPC 1.7.0 release

The S2OPC team is proud to announce the 1.7.0 release of S2OPC.

This release introduces several improvements including:

Security Audit: fires OPC UA events in case of cybersecurity related events
Role Permission: to assign permissions to roles rather than individual users, simplifying management and improving security
PubSub Extended Support: it is now available on Windows
History Read: adds the capacity for the server to store previous values of nodes
Node Management : completes the services to add and delete nodes run time
Performance Improvement: improves performance of write/add nodes operations
Zephyr 4.1 Support: compatible with the latest version of this real-time operating system

Tâches et rendez-vous en Ada

ou « Ada et les rendez-vous galants »

(www.pexels.com, licensed under PDM)

Introduction

Le tasking Ada offre la possibilité d’exécuter des portions de code de façon indépendante et au sein d’un même programme. Ce paradigme de la programmation concurrente permet à plusieurs tâches d’être exécutées simultanément ou de manière entrelacée.

Modélisation et Preuve B pour la détection de fuite mémoire

Minh-Thang Khuu

L’objectif de cet article est de donner un retour d’expérience de la preuve B pour la détection du risque de fuite mémoire dans le code généré à partir d’un modèle B et dans le cas qui nous intéresse, du modèle B de S2OPC

Exercice de crise de cybersécurité 2025

Mathieu Clabaut René Metery

Ce 10 octobre 2025, nous avons réalisé notre premier exercice de crise lié à la cybersécurité !

Pourquoi un exercice de crise de cybersécurité ?

Chez Systerel, nous travaillons depuis plusieurs mois à monter en conformité sur les questions de cybersécurité, qu’il s’agisse de la conformité à la norme ISO 27001 ou à la réalisation d’audits mandatés par des clients.

Ada pêche aux moules

Introduction

Le langage Ada offre, aux travers de la généricité, un mécanisme puissant permettant de créer des unités (sous-programmes ou paquetages) pouvant être utilisées avec différents types de données. Ce mécanisme permet d’avoir un code réutilisable, flexible et maintenable.

Découvrez trois bonnes raisons d’adopter l’open-source

Jérémie Barjhoux

L’Open Source : bien plus que du code gratuit

Davantage de garanties de Cybersécurité

À ses débuts, l’Open Source a fait face à de la défiance concernant la cybersécurité de par la possibilité d’accéder au code source. Il a depuis prouvé que cet accès apportait au contraire de meilleures garanties que du code propriétaire fermé : cela permet à différents acteurs, allant des utilisateurs aux universitaires en passant par les agences nationales de cybersécurité, d’auditer le code pour s’assurer de la présence des mécanismes indispensables (chiffrement, gestion de certificats/rôles…) et de l’absence de failles (CVE, backdoors, …).

L’IA ou l’Intelligence de l’Ada

Image générée par une IA

Un Adaiste convaincu vous dirait que le langage Ada est le « meilleur » des langages de programmation. Cela est bien évidemment faux, car le « meilleur » langage de programmation n’existe tout simplement pas et n’existera jamais. Chaque langage a ses qualités et ses défauts, et le choix du langage dépend en grande partie du projet dans lequel il est mis en œuvre.

GDS Push Server : Gestion des certificats et des listes de confiance OPC UA

Le standard de communication OPC UA permet de s’assurer de la confidentialité et de l’intégrité des échanges en s’appuyant sur les certificats X.509. Cependant, leur mise œuvre peut s’avérer laborieuse dans un environnement OT comprenant des mécanismes de mise à jour limités, de fortes contraintes de disponibilité sur un parc machines hétérogène et des compétences en cybersécurité peu présentes.

Comment tirer la couverture à soi

L’objectif de cet article est de donner quelques éléments sur ce qu’est la couverture de code, ce qu’elle apporte, ses différentes formes et dans quel cadre il est nécessaire de la mettre en œuvre.

Même si les exemples seront basés sur du code Ada, ils peuvent aussi s’appliquer à bien d’autres langages de programmation.

Model Checking: Formal Modeling and Verification

Model Checking: Formal Modeling and Verification

Model Checking is a Formal Safety Verification method in which tools are used to analyze a model of a system in order to verify if it respects some safety properties. The analysis is performed by exploring every possible evolution trace of the system¹, verifying that the properties hold on these traces.

S2OPC 1.6.0 release

The S2OPC team is proud to announce the 1.6.0 release of S2OPC.

This release introduces several improvements including:

OPC UA events management
Support of Zephyr revision 3.6 (see issue #1464)
Support of PikeOS revision 5.1 (thanks to our partner SYSGO) (see issue #1160)
Support of MbedTLS revision 3 (see issue #1446)
A complete rework of our Python binding PyS2OPC (see issue #1251)

As this revision contains important cybersecurity fixes, we advice all our customers to switch to this new revision.

Ada-mantium ou comment avoir une application fiable et sûre

L’adamantium est un métal imaginé par Marvel Comics et décrit comme étant le plus résistant de tous les métaux…

Et si on mettait de « l’Ada-mantium » dans nos applications ?!

Un nouveau cœur pour OVADO

Depuis plus de 10 ans le département MOP réalise des prestations de validation de données avec l’outil OVADO²® propriété de la RATP, qui est maintenu et distribué par Systerel.

Les delta aggregates en △da₂₀₂₂

Ada₂₀₂₂ a introduit la notion de delta aggregate permettant de modifier un objet sans passer nécessairement par une ou des données intermédiaires.

Cette fonctionnalité s’applique aussi bien aux structures qu’aux tableaux unidimensionnels.

On EN 50716, the latest software standard for safety-critical railway applications

Jérémie Saives

For over 20 years, Systerel has been recognized for its expertise in developing safety-critical software, particularly in the railway sector where the EN 50128 standard has been the reference. It will be definitively withdrawn by 2026, in favor of the EN 50716 standard, which ensures continuity with its predecessor while bringing its share of improvements and new features.

In this article, we propose to revisit the context, then provide and share some reflections on EN 50716.

A$_{da}$ la régulière

Le langage Ada est, par construction, contraint et il n’est par exemple pas aisé de parser facilement des chaînes de caractères.

Même si l’environnement Ada offre des services intéressants, il faut bien avouer que la possibilité d’utiliser des expressions régulières serait un plus.

S2OPC 1.5.1 release

The S2OPC team is proud to announce the 1.5.1 release of S2OPC.

The main new features are the availability of a demo server implementing the Push Management model according to the OPC UA part 12 (see issue #1247), and a hook to re-evaluate X509IdentityToken certificates for all sessions (on server side, see issue #1370).

TermiNA

Dans le cadre d’un portage Ada que nous avons réalisé pour un de nos clients, et en accord avec ce dernier, nous avons reconsidéré la façon dont l’application originelle en mode console gérait les traces et les logs.

Le système de traces et de logs souffrait des limitations suivantes :

First Level Security Certification (CSPN): The S2OPC Case Study

Vincent Pouzol Vincent Lacroix

CSPN visa

In October 2023, Systerel received the Security Visa from the French National Cybersecurity Agency (ANSSI) for the CSPN (First Level Security Certification) of its product: S2OPC. This achievement gives us the opportunity to focus on what the CSPN is and to provide feedback on the certification process.

INI-tiation

Configurer un logiciel peut se faire de différentes façons. La première est, par exemple, d’utiliser des options sur la ligne de commande. Cela se fait au travers du paquetage Ada.Command_Line ou encore plus simplement au travers du paquetage GNAT.Command_Line qui permet de définir et de traiter simplement les options d’une ligne de commande.

S2OPC 1.5.0 release

The S2OPC team is proud to announce the 1.5.0 release of S2OPC.

Comment voir la matrice ?

https://rosettacode.org/wiki/Matrix_digital_rain

L’objet de cet article est de montrer au travers d’un exemple complet quelques évolutions apportées par le langage Ada₂₀₂₂. Nous allons faire ici un bref focus sur :

La généralisation de l’attribut 'Image,
Les nouveaux types d’agrégats pour les tableaux,
Une utilisation des « Bigs Numbers ».

OVADO²® : second regard sur les données de configuration

Yannick Laumonier

OVADO²® est un outil RATP qualifié et extensible, dédié à la validation formelle des données de configuration des logiciels et systèmes. L’article Generating and verifying configuration data with OVADO²® décrit une utilisation d’OVADO²® dans le cadre d’un projet SIL4 de génération formelle de données de configuration.

Portons-nous bien

Problématique

Dans le cadre de certains portages Ada, on peut souhaiter continuer à faire vivre un temps le code legacy tout en commençant à utiliser le code porté.

Si, à l’issue du portage, on découvre un problème ou une évolution dans le code legacy, on devra alors reporter les modifications induites dans le code porté. On peut aussi avoir la situation inverse. En d’autres termes, les codes devront coexister.

Chercher la petite bête

Dans la littérature, on trouve une taxinomie des bugs teintée d’humour, mais non dépourvue d’une certaine réalité.

What did you Expect?

Pour assurer un certain nombre de services au sein de votre application Ada, il peut être intéressant et élégant d’utiliser des applications déjà existantes. Par exemple, si je dois faire des requêtes FTP, il est évidemment plus simple d’utiliser le client du même nom. Si l’application que vous voulez utiliser est en mode interactif (c’est le cas de la commande ftp) alors, la tâche risque d’être ardue.

Securing IIoT communications using OPC UA PubSub and Trusted Platform Modules

Olivier Gilles Daniel Gracia-Perez Pierre-Antoine Brameret Vincent Lacroix

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.

Generating and verifying configuration data with OVADO²®

Frédéric Badeau Joris Lamare

The OVADO²®¹ 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 systems². 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.

Back-to-back Testing

Formal methods to control the compliance of software implementations

Anaïs Guignard Julien Niguez Nicolas Breton Vincent Pouzol

Back-to-back zebras

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.

On a marché avec la lune

La lune selon Méliès

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 Ada₂₀₁₂ 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 Ada₂₀₁₂ mis en œuvre.

Un échafaudage pour le développement de vos applications Ada

Un échafaudage

Dans la phase de construction ou de rénovation de bâtiments, un soin tout particulier doit être apporté à la mise en place d’échafaudages. Ces derniers permettent un accès au chantier efficace et sûr pour les artisans et le matériel.

Pour le développement d’une application, c’est exactement la même chose, votre échafaudage sera ici l’environnement de développement.

Un code a les preuves du temps

Natacha Porté Robert Cholay

A warpped clock

Au travers de l’article Démarche de portage d’un “legacy” Ada nous avions présenté les principaux problèmes pouvant être rencontrés lors d’un portage d’un legacy Ada et la façon de les adresser au mieux. L’approche ainsi proposée était « classique » et elle ne faisait aucunement appel aux méthodes formelles au travers par exemple de la technologie SPARK.

Dans le présent article, nous allons vous présenter en quoi la technologie SPARK peut conforter cette approche « classique ».

On n’a pas tous les jours vingt ans…

Berthe Sylva vers 1925 — En référence au titre de cet article…

Depuis maintenant une bonne dizaine d’années, les industriels doivent mener à bien des programmes de rénovation de systèmes développés en moyenne depuis plus de vingt ans. Ces rénovations impliquent généralement une remise à niveau aussi bien matérielle que logicielle.

Dans ce cadre, Systerel accompagne ses clients et ce dans des secteurs aussi variés que le transport, la défense ou l’avionique.

Ces développements nous ont ainsi amenés à avoir une réflexion rétrospective sur les changements opérés depuis plus de vingt ans sur la façon de développer du logiciel critique.

Use of B method for dynamic structures in S2OPC

Frédéric Badeau Vincent Lacroix Vincent Monfort Laurent Voisin

The software B method has so far been mainly used in the industrial world to develop safety critical software with very basic memory management limited to arrays of fixed size defined at compilation time.

We present here an alternative approach for modelling software based on a more classic memory management with dynamically allocated complex data structures accessed through pointers.

Multi-Agent Smart Solver (MASS)

Systerel introduces the latest member in Systerel Smart Solver family: Multi-Agent Smart Solver (MASS). MASS significantly reduces proof wall clock time for the user, using extensible computing clusters.

An overview of the GPR technology

GPR diagram

Implementing the various components of a software project can be a tedious task. This is why, for many years, a set of tools has been developed to facilitate, secure and systematize it.

This article is an introduction to one of the existing solutions named GNAT GPR (Gnat PRoject).

Certificate trust chain validation in OPC UA

Vincent Monfort

Stamp

OPC UA client/server protocol security is based on application certificates, each application shall trust each other. Determining if a certificate is trusted might include verification of a trust chain in cases that were not expected at first sight. This article explains how to validate a certificate to pass OPC UA certification 1 and hence how to configure correctly certificate validation to ensure your application certificate is accepted.

Porting an Ada legacy software

Ada Lovelace

Porting an Ada legacy software can be a delicate task despite the intrinsic qualities of the Ada language such as, for example, its true portability. This article identifies the main problems that may be encountered and how they can best be addressed.

This article is about the Ada language but, in terms of approach, some points are transposable to other languages.

S2OPC — Safe, Secure, Open Source OPC-UA

The benefits of open source

Mathieu Clabaut

Following the INGOPCS R&D project initiated with the support of the ANSSI, Systerel has built upon its experience of safe critical systems to develop a free and secure OPC UA stack under the Apache 2.0 license: Safe and Secure OPC (S2OPC).

In this article, we will give an overview of OPC UA, describe the S2OPC product, and then focus on the benefits and challenges of the open source approach for such a development.

Publish-Subscribe Pattern 2/2

Pierre-Antoine Brameret

This post is the second in the series. The previous one described the Publish/Subscribe pattern and analysed MQTT, MQTT-SN and DDS specifications. This article will continue the analysis of other protocols including OPC-UA PubSub, according to the characteristics highlighted in previous post.

Publish-Subscribe Pattern 1/2

Pierre-Antoine Brameret

This series of two posts presents an overview of the Publish/Subscribe pattern and analyses the features of some Pub/Sub implementations.

What is Pub/Sub? 1

The publish subscribe pattern is a messaging pattern, where publishers publish messages to topics and subscribers subscribe to topics to receive messages. In this pattern, publishers and subscribers are not directly connected to each other (loosely coupling).