Le SDL a été conçu pour décrire de manière détaillée et précise des systèmes communicants. En raison de sa nature asynchrone, le comportement est basé sur des machines d'états fonctionnant simultanément, ce qui rend la vérification de modèle d'un système SDL difficile. La création et la suppression d'instances dynamiques avec des PIDs calculés aléatoirement à la volée peuvent créer différents états du système qui devraient être considérés comme équivalents. Le nombre d'entrées possibles crée un tel nombre d'états du système qu'il est souvent trop grand pour être géré. De plus, lors de l'exploration, certaines variables internes, en raison de leurs valeurs, peuvent créer de nouveaux états alors qu'elles n'influencent pas réellement le comportement du système. Enfin, les vérificateurs de modèles existants sont basés sur leur propre langage qui n'est souvent pas aligné avec le langage de modélisation, SDL pour notre cas. Après quatre années de collaboration sur plusieurs projets industriels, l'ENSTA Bretagne et PragmaDev ont proposé une nouvelle approche de la vérification de système. Dans cet article, nous présentons le résultat de ce travail. Il combine quatre idées principales : 1) utiliser un moteur d'exécution basé nativement sur le langage de modélisation et séparé du vérificateur de modèle 2) restreindre les valeurs d'entrée possibles sans modifier le système lui-même 3) identifier les variables internes qui ne sont pas pertinentes pour l'état du système 4) réaffecter les PID et trier les instances pour identifier l'état du système.
Les modèles d’organisations, de systèmes et de systèmes de systèmes complexes peuvent être décrits avec NAF (NATO Architecture Framework) ou DoDAF (DoD Architecture Framework). La notation Business Process Model Notation (BPMN) fait partie de NAF et permet de décrire le comportement des différents acteurs du modèle. Cette notation est utilisée par l’Armée de Terre française ainsi que par ses principaux fournisseurs pour décrire les interactions entre les acteurs impliqués dans une mission. Il est donc primordial que les modèles soient corrects. Le projet VeriMoB est un projet de recherche financé par la DGA (Direction Générale de l’Armement) en collaboration avec Eurocontrol et Airbus DS qui ont fourni des cas d’utilisation réels. Le projet visait à développer un outil qui aidera les utilisateurs à vérifier leurs modèles BPMN. Cet outil couvre trois aspects principaux : une vérification statique, une exécution interactive, une exploration automatique des scénarios possibles. Suite à une demande du tout premier utilisateur de l’outil, cet article présentera l’analyse et la mise en œuvre d’un moyen automatique d’identifier les chemins inaccessibles dans un modèle BPMN en utilisant la technologie OBP issue du laboratoire de recherche ENSTA Bretagne.
Les modèles de systèmes complexes et de systèmes de systèmes sont décrits avec NAF (NATO Architecture Framework) ou DoDAF (DoD Architecture Framework). La notation Business Process Model Notation (BPMN) fait partie de NAF et permet de décrire le comportement des différents acteurs du modèle. Cette notation est utilisée par l’Armée de Terre française et ses principaux fournisseurs pour décrire les interactions entre les acteurs impliqués dans une mission. Il est donc important que les modèles soient corrects. Le projet VeriMoB est un projet de recherche financé par la DGA (Direction Générale de l’Armement) qui vise à développer un outil qui aidera les utilisateurs à vérifier leurs modèles BPMN. Cet outil couvre trois aspects principaux : la vérification statique, l’exécution interactive, l’exploration automatique des scénarios possibles. Cet article se concentre sur l’exploration automatique du modèle avec la technologie OBP issue du laboratoire de recherche ENSTA Bretagne.
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."
Il existe une forte demande d'environnements de développement de code minimal, qu'il s'agisse d'accélérer le développement d'applications dans un environnement hautement technique ou de permettre aux utilisateurs finaux de personnaliser un appareil. Selon le cabinet IDC en janvier 2023, le marché devrait connaître une croissance annuelle de 17,8 % de 2021 à 2026, avec des revenus projetés atteignant 21 milliards de dollars. Le code minimal sert d'abstraction aux langages de programmation traditionnels, ressemblant à un langage de modélisation. Diverses notations propriétaires de code minimal ont été développées spécifiquement, bien qu'elles manquent de standardisation, de portabilité et de réutilisabilité, nécessitant souvent un certain niveau de formation. Cette étude se penche sur les caractéristiques des notations de code minimal et examine si les langages de modélisation standard établis comme SDL ou BPMN pourraient servir d'alternatives viables à travers des cas d'utilisation pratiques simples.
De nos jours, la plupart des systèmes peuvent communiquer entre eux. De manière générale, un système communicant est un système piloté par événements. Le comportement est basé sur des machines à états déclenchées par des messages échangés entre des entités distantes, l'exécution des différents agents est asynchrone et de nombreuses données sont transférées. La combinaison d'entités concurrentes et les valeurs possibles des données échangées génèrent un nombre massif de chemins d'exécution. Pour ces différentes raisons, la vérification des propriétés sur de tels systèmes est un défi. Les vérificateurs de modèles existants sont basés sur leurs propres langages de modélisation qui ont été créés à des fins d'exploration, et non de modélisation d'un système communicant. Aujourd'hui, la meilleure notation de modélisation pour décrire les systèmes communicants de manière détaillée et précise est le SDL, qui est d'ailleurs normalisé par l'UIT-T. Le SDL est non seulement utilisé pour les systèmes de télécommunication, mais aussi dans les domaines aérospatial et automobile. La vérification des propriétés sur les systèmes SDL présente un grand intérêt. Après quatre ans de collaboration sur plusieurs projets industriels, l'ENSTA Bretagne et PragmaDev ont mis au point une nouvelle approche de la vérification des propriétés. Dans cet article, nous présentons le résultat de ce travail. Il combine quatre idées principales : 1) utiliser un moteur d'exécution basé nativement sur SDL 2) restreindre les valeurs d'entrée possibles sans modifier le système lui-même 3) réduire l'état du système 4) utiliser le PSC (Property Sequence Chart) pour écrire la propriété et la transmettre au vérificateur de modèle.
Les modèles de systèmes complexes et de systèmes de systèmes sont décrits avec NAF (NATO Architecture Framework) ou DoDAF (DoD Architecture Framework). Business Process Model and Notation (BPMN) fait partie de NAF et permet de décrire le comportement des différents intervenants du modèle. Cette notation est utilisée par l’Armée française ainsi que par ses principaux fournisseurs pour décrire les interactions entre les intervenants impliqués dans une mission. Il est donc important que les modèles soient corrects. Le projet VeriMoB était un projet de recherche financé par la DGA (Direction Générale de l’Armement) qui visait à développer un outil qui aidera les utilisateurs à valider leurs modèles BPMN auprès des parties prenantes. L’outil devait couvrir trois aspects principaux : une vérification statique, une exécution interactive et une exploration automatique des scénarios possibles. Cet article présentera le travail effectué pour tenter de convertir BPMN en SDL afin de remplir cet objectif avec un ensemble d’outils existant.
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."