A Preliminary Experiment of Checking Usability Principles with Formal Methods

Theoretical computer science has been occupied with formal methods since the beginning. It has had its share of challenges, though. Often, excessive additional work is required to re-specify applications precisely in a new formalism, so that they can be analyzed algorithmically. With more model-based software engineering, this may have changed. In many instances, specifications are now complete and updated throughout the systems development life-cycle, primarily to drive rather than to document the process. Thus, formal approaches have become more realistic. This paper looks at one experiment with automatic usability evaluation, based on a structured user interface specification. It shows that there are promising results ahead. Examples of automatic usability evaluation based on a widely-use user-interface specification language are presented. Benefits of formal specification cannot be reaped, however, unless this approach is bolstered by a purposeful design of the modeling techniques and languages themselves. Thus, some requirements of the formalisms for model-based usability engineering conclude the paper.