Présentateur : Andrew Hussey,
Date : Vendredi 1 octobre 99, 14h
Lieu : CENA, Salle de conférences Contact :
Philippe Palanque
Sujet : Andrew Hussey a appliqué une technique de
spécification formelle (Object-Z) au domaine du controle aérien et a plus
particulièrement travaillé sur l'application des technique d'analyse
de risque (HAZOP) et de Object-Z au contrôle en-route utilisant la
technologie data-link (Druides plus précisément).
Thesis Abstract for Andrew Hussey Formal methods are increasingly accepted for developing software
systems, however their particular application to user-interface
development is less common. In this thesis, we demonstrate the utility
of formal object oriented techniques for specifying, designing and
implementing user-interfaces.
The specification of a user-interface describes user-perceivable
operations and information structures for an interactive system in
an implementation independent way. Operations of a user-interface
specification define elementary tasks. User-interfaces can be
modelled as a system of communicating agents where some agents are
presented to users. An agent and its presentation together define
an interactor. Defining the presentation of interactors is a design
concern. Interactor-based user-interface specifications define an
architecture for a corresponding system implementation. Widgets are common
re-usable interactors for which the presentation is usually well defined.
Definitions of widgets may be stored in a library. We illustrate the
characteristics of notations for interactor based specification using
the Object-Z language and demonstrate re-use of interactors from a
widget library.
Formal methods enable a "model-based" approach to be taken to the
development of user-interface designs. A specification in terms of
widgets is derived from an abstract interactor-based specification. A
corresponding user-interface design is usually easily identified
from a widget-based specification. Derivation of such a widget-based
specification from an abstract specification corresponds to a "task
transformation" (i.e., the abstract and widget-based specifications
enable the same tasks to be performed, although the operations involved
may differ). Task transformation defines a compatibility relation between
user-interface specifications. We define several task transformations
for user-interface specifications and give "specification patterns"
to assist incrementally transforming an abstract user-interface
specification to an equivalent specification in terms of widgets. We
demonstrate transformation of user-interface specifications by reference
to a case study.
Information about Andrew Hussey Andrew Hussey is a Research Officer at the Software Verification Research Centre (SVRC) of the University of Queensland (Australia).
The Software Verification Research Centre (SVRC) is a Special Research
Centre of the Australian Research Council (ARC), established in January
1991, within what was then the Department of Computer Science, now the
Department of Computer Science and Electrical Engineering.
Andrew Hussey graduated from The University of Queensland in 1988
with a Bachelor of Arts majoring in Psychology and in 1993 with Law
(Hons.). He completed a Bachelor of Science (Hons.) in 1994, before
becoming an SVRC PhD student supervised by David Carrington. His PhD was
on methods for developing graphical user-interfaces from formal system
specifications and was awarded in February 1999.
Andrew's current role with the SVRC is a balance of research
and technology transfer. Andrew's technology transfer role involves
evaluation of the safety case for the Active Missile Decoy system
(Nulka) and contribution to the Software Acquisition Reform project. In
his research role, Andrew is currently working on methods for the
safety analysis of human-computer interfaces. His overall research
interests include architectures for interactive systems, object-oriented
software engineering methods, patterns, safety and design methods for
human-computer interfaces.
