Ergonomie ist seit Jahren ein wichtiges Thema in allen Bereichen des Lebens. Unter anderem beinhaltet dies auch die Anpassung der Arbeit an den Arbeiter, um so kurz- und langfristige gesundheitliche Probleme zu minimieren. Ergonomen begutachten in diesem Kontext zum Beispiel den Arbeitsplatz eines Werkers. Sie beobachten ihn bei seiner Tätigkeit, führen Messungen durch und untersuchen die erlangten Daten. Nach der Analyse präsentieren sie ihre Erkenntnisse Dritten (bspw. im Rahmen eines Workshops), dem Management und den Werkern. Insbesondere wenn es um die Auswertung über einen längeren Zeitraum geht (eine ganze Schicht oder mehrere Arbeitszyklen) sind gute Visualisierungen Mangelware und beschränken sich häufig nur auf einfache Linien- oder Balkendiagramme. Um den Ergonomen ihre Tätigkeit zu erleichtern, wurde ein Programm entwickelt, dass die ergonomischen Probleme in einer einfachen Weise als Gesamtüberblick dargestellt. Es ist hierbei möglich von der groben Übersicht aller kritischen Situationen bis hin zu einer detaillierten Ansicht eines Einzelfalls zu navigieren. Ungünstige Posen werden als Piktogramme in Form digitaler Menschmodelle repräsentiert und ermöglichen somit eine intuitive Darstellung. Die Visualisierung berücksichtigt mehrere Methoden aus dem Umfeld der Ergonomie. Eine Methode ist zum Beispiel RULA (Rapid Upper Limb Assessment). Hier wird eine statische Pose des Werkers betrachtet, sozusagen eine Momentaufnahme bei der Ausübung seiner Arbeit. Es basiert auf der Betrachtung der Gelenkwinkel und berücksichtigt zusätzlich Gewichte und Kräfte, die der Werker zu tragen hat beziehungsweise die er aufbringen muss. Darüber hinaus werden auch Anzeichen grenzwertiger Arbeitsumweltfaktoren dargestellt. Die finale interaktive Visualisierung wurde während des gesamten Entwicklungsprozesses in unterschiedlichen Studien evaluiert. Dies beinhaltet unter anderem die Erfassung der Benutzeranforderungen durch Expertenbefragungen, iteratives Prototyping und einer abschließenden Benutzbarkeitsstudie. / Ergonomics deals with the analysis and design of work processes. To identify ergonomically critical situations, appropriate evaluation options have to be developed to enable an efficient analysis process. Nowadays, such analyses are typically carried out with the help of digital models of the surrounding area and virtual humans. These produce a multitude of geo-referenced and time-oriented data. A design study was conducted on how to visualize this data to support the ergonomically analysis process optimally. We propose a novel interactive visualization which provides the user an overview of ergonomically critical situations and their causes. Simultaneously, the user obtains the main stress factors in a compressed form by a glyph-based visual design. During the implementation of the prototype, usability and ergonomics experts were consulted and their suggestions were included in the development of the system. Final expert interviews and a usability study depict the utility of the proposed visualization tool.

Immer wenn neue Anforderungen an ein System gestellt werden, müssen die Korrektheit und Konsistenz der Systemspezifikation überprüft werden, was in der Praxis in der Regel manuell erfolgt. Eine mögliche Option, um die Nachteile dieser manuellen Analyse zu überwinden, ist das sogenannte Contract-Based Design. Dieser Entwurfsansatz kann den Verifikationsprozess zur Überprüfung, ob die Anforderungen auf oberster Ebene konsistent verfeinert wurden, automatisieren. Die Verifikation kann somit iterativ durchgeführt werden, um die Korrektheit und Konsistenz des Systems angesichts jeglicher Änderung der Spezifikationen sicherzustellen. Allerdings ist es aufgrund der mangelnden Benutzerfreundlichkeit und der Schwierigkeiten bei der Interpretation von Verifizierungsergebnissen immer noch eine Herausforderung, formale Ansätze in der Industrie einzusetzen. Stellt beispielsweise der Model Checker bei der Verifikation eine Inkonsistenz fest, generiert er ein Gegenbeispiel (Counterexample) und weist gleichzeitig darauf hin, dass die gegebenen Eingabespezifikationen inkonsistent sind. Hier besteht die gewaltige Herausforderung darin, das generierte Gegenbeispiel zu verstehen, das oft sehr lang, kryptisch und komplex ist. Darüber hinaus liegt es in der Verantwortung der Ingenieurin bzw. des Ingenieurs, die inkonsistente Spezifikation in einer potenziell großen Menge von Spezifikationen zu identifizieren. Diese Arbeit schlägt einen Ansatz zur Erklärung von Gegenbeispielen (Counterexample Explanation Approach) vor, der die Verwendung von formalen Methoden vereinfacht und fördert, indem benutzerfreundliche Erklärungen der Verifikationsergebnisse der Ingenieurin bzw. dem Ingenieur präsentiert werden. Der Ansatz zur Erklärung von Gegenbeispielen wird mittels zweier Methoden evaluiert: (1) Evaluation anhand verschiedener Anwendungsbeispiele und (2) eine Benutzerstudie in Form eines One-Group Pretest-Posttest Experiments. / Whenever new requirements are introduced for a system, the correctness and consistency of the system specification must be verified, which is often done manually in industrial settings. One viable option to traverse disadvantages of this manual analysis is to employ the contract-based design, which can automate the verification process to determine whether the refinements of top-level requirements are consistent. Thus, verification can be performed iteratively to ensure the system’s correctness and consistency in the face of any change in specifications. Having said that, it is still challenging to deploy formal approaches in industries due to their lack of usability and their difficulties in interpreting verification results. For instance, if the model checker identifies inconsistency during the verification, it generates a counterexample while also indicating that the given input specifications are inconsistent. Here, the formidable challenge is to comprehend the generated counterexample, which is often lengthy, cryptic, and complex. Furthermore, it is the engineer’s responsibility to identify the inconsistent specification among a potentially huge set of specifications. This PhD thesis proposes a counterexample explanation approach for formal methods that simplifies and encourages their use by presenting user-friendly explanations of the verification results. The proposed counterexample explanation approach identifies and explains relevant information from the verification result in what seems like a natural language statement. The counterexample explanation approach extracts relevant information by identifying inconsistent specifications from among the set of specifications, as well as erroneous states and variables from the counterexample. The counterexample explanation approach is evaluated using two methods: (1) evaluation with different application examples, and (2) a user-study known as one-group pretest and posttest experiment.

Public displays are increasingly used in public transport to present information such as departure and arrival times or network maps. Since this information is displayed generically, users often have problems to find the specific information they need. We propose context-aware visualizations on public displays to support passengers by improving personalized information access. Several visualizations for this domain were identified, for example, highlighting individual route or pricing information by fading out the background or increasing readability by font size adaptation. To investigate the influence of adapted content on the user we tested prototypical presentations that show personalized information concerning personal trips. In our user study with 20 participants we analyzed these visualizations to compare their efficiency in contrast to non-adaptive content by measuring time to perform specific tasks. This work presents the results of our user study. They show that especially highlighted information supports the user in finding personalized information faster.