| Summary: |
Human factors account for a very large proportion of failures in systems and the proportion is growing as methods of software development improve. There seems to be general agreement to attribute somewhere in the range of 60-90% of all system failures to erroneous human actions. Model checking has become an established verification technique both for hardware and software development. The attempt to apply model checking tools to the verification of complex human-computer interactions was a logical step. However, interactive systems pose a specific set of human related questions, and typical tools are not specifically tailored to address these. In the last decade the applicability of automated reasoning tools to the analysis of usability issues from interactive systems models has been investigated by a number of authors. In this context the PI has developed a prototype tool (i2smv) that supports a semi-automated analysis process of behavioural issues of the interaction. These works have been concerned mainly with investigating how the verification tools could be applied lo reason about issues related to human-computer interaction. Developing an understanding of how verification technology can help in usability evaluation is not enough. There is also the need to adequately support the verification process. A possibility for this is to build layers on top of the existing verification tools, creating an abstraction layer which assists in reasoning about interaction related issues and also make the tool more accessible to someone not fluent in formal methods. This project aims at developing i2smv into a more usable modelling and analysis tool. This in turn will enable it to act as a test-bed for the applicability of formal methods and tools to different styles of analysis of interactive systems models. The new tool will be called IVY (Interactors VerifYier). The tool will be modular in order to allow for future improvements. At this stage it is expected to consist of  |
Summary
Human factors account for a very large proportion of failures in systems and the proportion is growing as methods of software development improve. There seems to be general agreement to attribute somewhere in the range of 60-90% of all system failures to erroneous human actions. Model checking has become an established verification technique both for hardware and software development. The attempt to apply model checking tools to the verification of complex human-computer interactions was a logical step. However, interactive systems pose a specific set of human related questions, and typical tools are not specifically tailored to address these. In the last decade the applicability of automated reasoning tools to the analysis of usability issues from interactive systems models has been investigated by a number of authors. In this context the PI has developed a prototype tool (i2smv) that supports a semi-automated analysis process of behavioural issues of the interaction. These works have been concerned mainly with investigating how the verification tools could be applied lo reason about issues related to human-computer interaction. Developing an understanding of how verification technology can help in usability evaluation is not enough. There is also the need to adequately support the verification process. A possibility for this is to build layers on top of the existing verification tools, creating an abstraction layer which assists in reasoning about interaction related issues and also make the tool more accessible to someone not fluent in formal methods. This project aims at developing i2smv into a more usable modelling and analysis tool. This in turn will enable it to act as a test-bed for the applicability of formal methods and tools to different styles of analysis of interactive systems models. The new tool will be called IVY (Interactors VerifYier). The tool will be modular in order to allow for future improvements. At this stage it is expected to consist of the following components: a interactor models' editor, a properties editor, a compiler, a trace visualizer tool, and a reverse engineering component. The verification step will be carried out externally by the SMV model checker. The project is divided into 8 tasks: 1. Integration - responsible for guaranteeing that the work carried out in all the other different tasks can be integrated into a meaningful whole. 2. Development of the interactor models' editor. 3. Development of the properties definition wizard. 4. Development of the interactor to SMV compiler. 5. Development of the traces visualizer. 6. Development of the Java/Swing reverse engineering component. 7. Study of alternative modelling notations - will enable the identification of potential improvements/alternatives to the modelling approach. 8. Case study - responsible for an extended case study where the applicability of the IVY tool to a realist interactive application will be demonstrated. |