PragmaDev Studio


   Use case

PragmaDev and CEA LIST common laboratory aims at generating a minimum set of test cases to cover all or a part of a model.


PragmaDev Studio

PragmaDev Studio is organized in 4 independent and integrated modules. Among them PragmaDev Specifier helps system engineers to unambiguously specify and verify the functionalities of the system, and define the best architecture for performance or energy efficiency. The technology used results in a graphical and executable model. Verification and validation of the dynamic of the system is done with the integrated simulator, and the best architecture is analyzed with a unique performance analyzer.

PragmaDev Tester helps testers to write validation and integration tests with an abstract dedicated language. A substantial number of test cases with this technology are published by international standardization bodies to ensure conformance to their specifications.

PragmaDev Studio can execute test cases described in PragmaDev Tester against a high level specification designed with PragmaDev Specifier.

PragmaList objective is to automatically generate conformance test cases out of a model. More precisely the minimum number of test cases that will cover a maximum of the model transitions.


The DIVERSITY platform developed in the LISE laboratory of the CEA LIST, gathers several tools dedicated to the validation and verification of complex embedded software systems. These tools take as inputs, models of complex systems corresponding to specification level and lower design level.

Models may be described with the help of Stateflow- type languages describing potentially concurrent and communicating automata. The two main tools offered by DIVERSITY are Diversi ty-TG and Diversity-MC:

  • Diversity-TG (TG for Test Generator) can, in a fir st step, generate simulation scenarios to validate the input model.
  • Diversity-MC (MC for Model Checker) can automatica lly validate a property with respect to the input model, provided that this property is express ed with inputs/outputs and state variables of the system in a linear temporal logic form.