In a modern world torn apart by war the basic human need to feel safe is threatened. In order to defend and protect this need, technical defense systems solving complex situations are of great importance. As the rate of technological innovation accelerates it is important for companies like Saab to maintain their competitive advantage. One way of doing this is by offering modern systems of high quality with intuitive interfaces increasing the usability. This master’s thesis aims at evaluating Saab Surveillance’s command and control system C2STRIC by an analysis of its user interface. It further aims at identifying usability problems and designing prototypes solving said problems, to increase the system’s usability. The system in question is a safety critical system, meaning that its malfunction might lead to severe consequences or death. This system characteristic permeates the whole thesis, resulting in findings unique for C2STRIC and thus maybe not generalizable. Through a close collaboration and interviews with the users the issues were identified and compiled. Due to secrecy reasons all the interviews were conducted live without recordings. All of them at Saab’s premises, except one which was conducted at “Stridslednings- och luftbevakningsskolan” at Uppsala garrison. Most of the interviews were scheduled while some were spontaneous. With the help of the compilation of identified problems, high fidelity prototypes could be developed in Adobe XD through an iterative user-centered design process. The process provided continuous feedback which helped in delivering prototypes satisfying the needs of the users. The primary problems regarded disturbances of the situational awareness of the user, i.e., issues preventing the user from performing its tasks according to circumstances. These disturbances were caused by ineffective navigation in the interface and poorly optimized object visualization. Prototypes introducing transparency, docking systems, search functions, radial menus and a new main menu solved these problems and increased the usability of C2STRIC - and they will in extension help in defending and protecting the basic human need to feel safe.

Reliability of low-level operating-system (OS) code is an indispensable requirement. This includes functional properties from the safety-liveness spectrum, but also quantitative properties stating, e.g., that the average waiting time on locks is sufficiently small or that the energy requirement of a certain system call is below a given threshold with a high probability. This paper reports on our experiences made in a running project where the goal is to apply probabilistic model checking techniques and to align the results of the model checker with measurements to predict quantitative properties of low-level OS code.

Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.

Les langages synchrones tels que Signal, Lustre et Esterel sont dédiés à la conception de systèmes critiques. Leurs compilateurs, qui sont de très gros programmes complexes, peuvent a priori se révéler incorrects dans certains situations, ce qui donnerait lieu alors à des résultats de compilation erronés non détectés. Ces codes fautifs peuvent invalider des propriétés de sûreté qui ont été prouvées en appliquant des méthodes formelles sur les programmes sources. En adoptant une approche de validation de la traduction, cette thèse vise à prouver formellement la correction d'un compilateur optimisé et industriel de Signal. La preuve de correction représente dans un cadre sémantique commun le programme source et le code compilé, et formalise une relation entre eux pour exprimer la préservation des sémantiques du programme source dans le code compilé. / Synchronous languages such as Signal, Lustre and Esterel are dedicated to designing safety-critical systems. Their compilers are large and complicated programs that may be incorrect in some contexts, which might produce silently bad compiled code when compiling source programs. The bad compiled code can invalidate the safety properties that are guaranteed on the source programs by applying formal methods. Adopting the translation validation approach, this thesis aims at formally proving the correctness of the highly optimizing and industrial Signal compiler. The correctness proof represents both source program and compiled code in a common semantic framework, then formalizes a relation between the source program and its compiled code to express that the semantics of the source program are preserved in the compiled code.