Home > Products > PragmaDev Studio

PragmaDev Studio is a set of tools that helps Specifiers, Developers, and Testers to manage complexity in the development of today’s systems. PragmaDev Studio is our premium package that includes all other modules: PragmaDev Specifier, PragmaDev Developer, PragmaDev Tester, and PragmaDev Tracer, as well as a number of advanced features linking one module to another in a consistent environment. PragmaDev Studio is the ideal solution for small or large corporate entities that have a modeling or a testing need in one of its development phase such as specification, design, or validation.

In addition to the features of PragmaDev Specifier, PragmaDev Developer, PragmaDev Tester and PragmaDev Tracer, PragmaDev Studio includes the following specific features.

Model checking

Thanks to the execution semantic of the modeling language, analysis of the model can be automated to verify properties on the model with third party technologies. PragmaDev embeds OBP (Observer Based Prover) technology from ENSTA Bretagne research lab. The key caracteristic of OBP is that it does not rely on a dedicated language. It relies on a third party executor to execute the model. In PragmaDev Studio, OBP interacts with PragmaDev SDL executor to execute the transitions. OBP does not actually know anything about the model it is exploring. That garantees the model is properly interpreted by the exploration tool and allows to have built-in optimization features in the modeling tool.

Model based testing

In order to validate the system, stakeholders will use the built-in graphical user interface connected to the model simulator. All these scenarios can be saved and converted automatically to validation test cases that can be run on a real tester against the real system.


PragmaDev has partnership with some of the major research labs and regularly participate in collaborative projects. The latest collaboration includes Airbus and ENSTA Bretagne research lab to optimize business processes. The very promising results obtained lead to the integration of OBP in PragmaDev Studio.


Click here to get the brochure

Freemium model

PragmaDev Studio is free for small projects and education. Download it here.

Video presentation

Deployment Simulator

Mobile communication, M2M, and the Internet of Things deploys thousands or millions instances of small systems to build up a system of system. PragmaDev Deployment simulator aims at verifying such a topology works correctly. The network characteristics and the topology are taken into account. Graphical traces can be obtained on-line or replayed off-line with the ability to step back and forth. The deployment simulator can execute a huge number of instances of a part of the system and check the overall behavior remains correct.

Deployment Simulator
Deployment simulator

Performance analyzer

Timing and energy consumption can be associated to the actions in the model. The Performance Analyzer runs scenario on different architectures to help stakeholders decide which architecture is the best based on the system performances and energy consumption.

Performance Analyzer
Performance analysis

Internal traceability

PragmaDev Studio can import requirements files in csv format. The modeler can keep trace from a requirement to a model and testing will automatically analyze which part of the model it has covered. Therefore the impact analysis is straightforward and it is possible to know which test cases should be run if a requirement is modified.