IMDEA Software Institute

Contact Information

---

Carolina Dania
IMDEA Software Institute
Campus de Montegancedo s/n
28223-Pozuelo de Alarcón, Madrid
SPAIN

Telephone: +34-91-101-2202
Fax: +34-91-101-1358
Cel: +34-683-294404

e-mail:
carolina.dania # imdea.org
       (Replace "#" by "@")

Traces Analyzer

• Description:
  Traces analyzer is a methodology for the analysis of ActionGUI models. ActionGUI toolkit generates automatically code from the ActionGUI models. The quality of the generated code depends on the quality of the source models. If the models do not specify the system intended behavior, one should not expect the generated system to do so either. Using the OCL2FOL+, I developed a methodology to analyze different kind of properties on ActionGUI models. They include checking consistency of the data model and analysis of invariant preservation on the GUI model. The methodology was implemented using the SMT solver Z3 and the automatic theorem provers SPASS as back ends.
  
  
• More people envolved: Manuel Clavel.
  
  A case study eHRM is available here.