From: johnson@minster.york.ac.uk Subject: EVENT: Formal Methods & HCI Workshop, York, UK, 23 Jul 93 (abstracts, long) Date: 17 Jun 1993 11:43:35 GMT Organization: Department of Computer Science, University of York, England I've received a number of request for abstracts from the papers to be presented at the workshop - here they are... Registration information can be obtained from the workshop organisers (johnson@minster.york.ac.uk). Yours, Chris. --------------------------------- Workshop On Formal Methods For The Design Of Interactive Systems Friday, 23 July, 1993. The Huntingdon Room, King's Manor, York, U.K. 10.00 Registration and coffee 10.30 H. Thimbleby Stirling University, U.K. Formulating Usability 11.15 K. Systa Tampere University, Finland. Specifying User Interfaces in DisCo 12.00 L.M.F Carneiro, D.D. Cowan, and C.J.P. Lucena. University of Waterloo, Canada. ADVcharts: a Graphical Specification for Multi-Modal Interactive Systems - Abstract Data Views in Perspective 12.45 ** Lunch ** 13.45 F. Paterno CNUCE - CNR, Italy. A Formal Approach To The Evaluation Of Interactive Systems 14.30 B. De Carolis and F. de Rosis. University of Bari, Italy. Modelling Adaptive Interaction in OPADE Using Petri Nets. 15.15 B. Fields, M.D. Harrison and P.C. Wright British Aerospace and University of York, U.K. From Natural Language Requirements To Agent-Based Specification: An Aircraft Warnings Case Study 16.00 ** Tea ** Workshop organisers: Dr. C.W. Johnson and Prof. M.D. Harrison, The HCI Group, The Department of Computer Science, The University of York, York, YO1 5DD. E-mail: johnson@minster.york.ac.uk, Phone: 0904 433376 %%%%%%%%%%%%%%%%%% Formulating Usability H. Thimbleby Stirling University, U.K. hwt@cs.stir.ac.uk Usability is empirical, and often highly context-specific, but it would be useful for designers to have general estimates of usability from interactive system specifications alone. We discuss how this problem may be approached, and we give examples. We also discuss the justification for the approach, since it is unusual to measure usability without involving users. The explicit mathematical content of this paper has been deliberately kept to a minimum. User interfaces are getting more and more features, but there are very few systematic ways to make them any better, or even to know how good or bad they are. It is almost impossible to compare designs: first, because usability measures may not relate to identifiable design features; second, because one generally wants to compare two or more designs to spare the effort of implementing all of them - or the embarrassment of implementing the `wrong' one! The motivation of the present work is to make a contribution to user interface design, specifically to discuss ways of measuring usability from design, from specifications rather than implementations. The aim is to show that solid results can be obtained with very simple and general assumptions, and to illustrate certain usability criteria that can be established in the design cycle. Ideally, of course, user interfaces should be empirically evaluated and then improved, but in practice many products are designed and then fobbed off to users, with little opportunity for improvements. It is therefore crucial to have design support for usability measurement. A tool supporting the sort of analysis promoted here is discussed in a companion paper with a more practical emphasis (Thimbleby, 1993); related work includes (Thimbleby, 1991; Thimbleby and Witten, 1993). References Thimbleby, H. (1991). Formal Methods with no Psychology, IEE Colloquium on Theory in Human-Computer Interaction, IEE Publication No. 1991/92, pp.6/1-6/6. Thimbleby, H. (1993). Combining Systems And Manuals, Proceedings of the BCS HCI Conference, in press. Thimbleby, H and Witten, I. (1993). User Modelling as Machine Identification: New Methods for HCI. In H.R. Hartson and D. Hix (eds.) Advances in Human-Computer Interaction IV, 58-86. %%%%%%%%%%%%%%%%%% Specifying User Interfaces in DisCo Kari Systa Tampere University of Technology, Tampere, Finland. ks@cs.tut.fi DisCo is based on joint actions (Back and Kurki-Suonio, 1988) and it supports specification of reactive and potentially concurrent systems (Jarvinen et al, 1990). The specification is written at an abstract level where implementation details like the type of control and implementation concurrency is not overspecified. DisCo supports object-oriented modeling: DisCo objects always belong to a class that defines the data and state structures of objects. Instead of methods for objects, DisCo has multi-object actions in which the objects may participate. Whenever an action is executed with some objects as participants, the action body may change the states of the participating objects. The enabling of an action is determined by a boolean guard. The guard can therefore be used to restrict the possible participant combinations. In a logical computation an execution of a DisCo specification consists of successive actions; at any moment the next action can be any of the enabled actions. In real time, however, this logical order determines only a partial order, and actions without common participants may execute in parallel. DisCo has two mechanisms for stepwise derivation and reuse of specifications. These mechanisms allow refinement of the specification so that all safety properties are maintained. We have also a tool that can be used for browsing, execution, and animation (Systa, 1991). The execution facility of the tool helps in exposing errors in specifications by means of testing, and the animation helps in understanding the specifications. All critical properties cannot be verified by testing, because of the potentially infinite state space. On the other hand, formal reasoning is expensive and time consuming, and therefore applicable only to the most critical properties. Our goal is to combine testing and experimentation with formal reasoning. The semantics of the DisCo language has been described in terms of temporal logic of actions (TLA) (Lamport, 1990), and TLA can be used as a logic for reasoning in DisCo specifications. We describe a specification of an electronic mail system. The specification proceeds in three superposition steps. The first two steps describe the visible semantics of the system, and the third step specifies the users interface. The specification includes also some example proofs in TLA. References Back, R. J. R., Kurki-Suonio, R. (1988). Distributed cooperation with action systems. ACM Transactions on Programming Languages and Systems 10, 4, October, 513-554. Jarvinen, H-M., Kurki-Suonio, R., Sakkinen, M., Systa, K. (1990). Object-oriented specification of reactive systems. Proc. 12th International Conference on Software Engineering, Nice, France, 1990, IEEE Computer- Society Press, 63-71. Lamport, L. (1990). A Temporal Logic of Actions. Research Report 57, Digital Systems Research Center. Systa, K. (1991). A graphical tool for specification of reactive systems. Proc. Euromicro'91 Workshop on Real-Time Systems. Paris, France. IEEE Computer Society Press, 12-19. %%%%%%%%%%%%%%%%%% ADVcharts: a Graphical Specification for Multi-Modal Interactive Systems - Abstract Data Views in Perspective L.M.F Carneiro, D.D. Cowan, and C.J.P. Lucena. Department of Computer Science, University of Waterloo, Canada. lmfcarne@neumann.uwaterloo.ca This paper introduces a new visual formalism, called ADVcharts, for specifying the behaviour of multi-modal interactive systems as state machines. It combines concepts from Abstract Data Views, with notations from Objectcharts, Statecharts, Petri-nets, and Calculus of Concurrent Systems. ADVcharts are motivated by the need to provide a formal semantics for Abstract Data Views, while serving as a foundation for a future design methodology for multi-modal interactive systems. The analytic capability of ADVcharts is illustrated using several examples. In particular, we show that with ADVcharts we have a clear view of the different ways the system behaves in interacting with various media. This paper concludes by showing how VDM-like specifications can be directly derived from ADVcharts, thus providing the Abstract Data Views concept with both a graphical and textual formalism. %%%%%%%%%%%%%%%%%% A Formal Approach To The Evaluation Of Interactive Systems F. Paterno'. CNUCE-CNR, Pisa, Italy. paterno@vm.cnuce.cnr.it The main work of designers of interactive systems is to decide architectural and interactional solutions for supporting users' tasks. This work can be performed by task decomposition to drive modelling of the corresponding interactive system which has to support the needed interactions. A description of tasks indicates how to fulfill a specific goal without taking into account any particular system to perform them. An interactive system supports a set of accesses to application functionality and data. The possible application semantics define the set of tasks which it is able to support. Designers, in order to choose the better solution for supporting communication between user and application core, have to identify the space of all possible solutions and to provide criteria to select the more suitable for the users' requirements. In this work we want to provide a formal framework for this kind of work. The first aspect to take into account is the role that equivalences can play in this area. Equivalence is an important concept in computer science which has not yet been formally applied in the human-computer interaction field. However, it can be used for many purposes. For example, to precisely specify the space of task-equivalent interactions in order to indicate to designers all the possible choices to evaluate before deciding how to support a task. Formal equivalences can be used to verify behavioural conformance between an interactional description (the sequence of user actions and system feedback) and an architectural description of an Interactive System which is supposed to support the given interactions. The second aspect is to introduce formal criteria for evaluating the users' perception of an interactive system. For this purpose we use properties expressed in Action-Based Temporal Logic (ACTL) which can automatically be checked on LOTOS specifications of dynamic behaviour of user interfaces. The ACTL notation allows us to reason about a system in terms of the actions which it can perform. Thus we have a formal and powerful tool to answer questions such as ``if the user performs this action how will the system react?'' or ``is this the right interaction to fulfill that task?''. Combining these two aspects we obtain an approach which allows us to go towards the definition of a formal framework for verifying the users' perception of interactive systems and usability requirements. %%%%%%%%%%%%%%%%%% Modelling Adaptive Interaction In OPADE By Petri Nets B. De Carolis and F. de Rosis Dipartimento di Informatica, Universita di Bari, Italy. nadja@aos1.ba.infn.it In designing the interface for OPADE, a project aimed at prototyping an intelligent, multilingual computerized drug prescription system, it has been necessary to define and model the dialogue between the interface of the system and its different categories of potential users. OPADE will be used by people having different roles within the drug prescription process, different types and level of knowledge in the domain, different familiarity with computers, and, in addition, they will work in different countries and types of health services. Several aspects of the interaction need to be adapted to the user characteristics: from physical to cognitive ones. Users having different roles have also different access rights. In order to ensure that the dialogue facilities of the system match the communication needs of the users and constraints of the task environments, a dialogue specification method is needed, that allows describing the adaptivity in an expressive way to the medical partners of the project, so that they can cooperate in the design of the interface features and functionalities. We used Object Oriented Analysis and Design in order to specify the objects and functionalities of the OPADE interface. This formalism was not expressive enough. We attempted to couple the object oriented methodology with another formalism that could express the interface state consequent to user actions, that could be understandable for our medical partners, and that could represent all aspects of the adaptation in OPADE. Among the examined formalisms we found out that a particular extension of Petri Nets satisfied these requirements. The places in the Petri Net correspond to the interface state in a particular moment (i.e., a window and some icons on the screen) and transitions correspond to user actions (i.e., selection of buttons, menu options or icons). Representation of concurrency, sequencing and synchronisation of user actions and interface displays is made explicit by extending the Trellis set of primitive actions. Using colours associated to places and guards associated to transitions of the Petri Net gives us the possibility of representing the interaction for each user of the system. In fact, a colour in OPADE is a first order logic formula whose atoms are of the type: Characteristic(User, Value) , where Characteristic is a predicate which may refer to any user feature and Value may be a variable, a constant or a functional expression on the medical domain knowledge base. Transition guards, which are colour conditions on transitions are used to restrict the access to some parts of the network and to represent alternative paths of dialogue to different categories of users. Analysis of node reachability for each category of user has been used to simulate the interaction with OPADE by each of them and, following suggestions of our medical partners, to revise the dialogue accordingly. References De Carolis, B. and de Rosis, F. (1993). Specifying User Adapted Man-Machine Dialogues By Extended Petri Nets. To be presented at the Workshop On Computer Supported Cooperative Work, June. Furuta, R. and Stott, P.D. (1989). Petri Net Based Hypertext, Document Structure With Browsing Semantics. ACM Transactions On Information Systems, 7, 1. %%%%%%%%%%%%%%%%%% >From Natural Language Requirements To Agent-Based Specification: An Aircraft Warnings Case Study B. Fields, M. Harrison and P. Wright British Aerospace and University of York, U.K. bob@minster.york.ac.uk Previous work has demonstrated how interactive systems can be modelled formally using an agent specification language (Duke and Harrison, 1992). The use of formal modelling techniques has the advantage of bringing a greater degree of precision and clarity to the design of interactive systems, but the approach it is not without its problems (Monk, Curry and Wright, 1993). One issue that needs to be addressed is how system modelling can be integrated with the less formal requirements specification techniques typically found in industry. In this paper we wish to explore one way of bridging the gap between the natural language requirements definition and formal system model via an agent-based structured description. The approach takes as its starting point a natural language definition of properties of the system and the interactive environment in which it is embedded. Using this information a set of agents which make up the system and its environment are identified. Once the agents have been identified, agent frames are used to capture expressions in the natural language document relevant to each agent. The interactions between agents are then analysed. Natural language expressions relevant to these interactions are captured as requirements on the communication between agents. Once requirements have been structured in this way, the informal statements of requirements captured in the agent frames are replaced by formal statements written in Partial Order Logic ; a variant of temporal logic capable of modelling behaviour over time and concurrent user events. The system model formally captures the essential features of a class of potential design solutions. A refinement of the system model, or formal specification, is then produced, narrowing the scope to a particular design solution which serves as input to the implementation or rapid prototyping phase. The structures and notations are illustrated by an example from an aircraft alarms and warnings system. An informal description is taken through the agent structuring process and a system model is presented which describes a whole class of failure-monitoring systems by defining their observable behaviour in failure situations. While the informal specification describes of the way in which a failure occurs and is detected, the system model is a formal definition of the interaction between these failures and the temporal constraints on the way the resultant warnings are presented to the pilot. References Duke, D. and Harrison, M. (1992). Abstract Models for Interaction Objects, Report, Dependable Computing Systems Center, Univ. of York. Monk, A., Curry, M. and Wright, P. (1993). Why industry doesn't use the wonderful notations we researchers have given them to reason about their designs. In D. Gilmore, ed., `User-centred requirements for software engineering', Springer-Verlag (in press).