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