Home > Products > PragmaDev Studio

One minute animation

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, development, 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 Studio can export models to tools from well known research centers such as Verimag, LAAS, or CEA List.

Model based testing


Once the stakeholders have validated the system with PragmaDev Specifier through the built in graphical user interface tool connected to the simulator, the resulting traces can be used to generate validation test cases.

Fully automatic

PragmaDev has setup collaboration with several recognized research centers specialized in model checking technologies to explore the model. As a result of these collaborations PragmaDev Studio offers several ways to automatically generate test cases out of a model. The test case generators can target:
  • Coverage: generate the minimum number of test cases that will cover all transitions in the model.
  • Transition: generate a test case that will cover a specific transition.
  • Property: generate a test case that fulfils a static property (process state, variable value,...).
  • Observer: generate the test cases verifying a dynamic property (succession of action or temporal rules). A dynamic property is defined as a state machine called observer.
Integration with third party validation tool can lead to property based test generation or property validation on the model.


PragmaList is a common lab PragmaDev has set up with French National Nuclear Research Center CEA List. CEA List has developed a symbolic model analysis tool. The result of this collaboration is an integrated, easy to use and efficient way to generate the minimum number of test cases that covers a maximum of a the model transitions.

Introducing 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.

Freemium model

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

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

V5 introduces a Performance Analyzer. It is now possible to put timing and energy consumption in your model and analyze if it meets your requirements. Played on a set of different architectures the tool will automatically find the best architecture of your system for performance or energy consumption.

Performance Analyzer
Performance analysis


Click here to get the brochure