PragmaDev Studio

Specification and Description Language

The Specification and Description Language (SDL) is a modeling language standardized by ITU-T to describe communicating systems.^[6] SDL is graphical but contains an action language with a semantic of execution making the SDL models executable.^[7] SDL is considered formal because it is complete and non-ambiguous.^[7] SDL-RT is a variant of SDL where the action language is replaced by C or C++ instructions.^[8] SDL-RT is considered semi-formal because it mixes SDL with code.^[2] ITU-T has standardized a UML profile based on SDL making by extension any SDL tool a sort of UML tool.^[9]

Simulation

PragmaDev Specifier embeds an SDL simulator that behaves like a model debugger.^[10] It is possible to set breakpoints graphically, to view variables, and pending timers.^[11] During execution a live trace is generated based on the Message Sequence Chart ITU-T standard.^[11]

Code generation (compiler)

PragmaDev Studio can generate C or C++ code out of an SDL model, and PragmaDev Developer can generate C or C++ code out of an SDL-RT model.^[12] The generated code can be adapted to any Real Time Operating System or scheduler.^[13] The tool offers a number of integrations with debuggers such as gdb so that the user feels he is still debugging the model, not the generated code.^[12]

Model checking

PragmaDev Studio can export the SDL model to different formats such as IF, FIACRE,^[14] or XLIA in order to verify the model in third party tools^[15] such as IFx from Verimag, TINA from LAAS, or Diversity from CEA LIST. In that organization the execution engine is the one from the model checker that is not fully aligned with the model semantics. In version 6 PragmaDev Studio has integrated OBP (Observer Based Prover) tool developed by ENSTA research lab ^[16]. In that integration OBP drives the exploration of the state space while the execution is done by the SDL execution engine. This guarantees the executions is conform to the SDL semantics.

Functional testing

PragmaDev Tester supports the TTCN-3 international standard for testing.^[17] The tool can either simulate the test cases against the SDL model, or generate code to be compiled and run against a real SUT.^[18]

Model Based Testing

• PragmaDev Studio can generate TTCN-3 test cases out of Message Sequence Charts resulting from a simulation.^[19]

• Test cases can also be generated out of the SDL model through a third party technology such as IFx from Verimag or Diversity from CEA-LIST: Laboratory for Integration of Systems and Technology.^[20] For that purpose PragmaDev Studio exports the model to a pivot language that is understood by the third party tool.^[20]

Deployment simulation

PragmaDev Studio can simulate the deployment of many instances of an SDL model for verifying its behavior in a distributed computing environment.^[11] This feature is based on research from Humboldt University of Berlin.^[21][22]

Performance analysis

PragmaDev Studio introduces a Performance Analyzer to find the best architecture for time or energy in a set of scenario.^[23]

CPS simulation

PragmaDev Studio supports Cyber Physical Systems (CPS) simulation via the Functional Mock-up Interface.^[24]

Telecommunications

• Alcatel has selected PragmaDev for the development and maintenance of their telephone switches.^[25]
• Sharif University has studied an optimization of the MAC layer for the IEEE 802.11wireless protocol.^[26]
• Modeling and simulation of IoT.^[27][28]
• Testing of network protocols.^[29]

Avionic and space

• Specification and development of the Air traffic control system for Airbus planes.^[30]
• System architecture optimization for a space mission.^[31]
• Integration in TASTE, the ESA framework dedicated to the development of real time and embedded systems.^[32]

Semi-conductors

• Hardware architecture optimization of micro-processors.^[33]

Security

• Development of a decentralized earthquake early warning system.^[34][35]
• Design and implementation of an automatic identification system.^[36]
• Safety requirements verification applied to European Train Control System.^[37]