This page contains links to formal methods associated with user interface specification in particular and with usability engineering in general, where such general principles apply substantively to user interface issues. Such methods include (but are not limited to) grammars, trees, transition diagrams, statecharts, user-action notation, certain forms of expert reviews, formal usability inspections, and formal languages.
Research in formal methods has been going on for more than twenty years now in various
areas such as mathematical verification, formal specification, transformation,
prototyping, and testing. Recently, several flavors of formal methods have been
gaining industrial acceptance and production quality software tools have begun
emerging. The use of such formal methods in the software engineering
domain has proven difficult on all but the most limited problems. User interfaces
tend toward the more complex end of the software engineering spectrum and, therefore,
successful application of formal methods to user interface specification are quite
impressive. Most of the material presented in the following subsections support that
|Using Formal Methods for User Interface Design||University of York (UK)|
These pages form a short introduction to the use of mathematical specification and
reasoning, or formal methods, in the design of user interfaces.
|Grammars and Formal Languages|
Grammars are primarily rules (e.g., for sequences of actions) which combine with
syntax, vocabulary, and semantics to comprise languages. Stand-alone grammars in
technical contexts often function as sufficient languages for those contexts.
Grammars for textual interfaces (e.g., command line interfaces) are fairly common,
formalized grammars (e.g., a set of linguistic rules for the formulation of command
syntax) for textual interfaces are somewhat less common; formalized grammars for GUIs are
fairly rare...as are formal languages for user interface specification. This
sub-section identifies a sampling of recent research and several commercial and
pre-commercial grammar/formal language products for user interface specification.
|"Formal Design, Verification and Simulation of Multi-Modal Dialogues"||SRI Cambridge|
This paper describes a dialogue management design tool for use in dialogue design as a
component of user-interface design in multi-modal applications. The tool provides: a
formal language (typed feature structures) for describing states and events; a simple rule
formalism for specifying dialogues; an automatic dialogue-property checking module; a
dialogue-simulator for interactive testing of designs. This is a useful source
because it integrates a number of difficult topics (at least to the non-expert) in a
comprehensible fashion. One negative is that the full paper is available only in
|1996 IEEE Symposium on Visual Languages||IEEE|
This is a useful set of submitted abstracts for the cited Symposium. It includes
abstracts of papers on the Visual Algebraic Specification Environment (VASE), the Object
Block Programming Environment (OBPE), the Visual Repository Definition Language (VRDL),
and a number of other more or less formal languages and related technologies for visual
interface specification and implementation.
|Human Computer Interaction Lab||University of Maryland|
Points to results produced from an Advanced Search using the Altavista search engine
with the query parameters: "grammar NEAR 'user interface'". It is a partially
annotated bibliographic listing of publications, some of which are quite germane to the
topic of grammars and formal languages applicable to user interface specification and some
of which are only tangentially related to that topic. Worth at least a scan.
|Grammar development environments||LINGUIST e-mail list|
This link provides summary information about grammar development environments (GDEs) as
teaching tools. The particular aspects addressed include: Information on availability,
hardware/software requirements, range of formalisms supported, extent of customizability,
ease of writing and testing grammars, quality of display of analyses on screen, ease of
debugging grammars, speed and reliability, general user-friendliness, how used in
teaching, and with what kind of students. Useful data and links for practitioners,
handy information for teachers and students.
|DEIMOS Project||GMD FOKUS (Germany)|
Overview of a real-world, application-domain tool: A Grammar Module is
"inserted" into the COMPASS (Composition of Management Applications and
Services) Engine on demand, each provides means to automatically map the graphical
representation of the Management Service into (formal) specifications of the defined
models. The number or types of Grammar Modules are not defined and depend on the target
environment of the management service. However, all the generated specifications together
provide a complete specification of the Management Service. Useful for
practitioners, especially in the network management application domain.
|METAPHOR MIXER||Maxus Systems International|
This link describes an interesting product, based on a visual grammar, that combines
abstract theories and psychological factors in its generic framework--blending
"aspects of parallel, pre-attentive processing (topsight) with serial, attentive
processing (drill-down ability) for enhanced decision-support visualization"--with a
set of application-domain specific (e.g., financial analysis applications) implementations
of the grammar. Interesting information for researchers and possibly useful to
anyone looking to procure a high-end tool for some application.
|The ALEP Project||Commission of the European Communities|
This link describes the Advanced Language Engineering Platform Project, a multinational
European undertaking to create an environment intended to ease and speed up the
transitions from research to laboratory prototype, and from prototype to marketable
product. It is designed as a basic, low-cost, non-proprietary platform for a broad range
of research and technology development activities, related to natural language processing
and machine translation, primarily in the textual interface domain.. Typical users of the
ALEP environment will be either skilled researchers in computational linguistics or teams
of researchers and application designers, who will be provided with a software environment
enabling them to produce linguistic descriptions of different languages, for a number of
NLP or MT application domains.
|Grammars for Analytic Interface Evaluation||University of Portsmouth (UK)|
This link describes techniques which use descriptions of the users view of an
interaction to produce a very detailed view of the interaction. They are expressed in
terms of tasks or grammars. The descriptions are then analyzed to try to
detect problems. The whole process is built on psychological models which can predict the
behavior of users. The design itself is often analyzed in terms of goals and sub-goals and
sub-sub-goals, etc. Some examples of analytic evaluation techniques are the GOMS model (an analysis in terms of Goals, Operators,
Methods and Selection rules); the CLG (Command
Language Grammar); the TAG (Task Action
Grammar); and the keystroke level model.
All of these methods attempt to analyze some representation of the user interface design
in order to predict how the design will perform with real users. Useful for practitioners
and researches; has links to several seminal sources.
|Principles of Visual Programming Systems||University of Pittsburgh|
This link presents a formal specification of iconic systems using generalized
icons. A generalized icon is a dual representation of an object,
written as (Xm,Xi), with a logical part Xm (the meaning), and a physical part Xi (the
image). A formal iconic system consists of a set of such generalized icons and
rules governing their interactions. The iconic system can be seen to be a special
type of picture grammar. The icon grammar rules can also be expressed as commands in an
iconic language. This is a detailed examination of a kind of meta-language, and
continues on to cover a "visual compiler" for that meta-language as well.
Useful to academic researchers and theorists.
|DOCT: Introduction to 3D shape grammars||San Diego Supercomputing Center (SDSC)|
This white paper introduces features found in typical 3D shape grammars. It is intended as a reference used in conjunction with tabular shape grammar summaries such as those for DXF, IGES, RIB, and VRML. At a minimum, a shape grammar must include syntactic elements to describe the geometric form of one or more shapes. Shape grammars often include additional syntax to describe shape position, orientation, size, grouping, shading, texture mapping, lighting, sound, manufacture, animation, and interaction.. This is a remarkably comprehensive yet concise treatment of the topic...detailed, yet usable by the educated lay-person.
|Keystroke Level Model||Communications of the ACM|
A brief application of the Command Language Grammar of Moran . Useful for
practitioners and researchers, especially with respect to testing performance aspects of
keyboard-level user interfaces.
|Trees, Transition Diagrams, and Statecharts|
Menu trees and dialog trees provide simple structures that guide user interface designers and users in the construction and utilization of those interfaces. The primary value in such trees with respect to formal methods in user interface specification derives from the coverage they can provide, which also helps with consistency and completeness. Transition diagrams extend the value of menu and dialog trees by representing the state conditions and options which occur when the user moves from one menu choice to another or from one dialog context to another or from menu mode to/from dialog mode (all examples of workflow or actions). Statecharts extend the functionality of transition diagrams by adding temporal dimensions such as concurrency and synchronization. Statecharts are often used in complex user interface environments, such as aircraft flight control systems.
These techniques are more or less formal methods by definition, and they are quite
often applied to user interface specification tasks. This sub-section contains links
to some representative sources for more information about them.
|Do You Know What Mode You Are In ?||NASA|
Increased automation can lead to an increase in errors when the system interface does
not clearly communicate the current mode of the system or the machine. The problem of
'mode errors' can occur in complex aviation systems as well as in consumer products like
VCR's This paper discusses how statecharts can make mode problems visible during
|Modes in Human-Machine Interaction|
There are three kinds of modes described in the literature on human computer
interaction. Each of these is defined and described using a statechart. The kinds of modes
are discussed in relation to the automatic flight control system of a Boeing B-757.
|Modes in Automated Cockpits||NASA|
Increased automation in aviation systems has given rise to a class of problems called
'automation surprises'. This type of problem is usually caused by human confusion about
the mode of the flight control system. Modes are used in a variety of systems today in
order to increase functionality. Statecharts can be used to describe human-machine
interaction in such systems.
|Modes in Human-Automation Interaction||NASA|
Human error while interacting with complex modal systems like aircraft flight control
systems can be catastrophic. Statecharts provide a way to identify areas where human
confusion is likely. Then these areas can be clarified before the system is put into use.
BetterState is a product for creating statecharts. The site provides detailed product
information as well as a tutorial on statecharts. Online technical support for the product
is also available here.
The first part of this site provides a variety of bookmarks to statechart information.
It includes tools, versions of statecharts and links to pages of people involved in
statecharts work. Not all of the information is directly relevant to user interface
|User Action Notation|
Grammar and diagram approaches to user interface specification fall short for direct
manipulation user interfaces. User Action Notation is a high-level notation which
uses interface-specific symbols and incorporates task and context
considerations in the user interface. UAN adds the crucial dimension of feedback
|Pragmatic Formal Design: A Case Study in Integrating Formal Methods into HCI Design||University of Glasgow|
This paper suggests a pragmatic approach to formal design. In a case study of a
multi-user design rationale editor, it presents a range of semi-formal notations to
perform a task analysis.
|Formal Methods in Computer Human Interaction||Fabio Paterno, Phillipe Palanque|
This page reports on the results of a workshop examination of the need for notations
and models that describe human behavior. Such tools are needed to facilitate design of
|Formal Methods in HCI at QMW||Queen Mary and Westfield College|
This page reports on the application of formal methods to the design of user
interfaces. The need to relate formal models of users' task knowledge to some model of the
interface software, leads to research in interactor models of user interface software.
|Expert Reviews and Usability Inspections|
By their very nature, expert reviews and usability inspections must often employ less
than formal methods of analysis and evaluation. For the purposes of this web site,
however, this section focuses only on those aspects of expert reviews and usability
inspections which utilize or represent formal methods.
|Expert Knowledge Elicitation to Improve Mental and Formal Models||MIT|
Knowledge intensive processes are often driven and constrained by the mental models of
experts acting as direct participants or managers. For example, product development is
guided by expert knowledge including critical process relationships which are dynamic,
biased by individual perspectives and goals, conditioned by experience, aggregate many
system components and relationships and are often nonlinear. Descriptions of these
relationships are not generally available from traditional data sources such as company
records but are stored in the mental models of the process experts. Often the knowledge is
not explicit but tacit, so it is difficult to describe, examine and use.
|Usability Inspections||University of Hawaii|
Usability inspections are a very cost effective way to ensure a more usable
application. We can perform either onsite or offsite usability inspections using a
unique task-based inspection method.
|An Example of Formal Usability Inspections in Practice||Hewlett-Packard Company|
Can usability engineers, not formally educated as human factors engineers, help
facilitate improving the ease of use of software products? Can design engineers learn to
detect usability defects? The answer to both questions is yes. This is a success story of
a partnership between human factors engineers and usability engineers in providing a
Formal Usability Methodology that has been accepted and is continuing to be used by
product developers since it was introduced two years ago. The usability engineers have
added usability practices and facilitation skills to their traditional roles as technical
writers and support engineers. Design engineers enjoy using the methodology, and learn how
to evaluate their products from the user's viewpoint.
|General Usability Engineering|
Usability engineering is a young and growing discipline which, like expert reviews and
usability inspections (which are subsets of usability engineering in their own right),
must often employ less than formal methods. For the purposes of this web site,
however, this sub-section focuses only on those aspects of usability engineering which
relate to formal methods that may be applied to user interface specification.
|Towards a Framework for Investigating Temporal Properties in Interaction||Helen Parker, Chris Roast, and Jawed Siddiqi|
This paper surveys the issues involved in obtaining a clearer understanding of the
formal definition of factors which affect the usability of systems. It explores the
concerns raised in applying traditional engineering approaches to the treatment of
usability requirements and focuses, in particular, on the role that formalisms play in the
analysis of trade-offs between usability and system requirements.
|Formal Methods in Human Computer Interaction||University of York|
This page presents modeling techniques to describe salient features of interactive
systems, based on both domain and cognitive models. Applications under scrutiny include a
case-based reasoning system and an interactive theorem prover.
|Formal Methods in HCI||Staffordshire University|
The School of Computing at Staffordshire University presents a series of tutorials by
Alan Dix on the application of formal methods in human computer interface design.
This page was created by:
This page was last modified on 9/28/98.