EG 2009 Eurographics 2009: 30th of March to the 3rd of April 2009 in Munich (Germany). Previous Event: Eurographics 2008

@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",
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",
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",
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",
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",
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
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
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",
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",
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
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",
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
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",
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",
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",
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}
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",
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",
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",
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",
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",
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
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
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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
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",
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",
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",
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",
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",
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",
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",
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",
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
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
{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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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.
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",
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",
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",
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",
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",
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
editor =       "Bodart, F. and Vanderdonckt, J.",
booktitle =    "Design, Specification and Verification of Interactive Systems '96",
series =       "Eurographics",
pages =        "188--206",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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
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",
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",
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
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",
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",
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",
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
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",
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",
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",
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",
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",
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",
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",
at both semantic and presentation levels",
abstract =     "This paper presents an approach to interactive system design known
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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
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",
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",
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",
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",
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
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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",
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
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
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",
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
editor =       "Duke, D.J. and A. Puerta",
booktitle =    "Design, Specification and Verification of Interactive Systems '99",
series =       "Eurographics",
pages =        "100--116",
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",
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",
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",
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",
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",
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.
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
editor =       "Duke, D.J. and A. Puerta",
booktitle =    "Design, Specification and Verification of Interactive Systems '99",
series =       "Eurographics",
pages =        "205--224",
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",
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",
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",
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",
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",
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",
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",
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",
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",
publisher =    "Springer-Verlag",
year =         "1999"
}

------=_NextPart_000_0039_01C006AA.2