Investigating system navigation ergonomics through model verification

Abstract

This paper discusses the use of formal models in the process of investigating the ergonomics of the navigation component in interactive systems. The investigation is based upon model analysis and a set of navigation properties. The formalism employed on this work was Coloured Petri Nets. The paper illustrates how the set of ergonomic properties was mapped into the model properties with the support of the formalism tools and specific functions developed to support the interface designer during model analysis. The context chosen as the basis for discussion is the operation of automated systems in the electricity industry; and a case study is presented to illustrate the analysis. © 2008 Springer-Verlag Berlin Heidelberg.