Issue
Article
Vol.28 No.4, October 1996
Article
Issue
Issue |
Article |
Vol.28 No.4, October 1996 |
Article |
Issue |
In recent years there has been increasing interest in the application of formal methods in Interactive Systems [6][8]. This has been the topic of some international workshops [3][10][11] and many research institutes have begun work in this field. At CHI95 in Denver this was the topic of a workshop, but the discussion mainly focused on "what is formal" and did not consider in depth the state of the art in this area.
This area is particularly challenging as Interactive Systems are more complex than other classes of systems. However there is some scepticism from two sides: the formal methods community considers the work developed in this field as being too soft, whereas in the CHI community it is sometimes felt as too rigid.
We consider that a formal method is any method which uses notations with precise semantics to specify the system considered. We do not consider a formal specification just a natural language description of the functionalities considered.
Formal methods have proved to be useful for several application areas in order to improve the practice of the development process and the quality of the final result. It is an interesting open issue whether they can give valid results in the HCI field, for example whether they can give useful support in usability evaluation and obtain more reliable implementations of user requirements.
We think that formal methods are valid in specific phases of the development and design process of Interactive Systems and each specific approach is more suitable to address certain applications and problems. It is thus important to understand the differences and similarities among existing approaches.
The purpose of the workshop was to review the state of art in this area and to give a framework to evaluate current approaches. It was addressed to people who are strongly motivated to consider this area and have some experience in it.
In order to have a more focused discussion, a specific case study was selected and used to compare the various approaches proposed. This case study is a subset of the functionalities of a web application. We considered an environment where n browsers and one server are communicating and designers have to consider issues such as: history, browsability, non-pre-emptive behaviour, effective and continuous feedback of user interactions. Also, each approach was invited to consider properties such as button availability, the possibility to stop the interaction at each time, the possibility to go back to the initial state.
Each approach was evaluated against a design space for formal methods which considered at least five dimensions:
The selected participants were:
G. Abowd, Georgia Tech University (USA)
R. Bastide, University of Toulouse I (France)
D. Carr, University of Luleå (Sweden)
N. De Carolis, University of Roma (Italy)
A. Degani, San Jose State University (USA)
A. Dix, University of Huddersfield (UK)
P. Palanque, University of Toulouse I (France)
F. Paterno', CNUCE - C.N.R. (Italy)
E. Schlungbaum, University of Rostock (Germany)
P. Wright, University of York (UK)
The details of the proposed case study were circulated among all those who expressed interest in the workshop and were put up on a web server. Some discussions on the topics of the workshop were carried out beforehand by email. The selected presenters of specific approaches sent a position paper describing the first results on the application of their approach to the case study before the workshop. These position papers provided initial material to start discussions.
The first part of the workshop was dedicated to the presentation of the various methodologies applied to the case study. At the end of each presentation a short time was set aside for clarifying the presentations. The second part of the workshop was dedicated to creating a framework to compare the various approaches and to indicate when, how and where they can be applied in the design cycle. Finally, some discussion was dedicated to identifying the main results of the workshop and to decide how to carry on the work and how to communicate the results.
The main approaches considered were:
TLIM (Tasks, LOTOS, Interactors Modelling) [12], a method which uses task specification to structure the design of the user interface. To this end the LOTOS notation is used to indicate the temporal relationships among tasks and to specify the software components which support their performance.
Model Checking [1][10]. This is a technique which is based on building a model to describe the system of interest (by using a formal notation such as CCS or LOTOS) and then providing specific properties which summarise aspects of interest. Finally automatic tools are able to indicate whether or not the model satisfies the given properties.
ICO (a method based on Petri Nets and Object-orientation) [2], in this approach Petri Nets are used to indicate the temporal sequencing of actions and the objects are associated with the system components reacting to these actions.
Interaction Object Graphs [4], where both state modifications and behaviour in a user interface are described. The state modifications are presented by pictures representing the current state. The actions are represented by transitions labelled with UAN operators.
Coloured Petri Nets [5]. This is an extension of Petri Nets where colour tokens are used to indicate different types of data flowing in the net. This extension is used in a tool which integrates it with specific operators to formally specify and evaluate context-sensitive interfaces.
TADEUS Dialogue graphs [7] are a visual formalism with operators which try to capture in an immediate way the relationships among windows of a graphical user interface. In the TADEUS approach the Dialogue graphs are used to generate the user interface code automatically.
The discussion developed at the workshop pointed out four relevant dimensions to evaluate these methods besides those previously mentioned:
The discussion indicated that visual formalisms such as Petri Nets and TADEUS Dialogue Graphs are better for describing and explaining system behaviour, especially in not complex cases whereas process-based approaches and model checking are more useful to reason about user interface properties and to give indications about the effects of the design performed.
The workshop gave the opportunity to identify a research agenda for people working in this area. Some relevant directions identified were:
Since human behaviour is one the main parts of an Interactive System it becomes important that the notations and the models developed are able to describe it and not be limited to considering the user interface and the underlying software part.
Since formal methods are useful in various parts of the system design and development cycle it is important to have automatic tools which support the user in developing formal specifications and demonstrating its properties. Some recent tools developed in the formal methods community may be useful for this purpose, though it would be better to customise them for the specific needs of the application of formal methods in the human-computer interaction area.
The effort to learn formal methods is justified only if the system considered has a certain complexity, and finally some useful results can be obtained. It is thus important to apply them to larger case studies which have industrial relevance, especially in the application areas, such as safety critical systems, where the effects of an error in the design and specification can be very expensive. There is a lack of this type of work in the application of formal methods in human-computer interaction. This is demonstrated, for example, by the recent book [9] which reviews applications of formal methods in various fields and there is no chapter about applications to Interactive Systems.
As various approaches have been developed it was felt very important to have an opportunity to carry on the discussion in order to compare them and give more precise indications to designers and developers about when to use one method instead of another. Thus it was decided to write a book where the approaches developed (even from people who did not attend the workshop) are presented and discussed around the same case study as has happened in other application areas of formal methods.
Issue |
Article |
Vol.28 No.4, October 1996 |
Article |
Issue |