In dieser Arbeit wird eine Analysemethode entwickelt, die Mensch-Maschine-Systeme auf Basis diskreter mathematischer Modelle beschreibt. Die Modelle werden anhand einer hierarchischen automatenbasierten Beschreibungstechnik dargestellt. Der Schwerpunkt liegt in der strukturierten Beschreibung des Interaktionsverhaltens; die graphische Gestaltung der Nutzerschnittstelle steht nicht im Zentrum. Wesentliche Konzepte menügetriebener Nutzerschnittstellen werden zu einem konzeptuellen Modell zusammengefasst und in die Beschreibungstechnik integriert. Für die Modelle werden Eigenschaften, die in Bezug zur Gebrauchstauglichkeit stehen, identifiziert und mit Hilfe der Temporalen Logik formalisiert. Mit der Technik Model-Checking wird automatisch geprüft, ob die Modelle diese Eigenschaften erfüllen. Die praktische Anwendbarkeit der entwickelten Methode wird anhand einer umfangreichen Fallstudie aus dem Automotive-Bereich gezeigt.     «

In dieser Arbeit wird eine Analysemethode entwickelt, die Mensch-Maschine-Systeme auf Basis diskreter mathematischer Modelle beschreibt. Die Modelle werden anhand einer hierarchischen automatenbasierten Beschreibungstechnik dargestellt. Der Schwerpunkt liegt in der strukturierten Beschreibung des Interaktionsverhaltens; die graphische Gestaltung der Nutzerschnittstelle steht nicht im Zentrum. Wesentliche Konzepte menügetriebener Nutzerschnittstellen werden zu einem konzeptuellen Modell zusa...     »

In this thesis, an analysis method is developed that describes human-machine systems by means of discrete mathematical models. The models are notated by a hierarchical automaton-based description technique. The main focus lies on the structured description of the interaction behaviour and not on the graphical design of the user interface. The key concepts for the description of menue-driven user interfaces are combined within a conceptual model and integrated into the automaton-based description technique. Significantly, the properties of the models that influence the quality attribute 'usability' are identified and formalized by means of temporal logic. With the aid of model checking the conformity of the models to these properties is automatically verified. The practical applicability of the developed method is shown by means of an extensive case study from the automotive field.     «

In this thesis, an analysis method is developed that describes human-machine systems by means of discrete mathematical models. The models are notated by a hierarchical automaton-based description technique. The main focus lies on the structured description of the interaction behaviour and not on the graphical design of the user interface. The key concepts for the description of menue-driven user interfaces are combined within a conceptual model and integrated into the automaton-based descript...     »