SDL has been designed to describe communicating systems in a detailed and precise way. Due to its asynchronous nature, the behaviour is based on state machines running concurrently, making model checking of an SDL system a challenge. Creation and deletion of dynamic instances with PIDs randomly computed on the fly can create different system states that should be considered equivalent. The number of possible inputs creates such a number of system states that it is often too large to handle. Furthermore during exploration some internal variables, because of their values, might create new states while they actually do not influence the behavior of the system. Finally existing model checkers are based on their own language which is often not aligned with the modeling language, SDL for our concern. After four years of collaboration on several industrial projects, ENSTA Bretagne and PragmaDev came up with a new approach to system verification. In this paper we will present the result of this work. It combines four main ideas: 1) use an execution engine which is natively based on the modeling language and separated from the model checker 2) restrict the possible input values without modifying the system itself 3) identify internal variables that are irrelevant to the system state 4) re-assign PIDs and sort the instances to identify the system state.

Models of complex organizations, systems and systems of systems can be de-scribed with NAF (NATO Architecture Framework) or DoDAF (DoD Architecture Framework). Business Process Model Notation (BPMN) is part of NAF and allows describing the behavior of the different participants in the model. This notation is used by the French Army as well as its main suppliers to describe the interactions between participants involved in a mission. It is therefore paramount the models are correct. The VeriMoB project was a research project financed by the DGA (Direction Générale de l’Armement) in collaboration with Eurocontrol and Airbus DS who provided some real use cases. The project aimed at developing a tool that will help users to verify their BPMN models. This tool covers three main aspects: a static verification, an interactive execution, an automatic exploration of the pos-sible scenarios. Following a request from the very first user of the tool, this paper will present the analysis and implementation of an automatic way to identify the unreachable paths in a BPMN model using the OBP technology coming from ENSTA Bretagne research lab.

Models of complex systems and systems of systems are described with NAF (NATO Architecture Framework) or DoDAF (DoD Architecture Framework). Business Process Model Notation (BPMN) is part of NAF and allows to describe the behavior of the different participants in the model. This notation is used by the French Army and its main suppliers to describe the interactions between participants involved in a mission. It is therefore important the models are correct. The VeriMoB project is a research project financed by the DGA (Direction Générale de l’Armement) which aims at developing a tool that will help users to verify their BPMN models. This tool covers three main aspects: static verification, interactive execution, automatic exploration of the possible scenarios. This paper focuses on the automatic exploration of the model with OBP technology coming from ENSTA Bretagne research lab.

The JUpiter ICy moons Explorer mission, JUICE, is the first large-class mission in the Cosmic Vision 2015-2025 program of the European Space Agency. Planned for launch in 2022 and arrival at Jupiter in 2030, it will spend at least three years making detailed observations of the biggest planet in the Solar System and three of its largest moons, Ganymede, Callisto and Europa. JUICE will carry a total of 11 scientific experiments (instruments) to study the gas giant planet and its large ocean-bearing moons. Each instrument will do a number of readings producing streams of data, which will be stored in the on-board mass storage and then transmitted to Earth via a specific protocol. In this paper we present a model-based approach for system optimization in terms of instrument parameters, mass storage configuration, and transmission band allocation. We use standard modeling and testing languages with formal semantics for describing the system and the different configuration scenarios, which are then executed in co-simulation mode to produce (1) very precise results and (2) graphical comparison of different configurations to help trade off.

The Internet of Things (IoT) refers to the networked interconnection of objects equipped with ubiquitous intelligence, or simply “smart objects”. The “smart” part is often followed by words like grid, home, parking, etc., to identify the application domain, and it is provided by software applications and/or services running on top of these large-scale distributed communication infrastructures. Heterogeneity and distribution scale speak for the complexity of such systems and call for a careful analysis prior to any deployment on target environments. In this paper we introduce a model-driven approach for the analysis of IoT applications via simulation. Standard modeling languages, code generation, and network simulation and visualization are combined into an integrated development environment for rapid and automated analysis.

The constantly ever-growing interest for large-scale distributed systems like the Internet of Things imposes many challenges for developers and researchers from many areas. The development of distributed software applications is by no means trivial, and their inherent complexity becomes apparent during testing. Indeed, testing the operation of single isolated nodes does not suffice, because it may be affected by the distribution and inter-communication between nodes. Re-writing a test case to consider distribution is neither efficient nor simple, because concurrency is never easy to implement. In this paper we present an approach that automatically interleaves execution of test cases to simulate concurrency inherent in distribution. We focus on independent test cases that might exhibit a correlation due to distributed interaction. The approach is applied in the context of standard modeling and testing languages, and enables identification of interaction points during test case execution that depend on distribution. The re-execution of the test case is then interleaved at the identified points to account for distribution.

Specific modelling technologies for digital hardware design are typically the synthesizable, cycle-accurate register-transfer level descriptions (VHDL or Verilog RTL) or bit-accurate transaction level models (SystemC TLM). Given nowadays complexity of circuits such as System-on-a-Chip (SoC) for multimedia embedded systems, and of the embedded software interacting with the SoC, there is a need for a higher abstraction level that would ease mastering the interaction, starting from initial conceptual stages of a product development. The Specification and Description Language (SDL) modelling technology allows to describe functional models independently from their implementation. This paper describes a work done by STMicroelectronics and PragmaDev to experiment the use of SDL high level functional description in a typical simple hardware/ software interaction scenario involving interrupts handling.

Interconnected smart devices constitute a large and rapidly growing element of the contemporary Internet. A smart thing can be as simple as a web-enabled device that collects and transmits sensor data to a repository for analysis, or as complex as a web-enabled system to monitor and manage a smart home. Smart things present marvellous opportunities, but when they participate in complex systems, they challenge our ability to manage risk and ensure reliability.
SDL, the ITU Standard Specification and Description Language, provides many advantages for modelling and simulating communicating agents – such as smart things – before they are deployed. The potential for SDL to enhance reliability and safety is explored with respect to existing smart things below.
But SDL must advance if it is to become the language of choice for developing the next generation of smart things. In particular, it must target emerging IoT platforms, it must support simulation of interactions between pre-existing smart things and new smart things, and it must facilitate deployment of large numbers of similar things. Moreover, awareness of the potential benefits of SDL must be raised if those benefits are to be realized in the current and future Internet of Things.

Chapter 23 regarding the validation and verification of model based software requirements and designs namely quotes SDL (LDS in the text) as a modeling technology to design embedded software of aircraft equipment.

UML has been described by some as “the lingua franca of software engineering”. Evidence from industry does not necessarily support such endorsements. How exactly is UML being used in industry – if it is? This paper presents a corpus of interviews with 50 professional software engineers in 50 companies and identifies 5 patterns of UML use.

"Simulation is a popular method used for analysis and validation of distributed communication systems due to their complex dynamics. Visualization has proven to be an added value especially when large networks are concerned. In this paper we propose a novel approach and tool support for simulation visualization of formally described distributed communication systems. The system is modeled using Specification and Description Language Real Time (SDL-RT) and a simulation model for the ns-3 network simulator is automatically generated. Network visualization is used in combination with Message Sequence Charts (MSC) for providing detailed visual insight into system dynamics. System validation is also made possible because of the formal semantics of MSCs."

"A real time / embedded software is basically a software nobody sees but it is the one that has most constraints in the software industry such as high-level of reliability, small memory footprint, and high performance. In the same time embedded software requirements are getting more and more complex because all devices should now be able to communicate with each other and also because hardware components prices are dropping allowing the usage of powerful processors for small systems. What used to be a few hundred bytes of code in assembly language is now hundreds of thousands of lines in C code. Therefore it is a priority for all real time software developers to make sure the software architecture is good, the interfaces with other modules is well defined, the code is legible and re-usable. A reduced time to market also brings the need to develop software before the hardware is done: simulating and prototyping the software is now a must."

"Simulation is often the method of choice for analysis and validation of distributed communication systems because of their complex dynamics. But simulation modeling is not a trivial task mainly because there exists no unified approach that can provide description means for all aspects of such complex systems. These aspects include architecture, behavior, communication, and configuration. In this paper we focus on simulation configuration as part of our unified modeling approach based on the Specification and Description Language Real Time (SDL-RT). Deployment diagrams are used to describe the simulation setup of the components and configuration values of a distributed system. We provide tool support for automatic implementation of the models for the ns-3 network simulation library."

"A new approach for Earthquake Early Warning Systems (EEWS) is presented that uses wireless, self-organising mesh sensor networks. To develop the prototype of such IT-infrastructures, we follow a model-driven system development paradigm. For modelling a technology mix of SDL/ASN.1/UML/C++ is used to generate the code for different kind of simulators, and for the target platform (several node types). This approach is used for realizing a prototype-EEWS developed within the EU project SAFER (Seismic eArly warning For EuRope) in cooperation with the GeoForschungszentrum Potsdam."

"This work presents some new optimization approaches to implementation of Medium Access Control (MAC) layer of IEEE 802.11 wireless networking protocol using general purpose DSP and gate array systems. Optimization starts at design level. The hardware/software partitioning of the MAC’s architecture is optimized in the sense of minimal implementation burden, while maintaining the system’s functionalities and performance. The proposed partitioning and implementation technique obviates the use of any Real Time Operating System (RTOS), which leads to a simple, high speed, and low memory structure of the MAC’s software. Also, solutions such as using hash tables and pipeline processing are given and employed to gain a higher speed. The software section is implemented on the popular, low price DSP of TI’s C54 processor, whereas the hardware implementation is realized using Virtex2vp30 from Xilinx."

If your programs are sending and receiving data structures, you are probably using high-level encapsulations - e.g. XML or JSON. There are however far more optimal solutions in terms of memory, CPU and network requirements ; ASN.1 is one of them.

"Nous allons passer en revue les concepts du langage SDL, son historique, et évaluer les forces et faiblesses respectives de SDL et UML afin de projeter ce qui, à notre avis, serait une solution optimale pour l’utilisation de l’un ou l’autre de ces langages."

"Implementation of TTCN-3 in RTDS tool raised some interrogations. The concept of snapshot in the TTCN standard is not present in traditional RTOS. This paper will first make a short presentation of TTCN-3. It will then explain the alternative rationale and the concept of snapshot. A reminder of event-driven concepts in major RTOS will be done, to finish with a presentation of several solutions to implement the snapshot."

There is a high demand for low code development environments, whether it is to accelerate application development in a highly technical setting or for end users to personalize a device. According to market intelligence provider IDC in January 2023, the market is expected to experience a 17.8% annual growth from 2021 to 2026, with projected revenues reaching up to $21 billion. Low code serves as an abstraction to traditional programming languages, resembling a modeling language. Various proprietary notations have been developed specifically for low code development, although they lack standardization, portability, and reusability, often necessitating some level of training. This study delves into the characteristics of low code notations and explores whether established standard modeling languages like SDL or BPMN could serve as viable alternatives through simple practical use cases.

Nowadays most systems can communicate with each other. As a general approach, a communicating system is an event driven system. The behavior is based on state machines triggered by messages exchanged between remote entities, execution of the different agents is asynchronous, and there is a lot of data being transferred. The combination of concurrent entities and the possible values of the data exchanged generate a massive number of execution paths. For these different reasons, the verification of properties on such systems is a challenge. Existing model checkers are based on their own modeling languages that have been made up for the purpose of exploration, not for the purpose of modeling a communicating system. Now the best modeling notation to describe communicating systems in a detailed and precise way is SDL which is standardized by ITU-T for that matter. Not only SDL is used for telecommunication systems but also in the aerospace and automotive domains. Verifying properties on SDL systems is of great interest. After four years of collaboration on several industrial projects ENSTA Bretagne and PragmaDev came up with a new approach to property verification. In this paper we will present the result of this work. It combines four main ideas: 1) use an execution engine which is natively based on SDL 2) restrict the possible input values without modifying the system itself 3) reduce the system state 4) use the PSC (Property Sequence Chart) to write the property and pass it along to the model checker.

Models of complex systems and systems of systems are described with NAF (NATO Architecture Framework) or DoDAF (DoD Architecture Framework). Business Process Model and Notation (BPMN) is part of NAF and allows describing the behaviour of the different participants in the model. This notation is used by the French Army as well as its main suppliers to describe the interactions between participants involved in a mission. It is therefore important the models are correct. The VeriMoB project was a research project financed by the DGA (Direction Générale de l’Armement) which aimed at developing a tool that will help users to validate their BPMN models among the stakeholders. The tool had to cover three main aspects: a static verification, an interactive execution, and an automatic exploration of the possible scenarios. This paper will present the work done trying to convert BPMN to SDL in order to fulfil this objective with an existing toolset.

The design of a practical but accurate software methodology to guarantee systems correctness and safety is still a big challenge. Where test coverage is dissatisfying, formal analysis grants much higher potential to discover errors or safety vulnerabilities during the design phase of a system. However, formal verification methods often require a strong technical background that limits their usage. In this paper, we present a framework based on testing and verification to ensure the correctness and safety of complex distributed software systems. As a result of the application of our methodology we obtain a more reliable system, in terms of functionality, safety and robustness and a reduction of the time necessary for verification. In order to show the applicability of our solution we applied it on a real industrial case study, that is the European Train Control System (ETCS) (ERTMS Commission Group - European Commission, 2017). We specify the system using the SDL language (ITU-T, 2019), and we use a test generation tool to generate abstract test cases in TTCN-3. Based on these standardized tests, we verify using model-checking, some critical properties of the system, in particular these regarding safety requirements. We analyse a real train accident and we demonstrate how the accident could have been avoided if the ETCS system was used.

Models of complex systems and systems of systems are described with NAF (NATO Architecture Framework) or DoDAF (DoD Architecture Framework). Business Process Model Notation (BPMN) is part of NAF and allows describing the behavior of the different participants in the model. This notation is used by the French Army as well as its main suppliers to describe the interactions between participants involved in a mission. It is therefore important the models are correct. The VeriMoB project is a research project financed by the DGA (Direction Générale de l’Armement) in collaboration with Eurocontrol and Airbus DS who provided some real use cases. The project aims at developing a tool that will help users to verify their BPMN models. This tool covers three main aspects: a static verification, an interactive execution, an automatic exploration of the possible scenarios. This paper will present the results from this project.

Models in the railway industry are often based on synchronous technologies such as Matlab or Scade. This is due to technical reasons, but because of its concepts the abstraction level of synchronous models are very low and very close to the implementation level. A serious gap is observed between the requirements described in natural textual language and the model which is basically an implementation. The increasing level of system complexity, combining communicating subsystems, calls for a more abstract model. This paper will first discuss why synchronous technologies have been used in this type of systems, then an experiment of using an asynchronous technologies on a real ERTMS case coming from SNCF is described, and finally the paper will conclude on how an asynchronous modeling technologies could make the link between the informal textual requirements and the implementation of the system.

The interest in pragmatic analysis methods is constantly fueled by the increasing complexity of software systems. Although the methods are not scarce, to apply them successfully an additional expertise is required, which often deviates from the development process or the domain the system is intended for. The model-driven paradigm facilitates the development and analysis by means of automation. It can address the issue at a certain extent by raising the level of abstraction closer to the domain. The inherent complexity is shifted from the model towards the automation process. This has been quite effective in handling functional aspects, but non-functional aspects like performance have proven to be challenging in this regard. In this paper we present a model-driven approach for performance analysis based on standardized languages. SDL is used to capture the functional aspects of the system, which are further enriched with performance annotations. Deployment diagrams allow for the available resources to be assigned to system components, and model execution is driven by real test cases in TTCN-3. Automatic execution of different scenarios and graphical presentation of the results can aid the user to optimize performance by choosing the best allocation of resources in terms of execution time and payload.

The objective of the PragmaList Lab, a joint laboratory between PragmaDev and CEA LIST, is to integrate the test generation tool DIVERSITY in the SDL modeling environment Real Time Developer Studio (RTDS). The resulting environment aims to extend RTDS with a Model-Based Testing approach. After briefly describing the characteristics of RTDS and DIVERSITY, this paper presents the work done to integrate these two environments. Then, it highlights the main principles of DIVERSITY based on symbolic execution, which enables the generation of test cases in TTCN-3 format. The paper then presents the existing coverage criteria in the integrated generation of test cases. It concludes with the open strategy of the PragmaList approach to work together with industrial actors based on the definition and integration of new specific coverage criteria consistent with their validation constraints.

The translation of a system model to an intermediate format is an important step towards formal proofs of properties. This paper presents the formulation of rules to enable the translation of SDL standard models to Fiacre language. The translated model is then provided as input to a suitable toolset that performs model checking and other analysis. The formulated translation rules are discussed in view of the correctness of translation and ease of implementation. Implementations of some of the translation rules in an industrial tool (PragmaDev RTDS), and a proof of the concept on a simple SDL model are presented to ascertain the validity of the proposed translation.

"Since 2002, CS is involved in the conception and the specification of ATC systems for A320, A340, A380, A400M and A350 aircrafts. The ATC module, a ground/onboard communication system, is designed with SDL, a modelling language normalized by the ITU-T and which is described as a UML2-profile, too. The SDL well defined semantic allows to have homogeneous code generators and model simulators: these two technics are used in the process of the ATC projects, giving to the process a very efficient productivity. The automatic code generator generates the C code of the application. The code generator is qualified in accordance to the DO178B requirements (C level). This very strict qualification (development tool qualification) allows to highly reduce the tests effort of the ATC application. Verifications based on tests are realized on the SDL models, through execution simulation. CS uses RTDS, a SDL Z.100 simulator developed by Pragmadev. As well as providing edition and syntax/semantic checking of SDL models, RTDS provides debugging facilities such as breakpoints and step-by-step execution at the model level and a powerful scenarios language which enables to call some directives of the simulator such as MSC generation, internal signals sending, variables printing and so on…"

In the development process the very first phase focuses on the requirements. Most of the requirements are dynamic and describe how the system reacts to a set of stimuli. Not all the possible reactions are listed in the requirements but some mandatory reactions are described that can be seen as properties. Later in the development process is a real system or a representative model of the future system. At that point it is possible to gather execution traces of the real system. Based on the work of the European PRESTO project this paper describes the work that has been done to use the same kind of model in both cases and match one against the other.

After describing the SDL current position within the modelling languages domain, this document describes the route plan to 2010 version of the language.

TASTE stands for “The ASSERT Set of Tools for Engineering”, in reference to the European FP6 program where it finds its roots. It consists in an open-source tool-chain dedicated to the development of embedded, real-time systems. TASTE addresses the modelling and deployment of distributed systems containing heterogeneous software and hardware components; it focuses on the automation of tedious, error-prone tasks that usually make complex systems difficult to integrate and validate. TASTE relies on two complementary languages, AADL and ASN.1, that allow to create embedded systems which functional parts are made of C, Ada, SDL, SCADE, Simulink and/or VHDL code.

"Abstract: The TASTE tool-set results from spin-off studies of the ASSERT project, which started in 2004 with the objective to propose innovative and pragmatic solutions to develop real-time software. One of the primary targets was satellite flight software, but it appeared quickly that their characteristics were shared among various embedded systems. The solutions that we developed now comprise a process and several tools ; the development process is based on the idea that real-time, embedded systems are heterogeneous by nature and that a unique UML-like language was not helping neither their construction, nor their validation. Rather than inventing yet another “ultimate” language, TASTE makes the link between existing and mature technologies such as Simulink, SDL, ASN.1, C, Ada, and generates complete, homogeneous software-based systems that one can straightforwardly download and execute on a physical target. Our current prototype is moving toward a marketed product, and sequel studies are already in place to support, among others, FPGA systems."

"La production de systèmes critiques (contrôle de véhicule, détection de fautes, drones, etc.) requiert le respect de nombreuses exigences: ils opèrent dans des environnements contraints (domaine avionique, spatial, militaire) et s'exécutent sur des plateformes embarquées ayant des ressources limitées (capacité de calcul, taille mémoire). De plus, une erreur dans leur implémentation peut avoir de lourdes conséquences (abandon d'une mission, perte de vie) si bien que leur code doit être exempt de bogue. La conception de tels systèmes demande donc un processus de développement rigoureux, s'appuyant sur des technologies détectant tout potentiel vecteur d'erreur. Cet article présente une chaîne d'outils implémentant de tels systèmes au travers d'un cas pratique l'implémentation d'un drone d'exploration avec Linux."