S2OPC : OPC UA libre et sécurisé

Les bénéfices du logiciel libre pour du logiciel sûr

2020-02-20 17:24

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.

Publish-Subscribe Pattern 2/2

Pierre-Antoine Brameret

2020-01-27 10:33

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

2020-01-27 10:30

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).

Mininet and Performance Evaluation

Pierre-Antoine Brameret

2020-01-14 14:10

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.

S3 Formal Verification Solution — Instanciated Systems (4/4)

Nicolas Breton

2019-12-19 10:44

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.

S3 Formal Verification Solution — Workflows (3/4)

Nicolas Breton

2019-12-18 10:44

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.

S3 Formal Verification Solution — Introduction (2/4)

Nicolas Breton

2019-12-17 10:44

Introduction

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.

S3 Formal Verification — Executive Summary (1/4)

Nicolas Breton

2019-12-16 10:44

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.

Un jeu d’échec en Ada 2012

Robert Cholay

2019-12-09 08:51

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.

Ouverture du blog

Mathieu Clabaut

2019-12-03 17:10

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 !