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 !
