@InProceedings{Foley:is-94-3, crossref = "eg-is94-proceedings", author = "Foley, J.D. and P. Sukaviriya", title = "History, Results, and Bibliography of the User Interface Design Environment ({UIDE)}, an Early Model-based System for User Interface Design and Implementation", abstract = "{UIDE}, the {U}ser {I}nterface {D}evelopment {E}nvironment, was conceived in 1987 as a next-generation user interface design and implementation tool to embed application semantics into the earlier generation of {U}ser {I}nterface {M}anagement {S}ystems ({UIMS}s), which focused more on the look and feel of an interface. {UIDE} models an application's data objects, actions, and attributes, and the pre- and post- conditions associated with the actions. The model is then used for a variety of design-time and run-time services, such as to: automatically create windows, menus, and control panels; critique the design for consistency and completeness; control execution of the application; enable and disable menu items and other controls and make windows visible and invisible; generate context sensitive animated help, in which a mouse moves on the screen to show the user how to accomplish a task; generate text help explaining why commands are disabled and what must be done to enable them; and support a set of transformations on the model which change certain user interface characteristics in a correctness-preserving way. The model-based approach represented by {UIDE} is considered promising for four reasons. First, the model is specified in a non-procedural fashion at a higher level of abstraction than the code which the model replaces, thus replacing verbose procedural code with terser declarative knowledge. Second, many of the services provided automatically as a consequence of having the {UIDE} model, such as help, would typically have to be added after the application has been constructed. Changes to the application would have to be reflected back into those services. Third, when the model changes, all of the above uses of the model can be changed automatically. Finally, some of the design-time services provided by the model would not otherwise be available at all.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "3--14", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Barnard:is-94-15, crossref = "eg-is94-proceedings", author = "Barnard, P.J. and J. May", title = "Interactions with Advanced Graphical Interfaces and the Deployment of Latent Human Knowledge", abstract = "Advanced graphical interfaces are increasingly dynamic, multimodal and involve multi-threaded dialogues. This paper provides a theoretical perspective that can support an analysis of the issues in their use: the {I}nteracting {C}ognitive {S}ubsystems ({ICS}) framework. This framework is used to examine alternative ways in which information from different data streams can be blended within perception, thought and the control of action. The potential applicability of the core constructs to interface design is considered. The paper concludes by outlining a specific strategy for bringing this form of understanding into closer harmony with the formal methods community in computer science.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "15--49", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Duce:is-94-51, crossref = "eg-is94-proceedings", author = "Duce, D.A.", title = "Users", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "51--55", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Harrison:is-94-57, crossref = "eg-is94-proceedings", author = "Harrison, M.D.", title = "Role of Formalisms", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "57--60", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Sukaviriya:is-94-61, crossref = "eg-is94-proceedings", author = "Sukaviriya, P.", title = "Role of Development Environments", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "61--73", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Bodart:is-94-77, crossref = "eg-is94-proceedings", author = "Bodart, F. and A.-M. Hennebert and J.-M. Leheureux and J. Vanderdonckt", title = "A Model-Based Approach to Presentation: A Continuum from Task Analysis to Prototype", abstract = "This paper presents a complete model-based approach to the building of presentation for a business oriented highly interactive application. This approach is considered complete in the sense that it supports a continuum from task analysis to a first prototype without disruption. The main steps involved in the proposed methodology include a task analysis performed as a hierarchical decomposition of the interactive task into sub-tasks, a specification of the functional requirements and its integration with task analysis results, a writing of an activity chaining graph wich graphically depicts the information and function flow within the task, the selection of an interaction style, the definition of presentation units, the selection of abstract interaction objects, their transformation into concrete objects to be placed before generating a first prototype. The described methodology not only consists of the definition of these steps, but also shows how computer-aided tools can automatically generate the presentation of such an interface.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "77--94", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Bruin:is-94-95, crossref = "eg-is94-proceedings", author = "de~Bruin, H. and P. Bouwman and J. van~den~Bos", title = "Modeling and Analyzing Human-Computer Dialogues with Protocols", abstract = "A new object-oriented model for modeling and analyzing human-computer dialogues is presented. In this model, dialogues are distributed over a number of objects all running in parallel, and each object maintains the state of a sub-dialogue. The dialogue model is based on only a few concepts: autonomous concurrent objects, communicating with each other via message passing, and the behaviour of an object is recursively defined in terms of protocols. Protocols, a concept derived from the concurrent programming language {P}rotocol, describe the interaction patterns with an object using an augmented regular expression notation. This dialogue model is targeted to concurrent multi-threaded event-driven dialogues. In addition, dialogues can be quite naturally visualized and interactively specified using graphical direct manipulation techniques.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "95--116", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Hurley:is-94-117, crossref = "eg-is94-proceedings", author = "Hurley, W.D.", title = "Bridging the Gap from Conceptual Design to Software Design", abstract = "Designers need a bridge across the gap from conceptual design of the interactive system they want to build to software design of the system that will be built. A suitable framework for such a bridge would be a representation scheme that unifies design information from disparate conceptual spaces and supports automatic determination of software design. This paper presents a representation scheme that explicitly represents conceptual designs of user interface, functional core, and the internal dialogue between them. In particular, it makes precise distinctions among a wide variety of possible concept structures. These distinctions have direct implications for software design. A detailed example demonstrates an automated capability to deduce aspects of software design, including correspondence and control requirements, software construction, and communication mechanisms.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "117--127", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Luo:is-94-129, crossref = "eg-is94-proceedings", author = "Luo, P.", title = "A Human-Computer Collaboration Paradigm for Bridging Design Conceptualization and Implementation", abstract = "In this paper, we describe a human-computer collaborative environment called {MIDAS} that defines a new division of labour between human designers and computers. The environment leverages the strengths of both collaborative parties, while compensating for their weaknesses and smoothing the transition from higher level design abstraction to lower level design activities and implementation. The environment has the following tangible features: (a) it lets designers explicitly express their conceptual design intentions and helps them map the high-level intentions into interface implementations; (b) it lets human designers control design decisions and handles a pyramid of details for them during design; and (c) it provides flexible work and control flow for opportunistic design.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "129--147", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Paterno:is-94-149, crossref = "eg-is94-proceedings", author = "Patern\'{o}, F. and A. Leonardi and S. Pangoli", title = "A Tool-Supported Approach for the Refinement of Interactive Systems", abstract = "In this paper we present an approach to support developers in the refinement of specifications of interactive systems. We begin with a formal specification of user tasks. We then obtain an architectural description of the corresponding interactive system in terms of the composition of interaction objects, and finally we generate the prototype of the user interface. We describe the first results in the development of a tool for supporting designers through these phases by using graphical representations and automatic translation among different types of descriptions.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "149--159", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Schreiber:is-94-161, crossref = "eg-is94-proceedings", author = "Schreiber, S.", title = "The {BOSS} System: Coupling Visual Programming with Model Based Interface Design", abstract = "Due to the limitations of {WYSIWYG} {U}ser {I}nterface {B}uilders and {U}ser {I}nterface {M}anagement {S}ystems model based user interface construction tools gain rising research interest. The paper describes the {BOSS} system, a model based tool which employs an encompassing specification model ({HIT}, {H}ierarchical {I}nterface graph {T}emplates) for setting up all parts of the model of an interactive application (application interface, user interaction task space, presentation design rules) in a declarative, designer oriented manner. {BOSS} offers an integrated development environment in which specifications are elaborated in a graphical, visual-programming-like fashion. Through a refinement component a specification can be transformed according to high-level design goals. From a refined specification {BOSS} generates automatically user interfaces using modified techniques from compiler construction.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "161--179", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Sukaviriya:is-94-181, crossref = "eg-is94-proceedings", author = "Sukaviriya, P. and J. Muthukumarasamy and M. Frank and J.D. Foley", title = "A Model-Based User Interface Architecture: Enhancing a Runtime Environment with Declarative Knowledge", abstract = "A model-based user interface environment refers to an interface design and execution environment which utilizes declarative semantic knowledge about application interfaces. We capture in the \textit{application model} tasks which will be performed by users, their operational constraints, and objects on which these tasks operate. We capture in the \textit{interface model} interface components, application-independent interface tasks, and operational constraints on these tasks. Mapping from the application to the interface model serves as a means to constructan interface to an application. Modeling components in the interface model are coupled with executable components, thereby forming working interfaces. They also support intelligent behaviour such as partially automatic control sequencing, automatic generation of textual and animated help, and recordings of statistical and chronological command usage history. The modeling components in {UIDE} are task-oriented. Specifying an interface through these components not only eliminates the low-level programming from the interface creation process, but also makes the design process centred around user tasks.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "181--197", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Harmelen:is-94-199, crossref = "eg-is94-proceedings", author = "van~Harmelen, M.", title = "Object-Oriented Modelling and Specification for User Inteface Design", abstract = "Specification using object-oriented modelling is a useful technique for user interface design when it is placed in an appropriate methodological context. While designing a user interface, a designer can use object-oriented models to record, refer to and communicate user interface design information, namely, abstractions describing application domains, computer systems and their interactive components. This paper describes (a) the rationale for modelling; (b) a user interface design methodology, \textsf{Idiom}, which integrates modelling activities with other more traditional user interface design activities; (c) a notation for object-oriented modelling which includes the ability to append formal or informal descriptive properties to a model; (d) a brief example illustrating the kinds of model that are constructed during user interface design; and, (e) a discussion of experience with modelling in \textsf{Idiom}.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "199--231", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Bernsen:is-94-235, crossref = "eg-is94-proceedings", author = "Bernsen, N.O.", title = "Why are Analogue Graphics and Natural Language Both Needed in {HCI}?", abstract = "The combined use of graphics and analogue graphics for the expression of information probably is as old as language itself. The paper addresses the question why we need both the expressions of natural language and analogue graphics for the representation of information. It is argued that analogue graphics and natural language have the complementary expressive virtues of specificity and focus, respectively. Their corresponding lack of focus and specificity, respectively, explain why (a) both have developed a number of mechanisms for coping with these deficiencies and (b) why their combination may often have superior expressive power. Since specificity follows from the analogue character of analogue graphics rather than from their graphic character, analogue sound and touch representations are analysed to explore whether results from the analysis of analogue graphics and their complementarity with natural language can be transferred to other analogue modalities of expression. The paper exemplifies the comparatively new field of Modality Theory.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "235--251", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Fields:is-94-253, crossref = "eg-is94-proceedings", author = "Fields, R. and M.D. Harrison and P.C. Wright", title = "Modelling Interactive Systems and Providing task Relevant Information", abstract = "This paper presents an approach to the specification of interactive systems which supports reasoning about properties that emerge from the interaction between a system and a user. In particular, properties about the relationship between the information presented by the system and that required by the user in order to perform some task are studied. This gives rise to requirements being placed on the user's memory for the effective use of the system which can be employed to compare different design choices. The techniques and notations are illustrated with a simple example from the domain of desktop office systems.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "253--266", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Harrison:is-94-267, crossref = "eg-is94-proceedings", author = "Harrison, M.D. and A.E. Blandford and P.J. Barnard", title = "The Requirements Engineering of User Freedom", abstract = "", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "267--277", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Hartson:is-94-279, crossref = "eg-is94-proceedings", author = "Hartson, H.R. and K.A. Mayo", title = "A Framework for Precise, Reusable Task Abstractions", abstract = "Current methods for abstraction of task descriptions within the behavioural view are ad hoc, leading to imprecision, inconsistency, and ambiguity in task- and user-centered interface design representations. However, as interaction designers communicate with software designers and implementers, precise and consistent design representations are crucial. Our experience with the {U}ser {A}ction {N}otation ({UAN}) reveals the most difficulty in lower levels of abstraction, those levels just above the articulatory level of task description. This level is crucial in interface design because it is the level at wich user actions are used to manipulate interface artifacts, or widgets. Even cases believed to be simple and well understood, such as the {\tt select} task, are seen to be problematic. We argue for inclusion of semantics in task abstraction. We also argue for guiding lower level abstraction within the task-subtask hierarchy by bringing to bear other kinds of abstraction hierarchies, particularly domain-oriented and taxonomical hierarchies.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "279--297", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Dearden:is-94-301, crossref = "eg-is94-proceedings", author = "Dearden, A.M. and M.D. Harrison", title = "Modelling Interactive Properties for Interactive Case Memories", abstract = "Previous work on formal models for interactive systems has often used text editors and graphics editors as case studies. Consequently the notations developed do not necessarily include all the facilities that may be required in reasoning about other types of interactive system. In this chapter two possible interaction requirements for an interactive knowledge based system ({IKBS}), user-initiated recoverability and user-initiated reachability are considered. A two-level model based on the work of Sufrin and He [18] is used to show how these requirements can be expressed formally using the Z notation. This model is unable to support the structuring of specifications from collections of interacting components. Three specification notations, which can support structured specification, are then compared in terms of their powers to express these interaction requirements. We show that none of the specially designed notations is capable of adequately expressing the interaction requirements of user-initiated reachability and user-initiated recoverability in {ICM}s, although all the notations have been successfully applied to the specification of other types of system.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "301--316", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Dix:is-94-317, crossref = "eg-is94-proceedings", author = "Dix, A.", title = "{LADA} \- A Logic for the Analysis of Distributed Actions", abstract = "This paper presents a formalism, {LADA}, aimed especially at the description of systems and situations which arise during the design and analysis of groupware. We are particularly interested in highly distributed systems and so {LADA} explicitly models entities (people and things) acting at different unconnected locations. It not only describes the behaviour of the computer software, but also the social protocols required for its successful use. Temporal logic formulae which follow the subjective history of people and other entities are used to simplify the expression of some of the complicated properties required of real systems.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "317--332", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Duke:is-94-333, crossref = "eg-is94-proceedings", author = "Duke, D.J. and M.D. Harrison", title = "Folding Human Factors into Rigorous Development", abstract = "As part of the {ESPRIT} {B}asic {R}esearch {A}ction '{AMODEUS}-2' we are investigating the role of formal methods in specifying and understanding properties of systems as they relate to usability. This paper summarises a case study in which a formal specification is employed to understand user-significant properties of an interactionally rich audio-visual ({AV}) environment. We show how user-oriented requirements need to be considered both in the initial abstract task-oriented specification and in the subsequent refinement process.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "333--347", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Faconti:is-94-349, crossref = "eg-is94-proceedings", author = "Faconti, G.P. and A. Fornari and N. Zani", title = "Visual Representation of Formal Specification: An Application to Hierarchical Logical Input Devices", abstract = "In this paper we shall describe our experience in the definition of a visual representation for the {LOTOS} specification of {H}ierarchical {L}ogical {I}nput {D}evices. The logical input device model is being used to describe the input functionality of the current generation of graphics standards. An extension of the model has been previously proposed by the authors to take into account the hierarchical structuring of those devices. The model has been formally described and several properties have been investigated by addressing the {LOTOS} notation, an {ISO} standard originally developed for the specification of open distributed systems that comes with a graphical syntax. The complexity of such graphical notation makes its use very hard, especially in the early phases of a system specification. Our approach is to develop a simpler notation that, while keeping the basic concepts, focuses on the description of task (process) interrelation by only taking into account the parallel composition operators and is able to express all the required semantic knowledge. The paper, after the introductory remarks, gives a short overview of {(G-)LOTOS} and of logical input devices. Subsequently, it shows how such devices can be described by means of process-gate network pictures that are elements of a language defined by a graphical grammar. The methodology of operation is described through an example that highlights the advantages of developing a formal specification from drawings.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "349--367", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Limpouch:is-94-369, crossref = "eg-is94-proceedings", author = "Limpouch, A.", title = "Grammar-based Formal Specification for the Object-Oriented User Interface Development", abstract = "Object-oriented programming techniques are considered appropriate for the development of event-driven interactive systems with an object-oriented user interface. Due to the lack of any formalism in object-oriented user interface design and implementation, we utilize our experience in the use of grammar-based notations for the formal specification of user interfaces. This paper proposes a model which combines the {Arch} and {PAC} models with the {B}ypass mechanism and shows their proper application and interpretation in the decomposition of an interactive system during its development. The adoption of attributed layered translation grammars is proposed for the formal description of the agents in this model. The prototype of the {OOGC} {UIMS} system supporting the grammar-based specification of user interfaces is presented in this paper.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "369--382", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Palanque:is-94-383, crossref = "eg-is94-proceedings", author = "Palanque, P. and R. Bastide", title = "Petri Net Based Design of User-Driven Interfaces Using the Cooperative Object Formalism", abstract = "The research work presented here belongs in the domain of formal specification of human-software interaction. More precisely, we are concerned by the applying a formal specification technique in the various stages of the construction of an user-driven application, the kind supported by most of the current {UIMS}. We use the {I}nteractive {C}ooperative {O}bjects ({ICO}) formalism, in which structural (or static) aspects are described in an object-oriented framework and dynamic (or behavioural) aspects are described with high-level Petri-nets. The formalism, a case study and some of its expected benefits are presented here.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "383--400", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Roast:is-94-401, crossref = "eg-is94-proceedings", author = "Roast, C. and M.D. Harrison", title = "User Centred System Modelling Using the Template Model", abstract = "Abstract models of interaction may be used to support the development of interactive systems by providing frameworks in which properties of the proposed interface can be specified and reasoned about without necessarily requiring an implemented artifact. In this paper we illustrate such a model. We introduce extensions that identify and clarify system components that have user significance. These extensions enable system properties of the model to be linked to user requirements that may, for example, have their basis in experiment. These extensions form the basis for the \textit{template model}. The \textit{template model} is used to express usability requirements for a system that may support a user's recognition of its state. Two requirements are descibed, namely \textit{output correctness} and \textit{structural consistency}. \textit{Output correctness} requires that displayed information reflects state accurately and comprehensibly. \textit{Structural consistency} requires that all task relevant changes are \textit{consistently} reflected in system output.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "401--412", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Took:is-94-413, crossref = "eg-is94-proceedings", author = "Took, R.", title = "Understanding Direct Manipulation Interaction Algebraically", abstract = "Attempts to explain human computer interaction in an abstract and generic way have up to now resorted to a functional notation, in which input is identified with the arguments to a function, and output with its result. The semantics of the interaction is expressed in the evaluation of the function itself. This has some drawbacks, in particular the difficulty of expressing the semantic of temporal dependence between input and output events, which is a major characteristic of direct manipulation interaction. This paper presents an alternative algebraic formulation, which captures centrally these {IO} synchronisations and dependencies.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "413--428", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @InProceedings{Torres:is-94-429, crossref = "eg-is94-proceedings", author = "Torres, J.C. and B. Clares", title = "Using an Abstract Model for the Formal Specification of Interactive Graphic Systems", abstract = "Algebraic specification has been widely used for the formal specification of graphic systems. Normally, specification languages use only very simple geometrical concepts as graphical theoretical support, which results in complex specifications. The specification of interactive graphic systems has found a good formal model in the concept of `interactor'. An interactor is an abstraction of an entity in interactive graphics capable of both input and output. Interactors have been formally specified using {CSP}-like languages, but without any graphic abstract conceptual support. In this paper we discuss the integration of a formal abstract model (the graphic object concept), an algebraic specification language and synchronization mechanisms. Binding these concepts allows us to carry out a property oriented description of interactive systems, with a high level of abstraction.", editor = "F. Patern\'{o}", booktitle = "Design, Specification and Verification of Interactive Systems '94", series = "Focus on Computer Graphics", pages = "429--444", address = "Heidelberg", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994" } @Proceedings{eg-is94-proceedings, title = "Design, Specification and Verification of Interactive Systems '94", note = "Proceedings of the Eurographics Workshop in Bocca~di~Magra, Italy, June~8~--~10, 1994", editor = "Patern\'{o}, F.", series = "Focus on Computer Graphics", address = "Heidelberg", publisher = "Springer-Verlag", year = "1995" } @InProceedings{Duce:is-95-1, crossref = "eg-is95-proceedings", author = "Duce, D.A. and D.J. Duke", title = "Interaction, Cognition and Visualization", abstract = "The {S}horter {O}xford {E}nglish {D}ictionary defines the word `visualize' as: \- to form a mental vision, image, picture of; \- to construct a visual image in the mind, and `visualization' as: \- the action, fact or power of visualizing: a picture formed by visualizing. In the {O}xford {E}nglish {D}ictionary (1990) visualization is ``$\ldots$ forming a mental picture of something not visible or present, or of an abstract thing \ldots''. This paper gives the background to the recent upsurge of interest in scientific visualization and describes some of the work to develop a framework for understanding visualization. Some consideration is given to issues of \textit{truthfulness} in visualization both in the relationship between the data set and the display and the mapping from display to cognition. The paper describes some recent work in rule-based visualization and the automatic generation of graphical presentations, and concludes with a brief discussion on recent work that may provide a theoretical basis for understanding the effectiveness and veracity of such approaches.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "1--20", address = "Wien", publisher = "Springer-Verlag Wien New York", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Gaudel:is-95-21, crossref = "eg-is95-proceedings", author = "Gaudel, M.-C.", title = "Formal Specification Techniques for Interactive Systems", abstract = "This paper summarises a survey presentation on formal specification techniques and formal development methods. Currently, there is a significant amount of interest in the application of these methods to the specification, design, validation and verification of interactive systems (see for instance [9, 14] and several papers in these proceedings). This leads to the following questions: are general purpose techniques applicable? Is it better to design a specific formal approach for this kind of system? After a brief survey of the main mature techniques, some examples of techniques specific to some application domains are discussed.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "21--26", address = "Wien", publisher = "Springer-Verlag Wien New York", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Olsen:is-95-27, crossref = "eg-is95-proceedings", author = "Olsen~Jr., D.R.", title = "Interacting with Information", abstract = "In a workshop on formal specifications it is important to look carefully at the purpose of those specifications and to challenge some of their assumptions. This is not to discount the value of a formal approach but rather to expand the range of ideas that should be considered. This paper is not so much a report of research as it is an informal challenge to the community and a sketch of a potential direction of research.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "27--34", address = "Wien", publisher = "Springer-Verlag Wien New York", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Paterno:is-95-35, crossref = "eg-is95-proceedings", author = "Patern\'{o}, F. and M.S. Sciacchitano and J. Lowgren", title = "A User Interface Evaluation Mapping Physical User Actions to Task-Driven Formal Specification", abstract = "This paper describes the first results of a work which aims to join two different levels in order to evaluate user interfaces. The two levels are task specification and user physical actions. To achieve this goal we pass through an intermediate level: the formal specification of the system considered. The approach entails building an interactor-based {LOTOS} formal specification of the system starting from task specification. Then a tool, which we have developed, gathers information from both low and high abstraction levels and evaluates the user interactions. The behaviour and results of this tool are shown. We also present how this tool has been applied to {Map}, a real application used for presenting maps.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "35--53", address = "Wien", publisher = "Springer-Verlag Wien New York", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Duke:is-95-54, crossref = "eg-is95-proceedings", author = "Duke, D.J. and M.D. Harrison", title = "Interaction and Task Requirements", abstract = "Novel interaction techniques required for particular work domains or user communities may interfere with the functional or task-oriented requirements that a system is intended to support. This paper suggests that potential conflicts between these two types of requirements can be identified early in the design process through the use of appropriate specification techniques. Here `appropriate' means both that the structures used to express the specification must be able to represent perceivable elements of the system, and that the process through which the specification is constructed must allow for multi-disciplinary insight into the design problem. This paper explores the relationship between a specification and user requirements in the early stages of the design process of a multi-modal user interface.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "54--75", address = "Wien", publisher = "Springer-Verlag Wien New York", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Moher:is-95-76, crossref = "eg-is95-proceedings", author = "Moher, T.G. and V. Dirda", title = "Revising Mental Models to Accommodate Expectation Failures in Human-Computer Dialogues", abstract = "Faulty mental models of device operation may lead to expectation failure in human-computer dialogues. This paper presents an integrative modeling formalism for representing users and devices, and employs this formalism to describe a two-phase process of \textit{model strengthening} and \textit{model weakening} in response to expectation failure. During weakening, selected components of the mental model are tagged as ``uncertain''. The task plan is re-executed on the weakened mental model, and the mental model is strengthened as particular suspicions are eliminated. The revised mental model may then be used as the basis for the development of an alternative task plan.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "76--92", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Johnson:is-95-93, crossref = "eg-is95-proceedings", author = "Johnson, C.", title = "The Application of {P}etri {N}ets to Represent and Reason About Human Factors Problems during Accident Analyses", abstract = "Accident reports are intended to ensure that failures do not recur. They contain the analysis of many different experts, including human factors and systems engineers. The insights of these investigators are often separated into chapters that reflect the particular concerns and expertise of their authors. Such a separation often makes it difficult for readers to trace the ways in which human and system `failures' combine to create the necessary conditions for an accident. The following paper argues that mathematically based modelling techniques can be used to overcome this problem. It is hypothesised that the application of formal notations can be extended from the domain of systems engineering in order to represent the findings of human factors analyses. In particular, it is argued that {P}etri {N}ets can be used to represent and reason about the concurrent behaviour of multiple operators and their systems. Tool support can be recruited to validate the resulting nets. The sequences of events leading to an accident can be simulated and shown to human factors and systems engineers. This, in turn, may elicit further observations about the causes of an accident. A near collision analysed by the {U.K.} {D}epartment of {T}ransport's {A}ir {A}ccident {I}nvestigation {B}ranch ({AAIB}) is used in order to evaluate this approach.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "93--112", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Gray:is-95-113, crossref = "eg-is95-proceedings", author = "Gray, P.D. and C. Johnson", title = "Requirements for the Next Generation of User Interface Specification Languages", abstract = "Many existing interface specification notations cannot capture the temporal properties that characterise interaction with distributed systems, such as the Internet browsers {M}osaic and {N}etscape. This paper presents a range of formalisms that avoid this limitation. We present a spectrum of approaches that range from the purely textual constructs of branching time logics, through the mixed graphical and textual notation of {E}xtended {U}ser {A}ction {N}otation ({XUAN}) to the fully graphical representation of {P}etri {N}ets. It is concluded that each notation highlights different aspects of the interaction problems that arise when using distributed systems. It is also argued that these notations all suffer from significant usability problems. The paper ends by presenting an agenda for future research into the development of temporal notations for the design of human computer interfaces.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "113--133", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Bramwell:is-95-134, crossref = "eg-is95-proceedings", author = "Bramwell, C. and R.E. Fields and M.D. Harrison", title = "Exploring Design Options Rationally", abstract = "This paper describes a design technique for interactive systems that allows designs to be specified and refined formally, using a notation based on {A}ction {S}ystems. The rationale underlying the choices made by designers is recorded in a style based on the ``{Q}uestions, {O}ptions, {C}riteria'' notation. The means of capturing formal specifications and the reasoning behind design decisions are presented as parts of a uniform framework; a formal account is given of how design options satisfy criteria and how design options can be combined to answer larger design questions.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "134--148", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Dix:is-95-149, crossref = "eg-is95-proceedings", author = "Dix, A.", title = "Moving Between Contexts", abstract = "Any action is performed in a particular context. So what does it mean to do the `same' thing in a different context? There is no simple answer to this question, it depends on the interpretation of the operation and even then may be ambiguous. This is not a purely theoretical problem, but occurs in practical computational problems. This paper examines this issue looking at three different problems: multi-user undo, distributed update and the simultaneous development of a document in multiple formats. In each case, we find formal rules which any sensible translation must obey. We also see that dynamic pointers, a generic specification and implementation concept defined in previous work, can be used to generate default translation rules which suffice in many circumstances. This is because dynamic pointers can themselves be seen as a translation of location information between different contexts", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "149--173", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Bumbulis:is-95-174, crossref = "eg-is95-proceedings", author = "Bumbulis, P. and P.S.C. Alencar and D.D. Cowan and C.J.P. Lucena", title = "Combining Formal Techniques and Prototyping in User Interface Construction and Verification", abstract = "In this paper we investigate a component-based approach to combining formal techniques and prototyping for user interface construction in which a single specification is used for constructing both implementations (prototypes) for experimentation and models for formal reasoning. Using a component-based approach not only allows us to construct realistic prototypes, but also allows us to generate a variety of formal models. Rapid prototyping allows the designs to be tested with end users and modified based on their comments and performance, while formal modeling permits the designer to verify mechanically specific requirements imposed on the user interface such as those found in safety-critical or security-critical applications.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "174--192", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Elwert:is-95-193, crossref = "eg-is95-proceedings", author = "Elwert, T. and E. Schlungbaum", title = "Modelling and Generation of Graphical User Interfaces in the {TADEUS} Approach", abstract = "The use of the {TADEUS}-approach ({TA}sk-based {DE}velopment of {US}er interface software) is the task-oriented and user-centred development of graphical user interfaces ({GUI}). For this reason {TADEUS} is a methodology as well as a supporting environment for {GUI} development. An overview about the {TADEUS} approach is given in this paper. The {TADEUS} {D}ialogue graph, a new specification technique for {GUI}, and the generation of {GUI} based on {D}ialogue graphs are described.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "193--208", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Rauterberg:is-95-209, crossref = "eg-is95-proceedings", author = "Rauterberg, M.", title = "Four Different Measures to Quantify Three Usability Attributes: `Feedback', `Interface Directness' and `Flexibility'", abstract = "One of the main problems of standards (e.g., {DIN} 66234, {ISO} 9241) in the context of usability of software quality is, that they can not be measured in product features. We present a new approach to measure user-interface quality in a quantitative way. First, we developed a concept to describe user-interfaces on a granularity level, that is detailed enough to preserve important interface characteristics, and is general enough to cover most of known interface types. We distinguish between different types of `interaction-points'. With these kinds of interaction-points we an describe several types of interfaces ({CUI}: command, menu, form-filling; {GUI}: desktop, direct manipulation, multimedia, etc.). We carried out two different comparative usability studies to validate out quantitative measures. The results of one other published comparative usability study can be predicted. Results of six different interfaces are presented and discussed.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "209--223", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Bauer:is-95-224, crossref = "eg-is95-proceedings", author = "Bauer, B.", title = "Proving the Correctness of Formal User Interface Specifications", abstract = "Formal grammars, task action grammars and attribute grammars are widely accepted approaches for the specification of dialogues of interactive systems. In this paper we present a formal specification technique \- based on attribute grammars \- coupling dialogue specifications with application and layout specifications. For this specification formalims a proof principle and an analyzing technique is provided and applied to a user interface specification of an {ISDN} telephone. Properties can be shown between the interaction of a user and the behaviour of the system. The used specification technique allows e.g. to show that there are dialogues such that a special action can be performed, e.g. a menu-item can be selected and e.g. that the application has a special state after a distinguished action.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "224--241", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Bernsen:is-95-242, crossref = "eg-is95-proceedings", author = "Bernsen, N.O. and S. Lu", title = "A Software Demonstrator of Modality Theory", abstract = "For some years, the multimodal systems group at the {C}entre for {C}ognitive {S}cience, {R}oskilde {U}niversity, has been working on establishing and implementing the research agenda of modality theory. The research agenda for modality theory is the following [1]: (1) To establish sound conceptual and taxonomic foundations for describing and analysing any particular type of unimodal or multimodal output representation relevant to human-computer interaction ({HCI}); (2) to create a conceptual framework for describing and analysing interactive computer interfaces; (3) to develop a practical methodology for applying the results of steps (1) and (2) above to the problem of information mapping between work/task domains and human-computer interfaces in information systems design. Modality theory thus aims to establish the theoretical and methodological basis for addressing the information mapping problem in its most general form, i.e.: Given any particular class of task domain information which needs to be exchanged between user and system during task performance, identify the set of input/output modalities which consititute an optimal solution to the representation and exchange of that information.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "242--261", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Bodart:is-95-262, crossref = "eg-is95-proceedings", author = "Bodart, F. and A.-M. Hennebert and J.-M. Leheureux and I. Provot and B. Sacr\'{e} and J. Vanderdonckt", title = "Towards a Systematic Building of Software Architecture: The {TRIDENT} Methodological Guide", abstract = "When designers are facing the question how to build an application architecture practically, they often have to consider various arguments and factors coming from different perspectives: decomposition criteria in architecture design, dialog independence in user interface ({UI}) design, methodology to follow in a development team. These factors are not easy to concilate, forcing designers to make trade offs or unbalanced choices. In this paper, we discuss an architecture model, which is part of {TRIDENT} project, that addresses these issues. It consists of a generic architecture model for highly interactive business oriented applications. It is accompanied with a practical task-based methodology for building an architecture that automatically preserves desired criteria. Assumptions made for the architecture model, its content and the semantics of relationships are explained. The systematic approach is exemplified by a complete architecture case throughout the paper. {S}oftware {A}rchitecture {A}nalysis {M}ethod ({SAAM}) is finally applied to prove the benefits of this architecture and to evaluate it with respect to relevant criteria. This paper suggest first steps towards a systematic building of a software architecture.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "262--278", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Green:is-95-279, crossref = "eg-is95-proceedings", author = "Green, M.", title = "The Design of Narrative Virtual Environments", abstract = "The hardware technology for the production of virtual environments ({VE}) has been available for at least five years, but very few software tools have been developed for this new technology. Existing software tools are very low level, forcing the application developer to use programming to produce most of the application code. Many {VE} applications will be developed by non-programmers, who don't have the skill or time to use today's low level tools. The development of high level tools has been hindered by the lack of models and specification techniques for these user interfaces. Since this interaction style is quite new, its not surprising that these models and techniques haven't been developed. Now that we have some experience with the development of {VE} applications, its time to start considering the formal basis of this interaction style. This paper presents our initial attempt at developing a formal model for narrative virtual environments, and the specification techniques that go along with this model. The model and specification techniques that we have developed form the basis for a set of software tools that can be used by non-programmers to produce narrative virtual environments.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "279--293", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Markopoulos:is-95-294, crossref = "eg-is95-proceedings", author = "Markopoulos, P.", title = "On the Expression of Interaction Properties within an Interactor Model", abstract = "This paper introduces a formal approach for the description of interactive systems based on the interactor model of [15,17]. Similarly to that model, it is intended to be used constructively for building specifications of interfaces as compositions of interactors. Changes are brought about to two aspects of the model: firstly, a modularised representation of control information is achieved which supports the independent description of the data transforming behaviour of the interactor and of the temporal constraints imposed on that behaviour. Secondly, distinct representations of `result' and `display' data handled by an interactor are related within a process algebraic framework, allowing the expression of usability related properties of interaction.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "294--310", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Middlemass:is-95-311, crossref = "eg-is95-proceedings", author = "Middlemass, J. and A. Stork and J. Long", title = "Applying a Structured Method for Usability Engineering To Recreational Facilities Booking User Requirements: A Successful Case Study", abstract = "{MUSE}, a structured {M}ethod for {U}sability {E}ngineering, was created to improve the practice of {H}uman-{C}omputer {I}nteraction practitioners, a practice that is primarily one of designing artefacts that fulfil user requirements. This paper offers a case-study application of {MUSE} to a set of recreational facilities booking user requirements to produce an artefact. The paper presents: an overview of {MUSE}; the necessary features of an application; the user requirements; the details of the application; the resulting artefact; an assessment of the artefact with respect to the user requirements; and a comparison of the case-study's user requirements with those in {S}tork, {M}iddlemass and {L}ong (1995). Finally, it is argued that this case-study be considered `successful', where a successful case-study extends the known frontiers of application of {MUSE}.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "311--328", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Took:is-95-329, crossref = "eg-is95-proceedings", author = "Took, R.", title = "A Formal Design for Mutually Composed Multiple Media in Presentations", abstract = "The motivation for this paper is to design a simple but expressive representation for the arbitrary organisation and nesting of text and images in presentations like user interfaces and document browsers. The design defined here achieves this with a single generic hierarchical structure, called a \textit{{TANGLE}}, instantiated with two node types, \textit{{BLOCK}}s and \textit{{SPACE}}s, to carry text and images respectively, and two mappings which represent how text may be \textit{framed} in graphical spaces, and images may be \textit{embedded} in text blocks. In addition, a \textit{projection} function is defined by which visualisations from the structure can be generated. The inclusion of other media types is also discussed.", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "329--341", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Harrison:is-95-342, crossref = "eg-is95-proceedings", author = "Harrison, M.D.", title = "Role of Verification", abstract = "", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "342--344", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Johnson:is-95-345, crossref = "eg-is95-proceedings", author = "Johnson, C.", title = "The Challenge of Time", abstract = "", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "345--357", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Moher:is-95-358, crossref = "eg-is95-proceedings", author = "Moher, T.G.", title = "Working Group Report: User and Task Modeling", abstract = "", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "358--362", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @InProceedings{Pierra:is-95-362, crossref = "eg-is95-proceedings", author = "Pierra, G.", title = "Towards a Taxonomy for Interactive Graphics Systems", abstract = "", editor = "Palanque, P. and R. Bastide", booktitle = "Design, Specification and Verification of Interactive Systems '95", series = "Eurographics", pages = "362--370", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995" } @Proceedings{eg-is95-proceedings, title = "Design, Specification and Verification of Interactive Systems '95", note = "Proceedings of the Eurographics Workshop in Toulouse, France, June~7~--~9, 1995", editor = "Palanque, P. and R. Bastide", series = "Eurographics", address = "Wien", publisher = "Springer-Verlag", year = "1995" } @InProceedings{Szekely:is-96-1, crossref = "eg-is96-proceedings", author = "Szekely, P.", title = "Retrospective and Challenges for Model-Based Interface Development", abstract = "Research on model based user interface development tools is about 10 years old. Many approaches and prototype systems have been investigated in universities and research laboratories around the world. This paper proposes a generic architecture for these tools, reviews the different approaches in light of this architecture, and discusses their progress towards the goals of increasing the quality and reducing the cost of developing interfaces. The paper closes with a discussion of challenges for future model-based development tools.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "1--27", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Keyser:is-96-28, crossref = "eg-is96-proceedings", author = "De~Keyser, V. and D. Javaux", title = "Human Factors in Aeronautics", abstract = "In this paper, we will discuss the human factors that must be taken into account in aeronautics, concentrating on the technological evolution this sector is undergoing and the cognitive demands which are therefore put on pilots. This will oblige us to clearly define the status of human error and to understand its processes, as well as the phenomena of judgment and causal attribution by which it is marked. We will also analyze the the question of how error is corrected within the framework of established technical systems. Finally, the predictability and, therefore, the certification of such technical systems will be questioned.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "28--45", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Charlier:is-96-46, crossref = "eg-is96-proceedings", author = "Le~Charlier, B.", title = "Abstract Interpretation and Application to Interactive System Verification", abstract = "Abstract interpretation is widely known as a methodology for building static analyses of programs and is mainly used for program optimization; it can also be used for verification. The aim of this paper is twofold: Firstly, a survey of the methodology of abstract interpretation is presented; secondly, some favourite formalisms and notations from the interactive system verification area are reviewed at light of abstract interpretation. We argue that systematic use of abstract interpretation in interactive system verification could help improving and unifying current techniques.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "46--72", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Faconti:is-96-73, crossref = "eg-is96-proceedings", author = "Faconti, G.P. and D.J. Duke", title = "Device Models", abstract = "Previous work on characterising the variety of interaction devices has focused either on physical properties of the devices or the range of behaviours that they can invoke. This work sets out a new approach to evaluating the usability of devices, one that accounts for the cognitive resources needed to use the device to perform particular tasks. The framework draws its expressive power from a technique called syndetic modelling that allows the description of both the device and cognitive resources to be captured in a common representation. In this paper syndesis provides a foundation for examining the coordinate spaces and transformations that are needed both by the operator and the computer system in performing tasks with a given device.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "73--91", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Accot:is-96-92, crossref = "eg-is96-proceedings", author = "Accot, J. and S. Chatty and P. Palanque", title = "A Formal Description of Low Level Interaction and its Application to Multimodal Interactive Systems", abstract = "The lack of formal models for describing low-level interaction restricts programmers to interactors provided by toolkits. It impedes the construction of highly interactive systems and the design of new interaction styles , such as multimodal interaction. This article reports on our experience with formalising low-level graphical interaction. We propose primitives for event specification and handling that can be used along with {P}etri nets to model such interactions. We then show how multimodal interactions can be built from monomodal ones by combining those models. This is exemplified by an experimental two-handed graphical editor that has been built using the proposed model.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "92--104", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Ausbourg:is-96-105, crossref = "eg-is96-proceedings", author = "{d'Ausbourg}, B. and G. Durrieu and P. Roche", title = "Deriving a Formal Model of an Interactive System from its {UIL} Description in order to Verify and to Test its Behaviour", abstract = "This paper focuses on verifying and testing the interaction or dialogue between a user and an interactive system, especially in case of safety critical systems. In order to verify that the interface of a system behaves as intended by the user, we based our ongoing research on a compromise by allowing the use of informal (but practical) and formal methods. In fact, a formal description of the user's interests and activities through the {I}nterface seems very hard to produce by common designers. A more realistic attitude consists in deriving a formal model from the description fo the intended interface as it was informally designed. Practically, a tool generates models in the language {L}ustre from a user's {UIL} description and these models are used for verification or test purposes.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "105--122", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Szwillus:is-96-123, crossref = "eg-is96-proceedings", author = "Szwillus, G. and K. Kespohl", title = "Prototyping Device Interfaces with {DSN/2}", abstract = "The specification language {DSN/2} and the corresponding tool {KAP} are presented in this paper. They are designed for prototyping user interfaces of electronical technical devices, such as answering machines, {CD} players, or {VCRs}. The language {DSN/2} is used to specify the control model of the user interface, including sound effects and timing conditions. The tool {KAP} adds a visual component to this abstract specification and allows editing, debugging, and end user testing with the defined model. Using this tool set, the designer of a user interface is enabled to create a realistic looking, sounding, and ``feeling'' model of the system under construction without the need of programming. In practical experience, the system was found suitable for performing user tests on the software model of a {CD} player. The results were verified against user testing on the real device.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "123--140", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Carr:is-96-141, crossref = "eg-is96-proceedings", author = "Carr, D.A.", title = "Toward More Understandable User Interface Specifications", abstract = "Many different methods have been used to specify user interfaces: algebraic specification, grammars, task description languages, transition diagrams with and without extensions, rule-based systems, and by demonstration. However, none of these methods has been widely adopted. Current user interfaces are still built by writing a program, perhaps with the aid of a {UIMS}. There are two principal reasons for this. First, specification languages are difficult to use. Reading a specification and understanding its exact meaning is very difficult. Writing a correct specification is even more difficult. Second, most specification languages are not executable. This means that after the user interface programmer makes the effort to write a specification, the user interface must still be coded. As a consequence, most programmers have little incentive to do a specification. A pilot study into the comprehensibility of specifications is described. The results of this study suggest that user interface specifications are difficult to interpret manually. A possible solution to this problem, specification animation, is also described.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "141--161", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Palanque:is-96-162, crossref = "eg-is96-proceedings", author = "Palanque, P. and F. Patern\'{o} and R. Bastide and Menica Mezzanotte", title = "Towards an Integrated Proposal for {I}nteractive {S}ystems design based on {TLIM} and {ICO}", abstract = "The importance of applying formal methods in the design and development process of {I}nteractive {S}ystems is increasingly recognised. However it is still an open issue the identification of systematic methods able to support designers and developers in specifying and demonstrating properties of user interfaces. {TLIM} and {ICO} are two formal methods which have been used for this purpose with interesting results. They address similar concepts but also have different features which allow us to consider useful their integrated use to obtain synergistic and complementary results. In this paper we show their application to some examples in order to discuss similarities and differences and we outline a proposal for their integrated use.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "162--187", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Johnson:is-96-188, crossref = "eg-is96-proceedings", author = "Johnson, C.", title = "The Evaluation of User Interface Notations", abstract = "Over the last decade a wide range of graphical, tabular and textual notations have been proposed to support the design of human-computer interfaces. These notations are intended to strip away the clutter of implementation details that frequently obscure interaction properties. Unfortunately, relatively little work has been done to evaluate the usability of these notations for `real world' interfaces. We have, therefore, conducted an empirical evaluation of the {U}ser {A}ction {N}otation ({UAN}), {S}tate {T}ransition {N}etworks ({STN}) and temporal logic `in the wild'. By this we mean that our subjects were drawn from realistic samples of users and designers. We also presented our subjects with realistic descriptions of two user interfaces. This avoids a weakness of previous investigations that have used `toy examples'. The results of our investigation show a strong preference amongst our subjects for the use of natural language descriptions. More surprisingly, our results also suggest a link between the frequency of comprehension errors and positive attitude statements towards particular notations. In other words, our subjects made most errors with the notations that they liked the best. This suggests that while graphical notations, suh as state transition networks, have strong intuitive appeal they may also create significant problems for real-world development tasks.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "188--206", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Johnson:is-96-207, crossref = "eg-is96-proceedings", author = "Johnson, C. and P. Gray", title = "Supporting Error-Driven Design", abstract = "This paper argues that two limitations restrict the utility of interface specification languages. Firstly, they provide no means of capturing the cognitive conditions that lead to operator `error'. This makes it difficult to distinguish between the normal behaviour of an expert and the mistakes that often lead to problems for novices. The second weakness is that interface notations cannot easily be used to represent and reason about asynchronous failures. This prevents designers from identifying solutions to failures that could occur at many different points during interaction. These are significant limitations because they reflect a pre-occupation with normative behaviour. Unless we have some means of analysing system failure and operator error then we will continue to have interfaces that are designed to support perfect users in perfect environments.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "207--228", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Dearden:is-96-229, crossref = "eg-is96-proceedings", author = "Dearden, A.M. and M.D. Harrison", title = "Risk Analysis, Impact and Interaction Modelling", abstract = "Operator error has been blamed for many accidents and incidents in safety-critical systems. It is important that human-machine interface ({HMI}) designers are aware of the relationships between their design decisions, operator errors, and the hazards associated with a system. In this paper, we demonstrate how information from risk analysis can be combined with formal specification of the {HMI}, to support designers in exploring these relationships. We use the concept of \textit{interactor} to model the human-machine interface ({HMI}); together with a concept of \textit{impact}, which we define informally as: ``the effect that an action or sequence of actions has on the safe and successful operation of a system''. We show how interactors can be used as design representations for the {HMI} at the earliest stages of design, as well as providing a medium by which risk analysts can inform {HMI} designers about the impact of human errors. To demonstrate the feasibility of this approach, we consider a simple, gas-fired, electricity generating plant as a case study. Our proposed approach is intended to complement, rather than compete with, existing design and analysis methods for the {HMI}. The method achieves this by making risk analysis information available in the early stages of the {HMI} design.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "229--247", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Akoumianakis:is-96-248, crossref = "eg-is96-proceedings", author = "Akoumianakis, D. and A. Savidis and C. Stephanidis", title = "Design assistance for user-adapted interaction", abstract = "This paper discusses current approaches to user interface adaption and describes how some of their shortcomings can be overcome by supporting the articulation of user interface adaptation constituents during the early phases of design and development of a user interface. It is claimed that this type of adaptation support is required to ensure accessibility of a user interface by different user groups with varying abilities, requirements and preferences. Additionally, the paper describes the components of a prototype design environment called {USE-IT} which has been developed to support the automatic derivation of such adaptation decisions so as to ensure that the resulting user interface will be accessible by the target user (group). The tool is part of a novel user interface development platform which integrates design assistance and development support to provide a unifying basis for constructing high quality user interfaces that are accessible by different user groups, including disabled and elderly people.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "248--271", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Torres:is-96-272, crossref = "eg-is96-proceedings", author = "Torres, J.C. and M. Gea and F.L. Gutierrez and M. Cabrera and M. Rodriguez", title = "{GRALPLA}: An Algebraic Specification Language for Interactive Graphic Systems", abstract = "The specification of interactive graphic systems involves the use of formal methods to describe the synchronization restrictions and graphic information. Several proposals have been made trying to join formalisms for the specification of concurrent systems with some methods to describe the graphic component. This paper presents an algebraic specification language which has been designed to specify interactive graphic systems. The language is founded on the use of a mathematical formalism to describe the graphic component, with an extension of algebraic specification language to describe synchronization, using guarded operations. The language is an extension of the previous {Gralpla} language, to which new features have been added to allow the specification of dynamic changes to the graphic representations and processes. A prototyping tool has been defined for the language to generate {C++} prototypes of the specification.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "272--291", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Hyde:is-96-292, crossref = "eg-is96-proceedings", author = "Hyde, J.K. and D.J. Duke", title = "Fusion Engines and Melting Pots", abstract = "Emerging multi-modal technology relies on innovative techniques for managing data, both at the user interface level, and at the internal application level. To assess design alternatives for this class of system, it is desirable to have models that focus attention on the critical features of these systems. Formal methods of software specification are known to provide this abstractive power in many contexts. This paper shows that an established specification technique can be used profitably to model, assess and improve the design of a generic kernel for multi-modal systems.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "292--311", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Moher:is-96-312, crossref = "eg-is96-proceedings", author = "Moher, T.G. and V. Dirda and R. Bastide and P. Palanque", title = "Monolingual, Articulated Modeling of Users, Devices, and Interfaces", abstract = "This paper presents a framework for combining the discrete models of users and devices into a global system model suitable for analysis and simulation. It views a system as a composite of interacting subsystems, and describes how those subsystems must be structured to permit compositions in which responsibility for global behaviour can be appropriately ascribed. The paper presents a human-device example (wrist watch) and develops a range of task and device models. The devices and tasks are modeled by colored {P}etri nets partitioned to cleanly distinguish submodel component visibility and interface affordances. The formality of {P}etri nets allows for axiomatic validation of isolated and interacting subsystems.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "312--329", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Merriam:is-96-330, crossref = "eg-is96-proceedings", author = "Merriam, N.A. and M.D. Harrison", title = "Evaluating the Interfaces of Three Theorem Proving Assistants", abstract = "A first step in systematically engineering better interfaces for theorem proving assistants ({TPA}s) is to assess what has already been achieved in the domain. We examine three {TPA}s employing quite different styles of interaction. We consider the support provided by the interfaces for each of four mechanisms for efficient interactive proof: planning, reuse, reflection and articulation. Common themes are observed, as are strengths and weaknesses of the interfaces and we discuss the general issues, attempting to abstract away from the particular artifacts studied.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "330--346", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Bumbulis:is-96-347, crossref = "eg-is96-proceedings", author = "Bumbulis, P. and P.S.C. Alencar and D.D. Cowan and C.J.P. Lucena", title = "Validating Properties of Component-based Graphical User Interfaces", abstract = "In this paper we describe a validation process for graphical user interfaces based on existing toolkits and higher-order logic as mechanized in the {HOL} system. The underlying approach uses a single specification for constructing both implementations (prototypes) for experimentation and models for formal reasoning. The formal models allow the designer to verify mechanically specific requirements imposed on the user interface such as those found in safety- or security-critical applications. We illustrate our approach with an example that shows how the proof process works for behavioural prototypes that have been expressed in a rule-based fashion.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "347--365", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @InProceedings{Reeves:is-96-366, crossref = "eg-is96-proceedings", author = "Reeves, S.", title = "Specifying and Reasoning about {CSCW}", abstract = "In this paper we introduce a pair of logics which, taken together, can be seen as a frist step towards a formal specification language for {CSCW} systems. We show the development of the logics and give some simple examples of their use. We also make a distinction between the computational part of the system and the people, i.e. we do not follow a simple action and agent analysis. Since people bring knowledge to a system we treat them differently. We also propose the use of situation theory as a way of capturing requirements.", editor = "Bodart, F. and Vanderdonckt, J.", booktitle = "Design, Specification and Verification of Interactive Systems '96", series = "Eurographics", pages = "366--383", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996" } @Proceedings{eg-is96-proceedings, title = "Design, Specification and Verification of Interactive Systems '96", note = "Proceedings of the Eurographics Workshop in Namur, Belgium, June~5~--~7, 1996", editor = "Bodart, F. and Vanderdonckt, J.", series = "Eurographics", address = "Wien", publisher = "Springer-Verlag", year = "1996" } @InProceedings{Hall:is-97-1, crossref = "eg-is97-proceedings", author = "Hall, A.", title = "Do Interactive Systems need Specifications?", abstract = "The obvious advantages of prototyping and incremental development for interactive systems lead some people to believe that specifications of such systems are unnecessary or even harmful. I question whether there really is a conflict between specifications and prototypes. In fact the two schools have more in common than is usually supposed. Both specifications and prototypes can be understood as theories about the system to be developed. Both have important and complementary roles in development.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "1--12", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Coutaz:is-97-13, crossref = "eg-is97-proceedings", author = "Coutaz, J.", title = "{PAC}-ing the Architecture of Your User Interface", abstract = "A number of architectural models, such as {PAC}, are available for the software design of interactive systems. These design abstractions, however, are not always clearly articulated nor do they explicitly exploit the foundational concepts developed recently in main-stream software architecture engineering. Similarly, technical solutions from main-stream software engineering may improve portability and reusability of at the code level while hindering the quality of the resulting user interfaces. This article is an attempt to undertake an explicit bridging effort between software engineering and the specific domain of user interfcae software design using {PAC} as the running example. We present a brief evolution of the architectural models for single-user systems that motivated {PAC}. We then unfold {PAC} into {PAC*} for designing the conceptual architecture of multi-user systems.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "13--27", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Fields:is-97-29, crossref = "eg-is97-proceedings", author = "Fields, R.E. and N.A. Merriam and A.M. Dearden", title = "{DMVIS}: {D}esign, {M}odelling and {V}alidation of {I}nteractive {S}ystems", abstract = "Much of the work reported in the first three {DSVIS} conferences has concentrated on techniques and languages for specifying and developing interactive systems. In this paper, we argue that a change of emphasis may be necessary as the field matures. We argue that real projects, with specific objectives for formal methods are more likely to employ a range of diverse, lightweight modelling techniques. We explore this view by showing how, on one example, several different kinds of analysis can be performed using different models.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "29--44", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Blandford:is-97-45, crossref = "eg-is97-proceedings", author = "Blandford, A. and R.J. Butterworth and J. Good", title = "Users as rational interacting agents: formalising assumptions about cognition and interaction", abstract = "One way of assessing the usability of a computer system is to make reasonable assumptions about users' cognition and to analyse how they can be expected to work with the system, using their knowledge and information from the display to achieve their goals. This is the approach taken in {P}rogrammable {U}ser {M}odelling {A}nalysis, a technique for predictive usability evaluation of interactive systems. The technique is based on the premise that an analyst can gain insight into the usability of a computer system by specifying the knowledge that a user needs to be able to use it and drawing inferences on how that knowledge will guide the user's behaviour. This may be done by observing how a cognitive architecture, ``programmed'' with that knowledge, behaves. An alternative approach is to develop a formal description of the essential features of the cognitive architecture and to use that description to reason about likely user behaviour. In this paper, we present the approach and an outline formal description of the cognitive architecture. The initial description is derived from an existing implementation. We illustrate how the description can be used in reasoning by applying it to the task of setting up call diverting on a mobile phone. Succesful performance of this task involves a combination of planned and responsive behaviour. The process of doing this analysis highlights what assumptions have been made by the designers about the user's knowledge. We discuss limitations of the current formalisation and identify directions for future work.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "45--60", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Sanz:is-97-61, crossref = "eg-is97-proceedings", author = "Sanz, M.F. and E.J. G\'{o}mez", title = "Establishing a link between usability and utility: validation of a task-based dialogue using a semantic prototype", abstract = "Usability is not sufficient condition to procure utility. The tasks performed by the system user, as a member of the organisation, must contribute to reach the business goals, establishing the basis for the system utility; and besides, the system usability depends, among other context variables, on the features of the user's tasks supported by the system. The use of `semantic prototypes' can enable the identification of the work domain to be supported by the system and can also aid the determination of opportunities for change in this work domain and, consequently, in the business process in which it is immersed. After their validation, this prototype could also aid the definition of specific usability goals that can be attained through the subsequent correct designs of user interface syntax and articulation. As a result of our experience we claim that the use of `semantic prototypes' for the design and evaluation of the user interface dialogue at the semantic level provides means to assess the utility of an interactive system n advance as well as to establish the starting point for usability.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "61--76", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Mallon:is-97-77, crossref = "eg-is97-proceedings", author = "Mellon, B. and B. Webb", title = "Evaluating Narrative in Multimedia", abstract = "A need exists within multimedia for a method which evaluates a holistic design as opposed to aspects of a design such as structure or interface style. Narrative is an entity which incorporates structure, content, process and context; a method based on this construct has the potential to evaluate a complete media design. Literature describes good narrative as crucial for good media design and as pivotal in determining the quality of a user's experience. The evaluation method described here employs a working assumption of these premises and then tests them empirically. This paper defines narrative, its origins, dimensions, essential components, and uses. It describes criteria for evaluating narrative within multimedia, identified through a literature survey, an inductive content analysis of specific texts and empirical analysis of commercial multimedia titles. These are broad evaluation criteria, identified as four narrative constructs visible within and directly relevant in interpreting commercial multimedia titles.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "77--92", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Sage:is-97-93, crossref = "eg-is97-proceedings", author = "Sage, M. and C. Johnson", title = "Interactors and {H}aggis: Executable specifications for interactive systems", abstract = "Executable formal specifications, of interactive systems, allow programmers to both reason about their systems, and test them on users. The feedback provided allows an iterative approach to interface design. We argue that new developments in concurrent functional languages make them ideal for executing specifications. To show this, we make use of {H}aggis, a concurrent functional graphical toolkit. We describe the development of a highly interactive game, from specification to execution. We start with an agent based specification, making use of the {CNUCE} {LOTOS} interactor model. This model provides for both modularity and reasoning power. We, however, make use of a {VDM} like specification language to describe the internal state of our interactors, and so overcome some of the problems with {CNUCE} interactors. We then show how this specification can be easily and quickly transformed into executable code, using the {H}aggis system. This application typifies the dynamic, real-time interfaces that many previous prototyping environments do not support.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "93--108", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Campos:is-97-109, crossref = "eg-is97-proceedings", author = "Campos, J.C. and M.D. Harrison", title = "Formally Verifying Interactive Systems: A Review", abstract = "Although some progress has been made in the development of principles to guide the designers of interactive systems, ultimately the only proven method of checking how usable a particular system is must be based on experiment. However, it is also the case that changes that occur at this late stage are very expensive. The need for early design checking increases as software becomes more complex and is designed to serve volume international markets and also as interactions between operators and automation in safety-critical environments becomes more complex. This paper reviews progress in the area of formal verification of interactive systems and proposes a short agenda for further work.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "109--124", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Faconti:is-97-125, crossref = "eg-is97-proceedings", author = "Faconti, G.P. and M. Massink", title = "Investigating the behaviour of {PREMO} Synchronizable Objects", abstract = "{PREMO} stands for {P}resentation {E}nvironment for {M}ultimedia {O}bjects and is a major new standard under development within {ISO/IEC}. It addresses the creation of, presentation of and interaction with all forms of information using single or multiple media. The standard (u.d.) is currently developed using an Object Oriented approach. Such a state based specification, however, does not support conveniently the analysis of the temporal relationships occurring among operations. In this paper we model {PREMO} Synchronizable objects defined in the standard as processes in the standardized process algebra {L}otos. The approach we follow is a new way to obtain a specification in a constraint oriented style and is inspired by the Object Oriented approach. We let methods correspond to actions and values of control variables with processes. Each process consists of actions that are enabled for the value of the control variable that is modelled by the process. This style leads to {B}asic {L}otos specifications that are directly suitable for computer assisted analysis such as model checking and simulation.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "125--141", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Accot:is-97-143, crossref = "eg-is97-proceedings", author = "Accot, J. and S. Chatty and S. Maury and P. Palanque", title = "Formal Transducers: Models of Devices and Building Bricks for the Design of Highly Interactive Systems", abstract = "Producing formal descriptions of low level interaction is necessary to completely capture the behaviour of user interfaces and avoid unexpected behaviour of higher level software layers. We propose a structured approach to formalising low level interaction and scaling up to higher layers, based on the composition of transducers. Every transducer encapsulates the behaviour of a device or software component, consumes and produces events. We describe transducers using a formalism based on {P}etri nets, and show how this transducer-based model can be used to describe simple but realistic applications and analyse unexpected defects in their design. We also identify properties that are meaningful to the application designer and users, and show how they can be formally checked on a transducer-based model of the application.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "143--159", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Hill:is-97-161, crossref = "eg-is97-proceedings", author = "Hill, J.C. and P.C. Wright", title = "From text to {P}etri {N}ets: the difficulties of describing accident scenarios formally", abstract = "Much work has been carried out using {P}etri {N}ets to describe interactions and the design of interactive systems. In this paper we are concerned with the use of {P}etri {N}ets to help describe accident scenarios. The issue here is that {P}etri {N}ets or some other formal notation might help eliminate ambiguities and imprecision that are characteristic of natural language descriptions in accident reports. We present a case study in which an attempt was made to describe a fragment of an aircraft accident report using a {P}etri {N}et description and identify four problems associated with this process. We argue that these problems can be overcome by the use of multiple renderings of the accident data. But this solution has its own problems of how to coordinate information from multiple renderings. A hypertext tool is outlined, which provides support for information coordination across multiple representations.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "161--175", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Savidis:is-97-177, crossref = "eg-is97-proceedings", author = "Savidis, A. and C. Stephanidis and D. Akoumianakis", title = "Unifying Toolkit Programming Layers: a Multi-purpose Toolkit Integration Module", abstract = "Learning to program with interface toolkits requires a considerable amount of time, while programmers familiar with one toolkit require considerable additional training before being able to effectively use another toolkit. Even though virtual toolkits have contributed positively in this context, users of virtual toolkits are not enabled: (i) to locally incorporate a new toolkit, or (ii) to extend or modify the supplied programming layer. A tool has been developed, called {PIM}, through which interface developers may establish the desired programming layers on top of toolkits, with reduced development effort. The {PIM} tool provides: (a) a language for the specification of the desired programming layers for toolkits; (b) a compiler to translate such a specification to a {C++} software library (i.e. generated programming layer); and (c) an asynchronous communication library, called generic toolkit interfacing protocol, for ``connecting'' the generated programming layer with the original target toolkit.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "177--192", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Rodriguez:is-97-193, crossref = "eg-is97-proceedings", author = "Rodr\'{i}guez, F.G. and D.L. Scapin", title = "Editing {MAD*} task descriptions for specifying user interfaces, at both semantic and presentation levels", abstract = "This paper presents an approach to interactive system design known as task-based design. The approach is centered on the task-oriented formalism ({MAD*}), and consists in the translation of a formal task description into an intermediary semantic interface ({SSI}), which can be linked to an actual interface. Various characteristics of the approach are described: the {MAD*} model and notation, the {SSI} model, and the different implementations ({IMAD*}, {ISSI}, and the links with the actual interface). The tools that support the process are then described. The conclusion identifies the limits of the approach, the relationships with similar approaches and further research work.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "193--208", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{markopoulos:is-97-209, crossref = "eg-is97-proceedings", author = "Markopoulos, P. and P. Johnson and J. Rowson", title = "Formal aspects of task based design", abstract = "The paper discusses the formalisation of some intuitions which underlie the task based design of user interfaces. Some aspects of user task knowledge are modelled formally and the user interface is represented using a formal interactor model. A conceptual framework is introduced which relates the two representations and helps formalise their relationship as a conformance relationship. The discussion gives rise to a practical scheme for verifying and testing user interfaces and their specifications with respect to task models.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "209--224", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Schouten:is-97-225, crossref = "eg-is97-proceedings", author = "Breedvelt-Schouten, I.M. and F.D. Patern\'{o} and C.A. Severijns", title = "Reusable Structures in Task Models", abstract = "Task analysis is a well-known approach that has been used to analyse usability of existing applications. Recently there is an increasing interest to apply this type of technique to the design and development of new applications, too. However if user interface designers want to apply task modelling on a larger scale, to industrail size case studies, the possibility of reuse is useful for saving time and effort. In this paper we present an approach for designing resuable structures in task models that allows designers to focus more clearly on the needs of the user and that speeds up the application design.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "225--239", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Diplas:is-97-241, crossref = "eg-is97-proceedings", author = "Diplas, C.N. and A.D. Kameas and P.E. Pintelas", title = "The Interactive Specification Workspace: Specifying and Designing the Interaction Issues of Virtual Reality Training Environments from Within", abstract = "Advances in {V}irtual {R}eality ({VR}) systems, {I}ntelligent {T}utoring {S}ystems ans {A}gent {T}echnology make it possible to design and develop {V}irtual {T}raining {E}nvironments ({VTEs}), where the trainees can immerse themselves and interact directly with the learning domain. This paper presents the {I}nteraction {S}pecification {W}orkbench ({ISW}) architecture for the specification and design of virtual environments for training purposes. {ISW} architecture provides the interaction designer with the capability to specify the training interaction with the virtual environment using the {V}irtual {R}eality {M}ulti {F}low {G}raph ({VR-MFG}) as the underlying interaction specification model. {ISW} implements a design space, where the processes of interaction specification and design of {VTEs} take place inside a three-dimensional virtual environment, the objects of which are tools by themselves. Inside this workspace, the designer can associate the abstract objects (the components of the {VR-MFG}) with ``actual'' ibjects of the target virtual environment (kept in a ``world'' database) and apply a number of agent templates with training capabilities.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "241--256", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Gorgan:is-97-257, crossref = "eg-is97-proceedings", author = "Gorgan, D. and D.A. Duce", title = "The Notion of Trajectory in Graphical User Interfaces", abstract = "The {A}ctive {O}bjects {M}odel ({AOM}) as a model-based user interface development environment is presented. The paper highlights the convenience of the trajectory notion in the description of the structure and functionality of graphical user interfaces. The {AOM} model consists of a set of active agents with private rule based behaviours. Model entities involve topological information which defines the behaviour of active objects, parallel and cooperative evolution of agents, time controlling, event oriented or supervised behaviour, interactive techniques, visual programming constructs, rapid prototyping, and intelligent user interfaces. All model entities may be defined by direct manipulation techniques.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "257--272", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Doherty:is-97-273, crossref = "eg-is97-proceedings", author = "Doherty, G. and M.D. Harrison", title = "A Representational Approach to the Specification of Presentations", abstract = "The principled design approach improves the quality of user interfaces by ensuring the conformance to certain carefully chosen design principles. This involves reasoning about the properties of an interactive system specification. Such specifications usually concentrate on interactive system state and behaviour, and pay little attention to the presentation. We show that arguments about the properties of an interactive system \textbf{cannot} be relied upon without placing requirements on the presentation mapping. We consider in detail these requirements, and the manner in which we can verify their satisfaction. Taking this approach, we can prove that a representation is valid with respect to a given property, and thus extend out reasoning into the perceptual domain of the presentation.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "273--290", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Butterworth:is-97-291, crossref = "eg-is97-proceedings", author = "Butterworth, R.J. and D.J. Cooke", title = "On biasing behaviour to the optimal", abstract = "A formal framework for synthesizing interactive systems is outlined. A distinction is made between the functional `behaviour' of a system, which is a description of everything that the user is permitted to do, and the `use' of a system, whcih is what the user is likely to do. A way for capturing the use requirements of a system in terms of how `good' is a given use is proposed and discussed as well as a way of describing interface specifications and terms of \textit{what} user interfaces do rather than \textit{how} they do it. The two aspects are related so that an analyst can judge whether changes in the interface model cause required improvements in the use of the system. Some of the implications of this approach are discusseed and a comparison is made to other formal approaches in {HCI}.", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "291--306", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @InProceedings{Fields:is-97-307, crossref = "eg-is97-proceedings", author = "Fields, R.E. and N.A. Merriam", title = "Modelling in Action", abstract = "", editor = "Harrison, M.D. and J.C. Torres", booktitle = "Design, Specification and Verification of Interactive Systems '97", series = "Eurographics", pages = "307--320", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997" } @Proceedings{eg-is97-proceedings, title = "Design, Specification and Verification of Interactive Systems '97", note = "Proceedings of the Eurographics Workshop in Granada, Spain, June~4~--~6, 1997", editor = "Harrison, M.D. and J.C. Torres", series = "Eurographics", address = "Wien", publisher = "Springer-Verlag", year = "1997" } @InProceedings{Olsen:is-98-1, crossref = "eg-is98-proceedings", author = "Olsen~Jr, D.", title = "Interacting in Chaos", abstract = "In considering which research problems to work on next, one must considec the key uses for future computing technology. To such roles are the support of interpersonal communication and the management, analysis and synthesis of massive amounts of information. When one considers the Macintosh and the impact it has had on computing it is important to understand that it was fundamentally not a computing engine but a communications device. The medium for communication was paper rather than electronic but the Mac was and is all about creating paper artifacts for communication among people. Even today when one examines a software catalog for Windows or the Mac, more than 90% of the software offered is focused on internet or paper-based communications. There is very little that computes or calculates in the classical sense. Personal computers as information engines are a rather more recent phenomenon. The first personal computers had no network and very little disk space. The advent of the internet has radically changed the role of the pecsonal computer as an information management device. The information management approaches that worked for centralized mainframes are not appropriate for personal internet computing. The personal computer environment was not designed for mass information management. These issues must be rethought. Before addressing the information and communication problems, we must first consider the key forces that will shape computing for the next ten years. These forces fall into three broad categories 1) exponential growth in digital technology, 2) market driven diversity, and 3) limited human capacity. The exponential growth in processor power, memory capacity, network bandwidth and the shear size of the internet a key story of the late 20th century: Such exponential growth will continue through the next and cannot be ignored when developing interactive technology for the future. We must work on problems which will still have relevance in an era when every individual has an order of magnitude more computing intecacting with several orders of magnitude more information resources. We must also consider the fact that diversity rather than uniformity will rule computing. There is no way that top-down uniformity will solve any of the key problems that face us. In the face of this explosive growth in technology and diversity, human capacity to absorb it all will not change. Human capacity is the limiting factor and technologies that leverage those capacities are the key to the future.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "1--8", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{McCarthy:is-98-9, crossref = "eg-is98-proceedings", author = "McCarthy, J.C.", title = "The Viability of Modelling Socially Organised Activity", abstract = "Research into socially organised activity provides insights which should not be ignored by interactive system designers. At the same time, the emergence of social context as a salient factor in the design and use of information technology poses problems for the activity of modelling in design. By highlighting the informal, tacit, contingent, and relational aspects of technology use, it raises issues which test the technical scope and practical value of model making. In this paper, attempts to use activity based insights in design are reviewed and their implications for the relationship between model and activity are considered.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "9--23", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Butler:is-98-24, crossref = "eg-is98-proceedings", author = "Butler, K. and C. Esposito and R. Hebron", title = "Deriving Business Object Definitions from User Work Process Models", abstract = "When software is developed to support user work processes ({WPs}) it's purpose is to improve their quality by making them faster, cheaper, more accurate, reducing variance, etc. But across industry this purpose has not yet been met in any conspicuous manner for information workers. There is an industry-wide need to improve internal processes continuously, and in some cases to re-engineer them completely. Often an interactive information system will be the means to implement the desired process. In effect, the information system serves as a major part of the implementation plan to achieve the new process. In current practice, however, the design of the {WP} and the design of the supporting software actually proceed as independent activities. It should not be any surprise that the resulting pieces are often a mismatch, disappointing users, frustrating computing support people, and failing to produce a worthwhile {WP} improvement in return for the computing investment. Early research on software engineering identified a number of breakdowns in joint problem solving as a likely cause of difficulties in creating usable applications. Our own analysis shows that a major obstacle to better coordination between the people who are responsible for {WPs} and those who create software lies in the difficulty of translating between {WP} models and software models. Currently, making the connection from {WP} to useful software requirements is slow, unreliable and expensive. Our focus here will be on the tools to make that translation more systematic and reliable, and far less labor intensive.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "24--40", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Fields:is-98-41, crossref = "eg-is98-proceedings", author = "Fields, R.E. and N.A. Merriam", title = "Inference and Information Resources: A Design Case Study", abstract = "Much attention has been paid in {HCI} to techniques for designing systems that conform to the tasks users wish to carry out. It is often the case that such approaches rely on identifying the combinations of commands a user will be expected to issue and information they will need to access, and designing an interface with appropriate temporal behaviour. Many fields of activity, however, are highly information intensive, and the way in which a human-machine cognitive system makes inferences and reasons and makes decisions is far more important than the way it carries out actions. In this paper, therefore, we explore an approach to design that places much more emphasis on the form and strueture of a display than it's temporal properties, and the role it plays in cognitive activity.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "41--56", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{vanWelie:is-98-57, crossref = "eg-is98-proceedings", author = "van Welie, M. and G.C. van~der~Veer and A. Eli{\"e}ns", title = "An Ontology for Task World Models", abstract = "Many different task modeling methods exist. In this paper, we discuss 1) ingredients common to most task models, 2) how task modeling relates to the design of user interfaces, and 3) our proposed ontology for task analysis. We then show our task analysis tool that is based on the ontology. It is our belief that task models should be based on an ontology that describes the relevant concepts and the relationships between them, independently of any used graphical representalions. Such an ontology helps to understand the different task modeling methods and it can also be operationalized for use in tools.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "57--70", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Paterno:is-98-71, crossref = "eg-is98-proceedings", author = "Patern{\`o}, F. and C. Santoro and S. Tahmassebi", title = "Formal Models for Cooperative Tasks: Concepts and an Application for En-Route Air-Traffic Control", abstract = "This paper presents a proposal for specifying task models for cooperative applications that allow designers to describe the relationships between the activities performed by various users involved in cooperative environments. To this end we extend the {ConcurTaskTree} notation so that new information useful for describing complex cooperative applications can be clearly specified. An example of application to describe En-Route Air Traffic Control ({ATC}) is given to illustrate and clarify our approach.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "71--86", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Butterworth:is-98-87, crossref = "eg-is98-proceedings", author = "Butterworth, R.J. and A. Blandford and D.J. Duke", title = "The Role of Formal Proof in Modelling Interactive Behaviour", abstract = "When proving properties of formally described interactive systems, trade-offs have to be made between the simplicity of the model --- which relates to the ease of performing proofs --- and the real-world validity of the model. This issue is particularly important when the proof incorporates properties of user behaviour as well as the device specification. This paper discusses these trade-offs, using a simple model of a web-browsing system as an example. The property we focus on relates to usability: showing whether or not the things a user wants to do are easy to do. As well as adding detail to move from a point where the modelled system is simple but does not satisfy a stated usability property, through a model that satisfies the property but is {`unreasonable'}, to one that is both reasonable and usable, we also move from a {`safety'}-based proof to a {`liveness'}-based proof, arguing that although liveness proofs are generally more difficult to execute, they correspond better to our intuitive understanding of what it means for a system to be usable, and are therefore more valuable.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "87--101", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Markopoulos:is-98-102, crossref = "eg-is98-proceedings", author = "Markopoulos, P. and G. Papatzanis and P. Johnson and J. Rowson", title = "Validating Semi-Formal Specifications of Interactors as Design Representations", abstract = "This paper discusses the nature of research in specifying and verifying interactive systems; it argues that researchers must assess the relevance of the models they propose to the concerns of user interface designers. The paper outlines a semi-formal representation of user interface software and reports a case study which assesses the relevance of the representation to the designer who is interested in the usability of a system. The paper discusses this case study and its findings, and discusses some methodological concerns about the validation of design representations of interactive systems.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "102--116", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Jones:is-98-117, crossref = "eg-is98-proceedings", author = "Jones, S. and J. Sapsford", title = "The Role of Informal Representations in Early Design", abstract = "Early design activities are of critical importance to the success of a system, yet are fraught with difficulty. This paper presents the results of two small-scale studies which investigated the role of informal and semi-formal graphical representations in the early design of interactive systems. We argue that informal graphical representations may have an important role to play in early design in enabling designers to think creatively about possible design solutions. However, we demonstrate that reliance on informal diagrams as the primary means of communicating and recording design decisions is associated with a number of difficulties. We also identify a number of challenges in relation to the post hoc recording of design decisions using semi-focmal notations. We end by discussing the way in which both informal and semi- formal notations may be used to maximum benefit.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "117--133", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Sage:is-98-134, crossref = "eg-is98-proceedings", author = "Sage, M. and C. Johnson", title = "Pragmatic Formal Design: A Case Study in Integrating Formal Methods into the {HCI} Development Cycle", abstract = "Formal modelling, in interactive system design, has received considerably less real use than might have been hoped. Formal methods can be expensive to use, with poor coverage of the design life cycle. In this paper, we suggest a pragmatic approach to formal design. We rely on a range of models that can help at different stages of development. We use as a case study, the design of a multi-user, design rationale editor. In the early stages of our design, we use a range of semi-formal notations, to perform a task analysis. We then develop a prototype in Clock, a high level functional language. >From this, we derive a {LOTOS} specification, which we use to verify that our system satisfies important design requirements. The task analysis helps here, in highlighting these requirements. Throughout we rely on tool support to simplify the process, and so make it cost effective.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "134--154", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Campos:is-98-155, crossref = "eg-is98-proceedings", author = "Campos, J.C. and M.D. Harrison", title = "The Role of Verification in Interactive Systems Design", abstract = "In this paper we argue that using verification in interactive systems development is more than just checking whether the specification of the system has all the cequired properties; and that changing the focus from a global specification into partial, pcoperty oriented, specifications can provide a number of advantages and make verification act as an aid to decision making. We also present a compiler that allows for the verification of interactor specifications to be done in {SMV}, as well as a simple case study where verification is used to inform a design decision.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "155--170", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Bastide:is-98-171, crossref = "eg-is98-proceedings", author = "Bastide, R. and P. Palanque and D.-H. Le and J. Mu{\~n}oz", title = "Integrating Rendering Specifications into a Formalism for the Design of Interactive Systems", abstract = "In interactive systems, the term rendering applies to any form of communication directed from the applicaM-zon towards the users. The present paper deals with the specification of rendering, and its relaM-zonship with the formal specification of the dialogue between application and user. We first present a taxonomy of rendering according to its function in the application. We briefly recall the basics of the {ICO} formalism, which is used for the formal specification of the application. We then present a case study illustrating how various categories of rendering are taken into account in the {ICO} formalism. Lastly, we show how mathematical analysis can be performed on the {ICO} models to verify predictability properties of the interactive system.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "171--190", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Stirewalt:is-98-191, crossref = "eg-is98-proceedings", author = "Stirewalt, K.R.E. and G.D. Abowd", title = "Practical Dialogue Refinement", abstract = "Researchers have suggested viewing interactive system design as the refinement of an abstract user-task model into an object-oriented interaction model. Inherent in this view is a shift in the nature of the behavior being modeled. We explore the manifestations of such a shift by critically analyzing properties of the forms used to represent task and interaction models. The analysis enabled us to uncover four obstacles to dialogue refinement. We believe that if designers cannot systematically address these obstacles, then the task-model refinement process of development will not be practical on any large scale. We then suggest a refinement framework that systematically deals with these obstacles and demonstrate it on a small, but significant example.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "191--205", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Hussey:is-98-206, crossref = "eg-is98-proceedings", author = "Hussey, A. and D. Carrington", title = "Which Widgets? Deriving Implementations from User-Interface Specifications", abstract = "We consider the process of transforming a formal user-interface specification, expressed using an interactor-based notation, to a form expressed in terms of {"widgets"} (common interactors). A set of patterns is provided for transforming user-interface specifications. By defining a user-interface design using widgets, determining the user-interface's presentation is simplified. Such transformation corresponds to redefinition of abstract user tasks at a more concrete level. We illustrate the process by reference to a simple file browser user-interface.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "206--224", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Fischer:is-98-225, crossref = "eg-is98-proceedings", author = "Fischer, M.", title = "A Framework for Generating Spatial Configurations in User Interfaces", abstract = "This paper describes an approach to the problem of designing and implementing visual presentaM-zons in direct-manipulative user interfaces. Such presentations are often corriplex and their construction requires in-depth design knowledge. A fiamework is proposed that includes declarative models and inference mechanisms, aimed to significantly reduce the demands on the interface developer. Models of application characteristics form the input for a generation system which is parameterised by the interface developer. The inferred layout is produced both as a declarative model and executable code, which, integrated with the rest of the application, produces the presentation at application runtime.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "225--241", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{dAusbourg:is-98-242, crossref = "eg-is98-proceedings", author = "d'Ausbourg, B.", title = "Using Model Checking for the Automatic Validation of User Interface Systems", abstract = "This paper describes the prototype of a software environment devised for assisting the formal validation of user interfaces systems ({UIS}). It suggests an approach to include such formal operations in the design process. It explains why the {UIS} can be modelled properly by a dataflow system, how this model can be expressed by using equations of flows in the language Lustre and how techniques of model checking can be used to check properties on it and to generate tests. It describes then how these functions are integrated in a software environment prototype.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "242--260", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Bowman:is-98-261, crossref = "eg-is98-proceedings", author = "Bowman, H. and G.P. Faconti and M. Massink", title = "Specification and Verification of Media Constraints using {UPPAAL}", abstract = "We present the formal specification and verification of a multimedia stream. The stream is described in a timed automata notation. We verify that the stream satisfies certain quality of service properties, in particular, throughput and end-to-end latency. The verification tool used is the real-time model checker {UPPAAL}.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "261--277", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Troetteberg:is-98-278, crossref = "eg-is98-proceedings", author = "Tr{\oe}tteberg, H.", title = "Modelling Direct Manipulation with Referent and Statecharts", abstract = "An approach to modelling mouse gestures in direct manipulation interfaces is presented. The Referent and Statechart languages are used for modelling structure and behaviour, respectively. A gesture is divided into a series of steps, driven by user action and aided by feedback, all modelled as Statechart states. The Referent describes dynamic relations between these states. The states and transitions determine the gesture syntax and the actual relations established and changed during recognition. We discuss how reasoning about these models can support the design of composite gesture recognisers and provide consistency checking and design critique.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "278--292", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @InProceedings{Doherty:is-98-293, crossref = "eg-is98-proceedings", author = "Doherty, G. and M.D. Harrison", title = "Integrating Joint Behaviour and Dialogue Description", abstract = "Agents ace becoming increasingly common as a means of structuring interactive systems, due to the highly complex and concurrent nature of modem systems. The mannec in which interaction between these agents is specified is of fundamental importance, and must pay heed to expressivity and reuse concems. There are also concerns specific to interactive systems, and in particular the need to specify and reason about user-system dialogue. We have shown previously that the standard model of object interaction is inadequate with respect to these concerns, and that the action model performs better with respect to these criteria. In this paper these results are drawn together with approaches previously taken in interactive systems. From this basis a schema calculus with intecleaving semantics is proposed, which better addresses the concems of expressivity and reuse in the interactive systems context.", editor = "Markopoulos, P. and Johnson, P.", booktitle = "Design, Specification and Verification of Interactive Systems '98", series = "Eurographics", pages = "293--308", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998" } @Proceedings{eg-is98-proceedings, title = "Design, Specification and Verification of Interactive Systems '98", note = "Proceedings of the Eurographics Workshop in Abingdon, UK, June~3~--~5, 1998", editor = "Markopoulos, P. and Johnson, P.", series = "Eurographics", address = "Wien", publisher = "Springer-Verlag", year = "1998" } @InProceedings{Srinivasan:is-99-1, crossref = "eg-is99-proceedings", author = "Srinivasan, M.A. and C. Basdogan and C.-H. Ho", title = "Haptic Interactions in the Real and Virtual Worlds", abstract = "In humans or machines, haptics refers to the use of hands for manual sensing and manipulation. Recently, haptic machines that enable the user to touch, feel, and manipulate virtual environments have generated considerable excitement. Synthesizing virtual haptic objects requires an optimal balance between the human haptic ability to sense object properties, computational complexity to render them in real time, and fidelity of the device in delivering the computed mechanical signals. In this paper, we primarily describe the progress made in our ``MIT Touch Lab'' over the past few years concerning the development of haptic machines, the paradigms and algorithms used in the emerging field of ``Computer Haptics'' (analogous to Computer Graphics), and experimental results on human perception and performance in multimodal virtual environments. Several ongoing applications such as the development of a surgical simulator and virtual environments shared by multiple users are also described.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "1--16", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Hollier:is-99-17, crossref = "eg-is99-proceedings", author = "Hollier, M.", title = "Matching Technology to People for Telepresence", abstract = "The first steps towards a multi-media telepresence revolution have already been taken. Ubiquitous network connectivity with variable bandwidth on demand will be available in the near future due to the evolution of Global {IP} networks and fixed mobile convergence, e.g. {UMTS}. In order to efficiently deliver the radical variety of services that will become possible it is necessary to match the delivery technology to the end user's needs. It will be necessary to enable a range of communications tasks with a variety of bandwidths, local processing power, and user requirements. To do so the delivery systems will have to be adaptive and context sensitive. The network, middleware and delivery technology must be optimised using perceptual criteria. These criteria will be in terms of audio/video perception and communications task requirements. Perceptual models are being developed at {BT Labs}. For multi-media systems we require multi-modal models for whih the influence of task is very significant. In order to account for this level of task dependency we are having to develop and evaluate cognitive models. Examples that illustrate the diversity of emerging service propositions and the complexity of the optimisation task they represent include: immersive telepresence environments, desktop video and video-graphic conferencing tools, portable multi-media terminal, and wearables.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "17--17", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Wuthrich:is-99-18, crossref = "eg-is99-proceedings", author = "W{\"{u}}thrich, C.A.", title = "An Analysis and a Model of {3D} Interaction Methods and Devices for Virtual Reality", abstract = "The growing power of computing devices allows the representation of three-dimensional interactive virtual worlds. Interfaces with such a world must profit from our experience in the interaction with the real world. This paper corrects the early taxonomy of interaction devices and actions introduced by Foley for screen based interactive systems by adapting it to real world and to virtual reality systems. Basing on the taxonomy derived, the paper presents a model for a Virtual Reality system based on {S}ystems {T}heory. The model is capable of including both traditional event-based interaction input devices, as well as continuous input devices. It is strongly device oriented, and allows us to model mathematically all currently possible input devices for virtual reality. The model has been used for the implementation of a general input device library serving asan abstraction layer to a virtual reality system.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "18--29", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Massink:is-99-30, crossref = "eg-is99-proceedings", author = "Massink, M. and D.J. Duke and S. Smith", title = "Towards Hybrid Interface Specification for Virtual Environments", abstract = "Many new multimodal interaction techniques have been proposed for interaction in a virtual world. Often these techniques are of a hybrid nature combining continuous interaction, such as gestures and moving video, with discrete interaction, such as pushing buttons to select items. Unfortunately the description of the behavioural aspects of these interaction techniques found in the literature is informal and incomplete. This can make it hard to compare and evaluate their usability. This paper investigates the use of {HyNet} to give concise and precise specifications of hybrid interaction techniques. {HyNet} is an extension of highlevel {P}etri {N}ets developed for specification and verification of hybrid systems, i.e. mathematical models including both continuous and discrete elements.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "30--51", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Roast:is-99-52, crossref = "eg-is99-proceedings", author = "Roast, C. and J. Siddiqi", title = "Contrasting Models for Visualisation (Seeing the wood through the trees)", abstract = "It is widely recognised that design quality is influenced by the perspective adopted by developers. In the case of formal methods such perspectives are frequently offered by identifying and/or developing appropriate models, from which requirements and systems can be expressed and even verified. In addition, to this there is a growing recognition that selecting and employing a model is an activity which is less dependent upon formal adequacy and more dependent upon ease of use. In this paper we examine and assess factors relevant to design quality that are apparent in comparing two alternative modelling approaches. The specific case study used is that of a system for visualising and manipulating a logical tree.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "52--66", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Cabrera:is-99-67, crossref = "eg-is99-proceedings", author = "Cabrera, M. and J.C. Torres and M. Gea", title = "Towards User Interfaces Prototyping from Algebraic Specification", abstract = "This paper describes the use of an algebraic specification language {GRALPLA}, to specify {U}ser {I}nterface. In order to obtain a description at a high level of abstraction, the specification language has been enriched with such concepts as {I}nteractive {O}bjects, and user actions. A description of a prototyping tool based on this language has been given.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "67--83", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Vanderdonckt:is-99-84, crossref = "eg-is99-proceedings", author = "Vanderdonckt, J.", title = "Computer-Aided Design of Menu Bar and Pull-Down Menus for Business Oriented Applications", abstract = "Building a usable menu bar, related pull-down menus and submenus or cascaded menus remains an important design activity in the development of interactive applications, especially in the domain of business oriented ones. To provide some assistance to designers who are responsible for achieving this task, a two-phased design method for a menu bar and related pull-down menus is presented. Based on a entity-relationship model of the final application, a first phase automatically generates an initial menu tree; a second phase enables designers to interactively perform refinement operations on the initial tree to obtain a final menu tree. This tree can be finally exported to a graphical editor for free editing and adaptation. This method covers the selection and the positioning of menu items, a first proposal for mnemonics and accelerators that are intrinsically based of menu design guidelines.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "84--99", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Castells:is-99-100, crossref = "eg-is99-proceedings", author = "Castells, P. and P. Szekely", title = "Presentation Models by Example", abstract = "Interface builders and multi-media authoring tools only support the construction of static displays where the components of the display are known at design time (e.g. buttons, menus). High-level {UIMSs} and automated designers support more sophisticated displays but are not easy to use as they require dealing explicitly with elaborate abstract concepts. This paper describes a {GUI} development environment, {HandsOn}, where complex displays of dynamically changing data can be constructed by direct manipulation. {HandsOn} integrates principles of graphic design, supports constraint-based layout, and has facilities for easily specifying the layout of collections of data. The system incorporates {P}rogramming {B}y {E}xample techniques to relieve the designer from having to deal with abstractions, and relies on a model-based language for the representation of the displays being constructed and as a means to provide information for the tool to reason about.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "100--116", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Markopoulos:is-99-117, crossref = "eg-is99-proceedings", author = "Markopoulos, P. and P. Shrubsole and J. de~Vet", title = "Refinement of the {PAC} Model for the Component-based design and Specification of Television Based Interfaces", abstract = "Componentisation of software promises to deliver cost eficiency that has not been achieved through object orientation [19]. {PAC} [5] is a popular conceptual architecture for structuring user interface software in an object oriented fashion. This paper reports our experience of adapting and refining {PAC} as a component architecture in the context of consumer electronics, and {O}n-{S}creen {D}isplays in particular. The paper describes a structured scheme for the specification of user interface software components, distinguishing `look' and `feel' specific components, and fostering their modular development and reuse.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "117--132", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Urnes:is-99-133, crossref = "eg-is99-proceedings", author = "Urnes, T. and T.C.N. Graham", title = "Flexibly Mapping Synchronous Groupware Architecture to Distributed Implementations", abstract = "Designlevel architectures allow developers to concentrate on the functionality of their groupware application without exposing its detailed implementation as a distributed system. Because they abstract issues of distribution, networking and concurrency control, designlevel architectures can be implemented using a range of distributed implementation architectures. This paper shows how the implementation of groupware applications can be guided by the use of semanticspreserving architectural annotations. This approach leads to a development cycle that involves first developing the functionality of the application in a localarea context, then tuning its performance by setting architecture annotations. The paper concludes with timing results showing that architectural annotations can dramatically improve the performance of groupware applications.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "133--147", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Ausbourg:is-99-148, crossref = "eg-is99-proceedings", author = "{d'Ausbourg}, B. and J. Cazin", title = "Using {TRIO} Specifications to Generate Test Cases for an Interactive System", abstract = "User Interface Systems (UIS) are quite an important part of many current applications involving human endusers. Testing such open reactive systems requires an interaction with the enduser which must be carefully guided so as to avoid inherent nondeterminism and combinatorial problems. In this paper we propose an approach based on a formal expression of UIS expressed in the temporal logic TRIO which uses a process of model generation to produce significant test cases and oracles. Moreover, we show how this approach can be integrated into a general validation and verification process in which the UIS is still informally developed.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "148--166", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Campos:is-99-167, crossref = "eg-is99-proceedings", author = "Campos, J.C. and M.D. Harrison", title = "Using Automated Reasoning in the Design of an Audio-Visual Communication System", abstract = "Formal reasoning about how users and systems interact poses a difficult challenge. Interactive systems design provides a context in which the subjective area of human understanding meets the objectivity of computer systems logic. We present results of a case study in the use of automated reasoning to aid the formal analysis of interactive systems. We show how we can use human-factors issues to generate properties of interest, and how we can use model checking and theorem proving to analyse our specifications against those properties. This is part of ongoing work in the development of a tool to allow the automatic translation of interactor based specifications into {SMV}, and in the analysis of the role which different verification techniques might have during the development of interactive systems.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "167--188", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Paterno:is-99-189, crossref = "eg-is99-proceedings", author = "Patern\'{o}, F. and C. Santoro and B. Fields", title = "Analysing User Deviations in Interactive Safety-Critical Applications", abstract = "Usability and safety problems have often been addressed separately in designing interactive safety-critical applications thus obtaining fragmented results. In this paper we present a method to analyse possible deviations of users in performing their activities in order to elicit safety requirements and to improve design of interactive safety-critical applications. An application of the proposed method to a case study in the {A}ir {T}raffic {C}ontrol domain is discussed.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "189--204", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Jambon:is-99-205, crossref = "eg-is99-proceedings", author = "Jambon, F. and P. Girard and Y. Boisdron", title = "Dialogue Validation from Task Analysis", abstract = "Up today, formal methods have mainly been used to allow designers to \textit{verify} that software conforms to its specification. In this article, we propose a \textit{validation} method and a tool to analyse whether the design actually fulfills the original requirements for the system. The principle of our validation method is to generate the complete set of possible user interaction sequences from the task analysis. Then, this set is injected in the {D}ialogue {C}ontroller {C}omponent of the application. At last, the {D}ialogue {C}ontroller {C}omponent's calls to the {F}unctional {C}ore are intercepted, and compared with the user's goals. Our case study is in the general {C}omputer-{A}ided {D}esign area, in which systems support a huge number of tasks.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "205--224", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Forbrig:is-99-225, crossref = "eg-is99-proceedings", author = "Forbrig, P.", title = "Task- and Object-Oriented Development of Interactive Systems -- How Many Models are Necessary?", abstract = "In the field of model-based development of interactive systems, several approaches have been proposed to integrate task and object knowledge into the development process and its underlying representations. Within the paper different types of models are classified according to their importance for the development process. The relation between existing, envisioned and programming models are discussed and a task driven approach for object-oriented programming is suggested.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "225--237", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Welie:is-99-238, crossref = "eg-is99-proceedings", author = "van~Welie, M. and G.C. van~der~Veer and A. Eli{\"{e}}ns", title = "Usability Properties in Dialogue Model", abstract = "Usability has gained a lot of attention in the design community and it is one of main goals of every design project. Evaluating usability is usually done with end-users after a prototype has been built and there are not many techniques available that allow usability evaluation during the early design phases. Current dialogue modeling techniques generally do not deal with usability aspects, as they are often funcational based models, dealing only with states abd state changes. This paper investigates how usability aspects can be incorporated into dialog models so that usability can be evaluated during the design process without doing usage tests. A set of measurable properties is given which together could give an indication about the usability of the design. This way, some usability aspects can be covered early in the design process without the need for an executable prototype or end-users.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "238--253", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Rowson:is-99-254, crossref = "eg-is99-proceedings", author = "Rowson, J. and P. Johnson and G. White", title = "Cross-Contextual Reference in Human-Computer Interaction", abstract = "", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "254--261", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Gea:is-99-262, crossref = "eg-is99-proceedings", author = "Gea, M. and F.L. Gutierrez and J.C. Torres and N. Padilla and M. Cabrera", title = "Modelisation of Co-operative Work", abstract = "Nowadays, there is an increasing interest in user co-operation and the different ways of accomplishing user tasks. Users share a common scenario simultaneously. In such systems, we must take into account technological aspects as well as human factors. Characteristics involved with users (such as usability and performance) as well as the social and contextual organisation must be studied. By doing so, an abstract model, regarding design and implementation details, allows us to contemplate the efficiency of these properties.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "262--267", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Duke:is-99-268, crossref = "eg-is99-proceedings", author = "Duke, D.J.", title = "Discussion Topics for the {DSV-IS'99} Working Groups", abstract = "As part of the {DSV-IS} workshop, participants are split randomly into working groups. For the 1999 workshop, three groups were organised and were given two design scenarios as a starting point for discussion. Each group was free to work on either or both of the scenarios. A {R}apporteur was appointed for each of the groups, and the following three chapters of these proceedings contain a summary of the points that were raised within the groups. Two scenarios were chosen, one concerned with haptic interaction, the second with telecollaboration. These reflected the theme for the 1999 workshop ``extending the mind by enriching the sense'', and were linked to the research areas of the invited speakers. The purpose of the discussion groups was not to design an interface or artefact, but rather to use the scenarios to generate discussion about the challenges presented to interface design by emerging technologies and trends.", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "268--269", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Smith:is-99-270, crossref = "eg-is99-proceedings", author = "Smith, S.P.", title = "Working Group 1 Report", abstract = "", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "270--275", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{White:is-99-276, crossref = "eg-is99-proceedings", author = "White, G.", title = "Working Group 2 Report", abstract = "", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "276--277", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @InProceedings{Duce:is-99-278, crossref = "eg-is99-proceedings", author = "Duce, D.A.", title = "Working Group 3 Report", abstract = "", editor = "Duke, D.J. and A. Puerta", booktitle = "Design, Specification and Verification of Interactive Systems '99", series = "Eurographics", pages = "278--280", address = "Wien", publisher = "Springer-Verlag", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999" } @Proceedings{eg-is99-proceedings, title = "Design, Specification and Verification of Interactive Systems '99", note = "Proceedings of the Eurographics Workshop in Braga, Portugal, June~2~--~4, 1999", editor = "Duke, D.J. and Puerta, A.", series = "Eurographics", address = "Wien", publisher = "Springer-Verlag", year = "1999" } ------=_NextPart_000_0039_01C006AA.2