Home About Help Community
Java UI Tools
Other UI Tools
Formal methods
Email us



Formal Methods


Grammars and Formal Languages
Trees, Transition Diagrams, and Statecharts
User Action Notation
Expert Reviews and Usability Inspections
General Usability Engineering




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 claim.

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 Postscript format.

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 user’s 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 design.seconds.

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 ISI Products

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.

Statecharts Bookmarks Bookmarks 

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 design.

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 as well.

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 interactive systems.

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.