Tools
|
|
|
|
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.
|
|
Diversity
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.
|
|
