Contents
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.
The benefits of open source
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.
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.
Contents
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.
Contents
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.
Contents
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.
Contents
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.
Developing a chess game can be a difficult task. This article shows how the implementation of a number of paradigms and services underpinned by Ada 2012 makes it possible to ease this task.
