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 system1, verifying that the properties hold on these traces.
The S2OPC team is proud to announce the 1.6.0 release of S2OPC.
This release introduces several improvements including:
As this revision contains important cybersecurity fixes, we advice all our customers to switch to this new revision.
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 ?!
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.
Depuis plus de 20 ans, Systerel est reconnue pour son expertise en développement de logiciels critiques, notamment dans le secteur ferroviaire où la norme EN 50128 est le standard de référence. Elle sera définitivement annulée à l’horizon 2026, au profit de la norme EN 50716, qui assure la continuité avec son aînée tout en apportant son lot d’améliorations et de nouveautés.
Dans cet article, nous proposons de revisiter le contexte, puis d’apporter et partager quelques réflexions sur l’EN 50716.
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.
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).
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 :
En octobre dernier, Systerel a obtenu le Visa de sécurité de l’Agence nationale de la sécurité des systèmes d’information (ANSSI) pour la certification CSPN (Certificat de Sécurité de Premier Niveau) de son produit S2OPC. Cela nous donne l’occasion de faire un focus sur ce qu’est la CSPN et de fournir un retour d’expérience sur son obtention.
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.
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 :
'Image,
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.
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.
Dans la littérature, on trouve une taxinomie des bugs teintée d’humour, mais non dépourvue d’une certaine réalité.
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.
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.
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.
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.
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 ».
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.
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.
Systerel présente le nouveau venu dans la famille Systerel Smart Solver : Multi-Agent Smart Solver (MASS). MASS permet de bénéficier des apports des clusters de calcul pour réduire significativement la durée de preuve perçue par l’utilisateur.
La mise en œuvre des différents éléments constitutifs d’un projet logiciel peut s’avérer être une tâche fastidieuse. C’est pour cela que, depuis de nombreuses années, un ensemble d’outils ont été développés afin de faciliter, de sécuriser et de systématiser celle-ci.
Cet article est une introduction à l’une des solutions existantes qu’est la technologie GNAT GPR (Gnat PRoject).
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.
Le portage d’un « legacy » Ada peut s’avérer être une tâche délicate malgré les qualités intrinsèques du langage comme, par exemple, sa réelle portabilité. Cet article identifie les principaux problèmes pouvant être rencontrés et la façon dont ils peuvent être au mieux adressés.
Cet article concerne le langage Ada mais, en termes de démarche, certains points sont transposables à d’autres langages.
Les bénéfices du logiciel libre pour du logiciel sûr
Suite au projet INGOPCS initié avec le support de l’ANSSI, Systerel a mis à profit son expérience dans le développement de systèmes critiques sûrs pour développer une pile OPC UA libre et sécurisée sous licence Apache 2.0 : Safe and Secure OPC (S2OPC).
Nous nous proposons dans cet article de rappeler ce qu’est OPC UA, de décrire le produit S2OPC, puis d’approfondir les bénéfices et les défis du logiciel libre pour un tel développement.
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.
This series of two posts presents an overview of the Publish/Subscribe pattern and analyses the features of some Pub/Sub implementations.
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).
Mininet is a network emulator. With Mininet, it is possible to create virtual hosts linked through virtual switches and links. Programs are executed on a single machine, but on different virtual hosts. This creates a network test bench which emulates complex (possibly corrupted or degraded) topologies.
As network emulation is run on a single machine, it is easy to automate tests and run them frequently.
Some systems are constructed by instantiating some generic design patterns on a collection of items (i.e. data). In the railway industry, the most widespread use of this mechanism is found for IXL, and to a lesser extend track-side ERTMS and CBTC systems.
While the overall structure of the S3 solutions dedicated to these kind of systems is not very different from that of the “standard” solutions described in the post about S3 workflow, they still admit some specificities. This section follows the structure of the aforementioned post and address these specificities.
This section will focus on IXL systems, but most of it could be adapted to other instantiated systems.
This post gives a generic description of the S3-based formal safety verification workflows. It starts with a short description of typical safety critical system development processes used in the industry. The two next section gives respectively a brief introduction to the S3 Modeling Languages, and a description of the development of the Safety Specification against which the system is to be verified. The rest of the section presents the S3 workflows together with the architecture and techniques used to ensure the trustworthiness of the solution.
The ever-rising use of software-based systems to fulfill safety-critical missions calls for methods to ensure the adequacy of these systems to their missions. Most industrial sectors have brought an answer in the form of standards such as EN-50128 for railways, DO-178C for aviation, ISO-26262 for automotive, or more generally IEC-61508 for critical systems. All these standards have in common the central role given to test-based validation techniques. However, alternate and usually complementary techniques, grouped under the banner of “Formal Methods”, are gaining increasing attention for the development and validation of these systems. In particular, the “Model Checking” technique has seen the multiplication of its application fields in the last decade.
Formal Verification is the act of mathematically proving that a system respects some properties under a number of hypotheses. When such a property is proved to hold, it means that it is impossible to find an input scenario satisfying the hypotheses in which the system would falsify this property.
Systerel Smart Solver (S3) is a formal verification solution able to perform a proof of the safety of a critical system after its design (i.e. a posteriori). This solution, combining a specialized modeling language (HLL) with a SAT-based symbolic model checker, has shown to be particularly efficient in handling industrial-size critical systems coming from various domains such as railways or avionics.
Développer un jeu d’échec peut s’avérer être une tâche ardue. Le présent article montre comment la mise en œuvre d’un certain nombre de paradigmes et de services sous-tendus par Ada 2012 permet de rendre cette tâche plus aisée.
Systerel ouvre son blog dédié aux sujets techniques. Vous y trouverez des articles liés aux produits Systerel comme Systerel Smart Solver ou S2OPC, mais aussi des articles de retour d’expérience sur notre façon de travailler et sur la mise en œuvre de technologies que nous jugeons intéressantes dans nos environnements de production.
Nous imaginons par ce biais pouvoir vous fournir une meilleure information sur nos produits et sur notre façon de travailler, mais aussi des guides techniques pour aborder certains problèmes.
N’hésitez pas à partager avec nous votre avis ou vos remarques.
Bonne lecture !