Acções do Documento

The Project

Project Description
The project is divided into eight tasks.
Task 1 - Integration
t+0 - t+36 [all members]
This task will be responsible for guaranteeing that the work carried out in all the other different tasks can be integrated into a meaningful whole. The end result will be the final version of the tool, together with a web site for its dissemination.
Task 2 - development of the interactors editor component
t+3 - t+12 [JFC/BIC1]
This task will produce a fully functional interactor models editor, supporting different editing modes, and capable of reading and writing files in a number of formats. The diferent editing models will enable the editor to be adjustable to diferent users and diferent editing tasks. The support for diferent file formats should enable at least a text format amenable for human reading, and an XML format for model exchange with the other components in the tool.
Task 3 - development of the properties definition wizard component
t+12 - t+21 [JFC/BIC2]
This task will produce a fully functional properties definition wizard, capable of supporting the IVY user in identifying and expressing relevant properties of the model under analysis. The wizard should have an assisted mode where the user is guided in the process by means of previously defined property patterns, and a fully manual model where users can write CTL formulae directly.
Task 4 - development of the interactors to SMV compiler
t+18 - t+24 [JFC/BIC3/JAS]
This task will produce a fully functional compiler from the MAL based interactor modelling language into the SMV input language.
Task 5 - development of the traces visualization component
t+18 - t+24 [JFC/ARF/BIC3]
This task will produce a fully functional visualization component, capable of supporting the IVY user in interpreting the results of the model checking step of the analysis. The component will animate the traces produced by the model checker in order to illustrate the scenarios of sage that these traces highlight.
Task 6 - development of the Java/Swing reverse engineering component
t+24 - t+36 [JFC/LSB/BI1]
This task will produce a fully functional reverse engineering component. The component will be capable of deriving interactor models of the user interfaces of applications developed in Java/Swing. The process will be partially automated only since the IVY user will have the opportunity of guiding the reverse engineering process. The tool will focus mainly on aspects regarding to what information is present at the interface. Behavioral issues will rely more on user guidance and input.
Task 7 - study of alternative modelling notations
t+0 - t+24
This task will enable the identification of potential improvements/alternatives to the modelling approach being used in IVY. It will explore other logics/specification languages, and what types of properties do they enable us to express and verify. It will look at how we can address representational issues into the analysis performed with the tool. It will look at approaches to restrict the space of analysis considered during the model checking step.
Task 8 - Case study
t+30 - t+36 [JFC]
This task will produce an extended case study where the applicability of the IVY tool to the analysis of a realist interactive application will be demonstrated.