Safety-critical software intensive systems are used in a lot of industries nowadays. Examples ofthese are in automotive and aircraft industry, medicine, and autonomous systems. Fault in suchsystems can lead to severe damage and/or loss of human lives. Therefore fault-tolerance should beconsidered at all stages of the system development, starting from the analysis and design.Different languages and tools have been developed for that purpose across the years. One of these isthe Architecture Analysis and Design Language (AADL) – a modeling language used to describethe architecture of a software system. It consists of textual and graphical descriptions of three typesof components – software, execution platform and composite.In this work we implement a prototype of an AADL simulator in Java that enables us to examine thepossible dynamic executions of an AADL specification. This allows us to verify the correctness ofan AADL specification based on the behavior it shows. The simulator would expect an AADLspecification of a software system as an input and simulate the dynamic execution of that system.Before implementing the simulator, we introduce the problem area - safety-critical systems andAADL. Since AADL is used primarily in the automotive and aircraft industries, we have chosen todescribe a simplified flight control system for a plane. It should give the reader an initialunderstanding of the language without going into unnecessary detail about rarely used features.Part of the simulator is a compiler that reads the AADL specification, validates it and transforms itto a Java model. We take a look at the individual steps needed for that, with focus on parsing theinput. Therefore we review the different kinds of algorithms used for parsing and explore how theywork.We also make a detailed literature review of previous works in the area of AADL modeltransformations. Finally, we describe the analysis, design and implementation of the simulator andexamine a case study to test the prototype.

Les systèmes critiques de vol tels que les actionneurs électromécaniques ainsi que les calculateurs de commande moteur (ECU) et de vol (FCU),sont conçus en tenant compte des contraintes aéronautiques sévères de sureté defonctionnement. Dans le cadre de cette étude, une architecture calculateur pourla commande et la surveillance d’actionneurs moteur et de surfaces de vol est proposée et à fait l’objet d’un brevet [13]. Pour garantir ces mesure de sureté, les ECU et FCU présentent des redondances matérielles multiples, mais engendrent une augmentation de l’encombrement, du poids et de l’énergie consommée. Pour ces raisons, les redondances à base de modèles dynamiques, présentent un atout majeur pour les calculateurs car elles permettent dans certains cas de maintenir les exigences d’intégrité et de disponibilité tout en réduisant le nombre de capteurs ou d’actionneurs. Un rappel sur les méthodes de diagnostic par générateurs de résidus et estimateurs d’états [58, 26, 47] est effectué dans cette étude. Les propriétés de platitude différentielle et la linéarisation par difféomorphisme et bouclage endogène [80, 41, 73] permettent d’utiliser des modèles linéaires équivalents avec les générateurs de résidus. Un banc d’essai a été conçu afin de valider les performances des algorithmes de diagnostic. / Flight-Critical Systems such as Electromechanical Actuators driven by Engine Control Units (ECU) or Flight Control Units (FCU) are designed and developed regarding drastic safety requirements. In this study, an actuator control and monitoring ECU architecture based on analytic redundancy is proposed. In case of fault occurrences, material redundancies in avionic equipment allow certaincritical systems to reconfigure or to switch into a safe mode. However, material redundancies increase aircraft equipment size, weight and power (SWaP). Monitoring based on dynamical models is an interesting way to further enhance safetyand availability without increasing the number of redundant items. Model-base dfault detection and isolation (FDI) methods [58, 26, 47] such as observers and parity space are recalled in this study. The properties of differential flatness for nonlinear systems [80, 41, 73] and endogenous feedback linearisation are used with nonlinear diagnosis models. Linear and nonlinear observers are then compared with an application on hybrid stepper motor (HSM). A testing bench was specially designed to observe in real-time the behaviour of the diagnosis models when faults occur on the stator windings of a HSM.

This thesis if focused on brand building on the internet and possibilities brought to this filed by usage of systems methodologies. SWOT analysis is widely used in marketing, but it is focused solely on evaluating the current state of things and there is no formal framework to connect branding with marketing. Critical Systems Heuristics (CSH) methodology is used to supplement traditional marketing approaches. CSH consists of 12 boundary questions which can be used to define ideal state of analyzed systems. CSH methodology is then used to create a draft of Monoe brand, which will stand for a provider of photographical and graphical services. Based on gathered information from boundary questions, a website for the brand was created and promotion on social networks was also started. This practical use of CSH shoved that the boundary questions are too vague to be properly used in branding, but mostly address the right fields. Because of that, the boundary questions were modified. The asset of this thesis is modifying CSH methodology so it can be used as a framework to build brands on the internet.

Cyber-Physical Systems (CPSs) are the core of modern critical infrastructure (e.g. power-grids) and securing them is of paramount importance. Anomaly detection in data is crucial for CPS security. While Artificial Neural Networks (ANNs) are strong candidates for the task, they are seldom deployed in safety-critical domains due to the perception that ANNs are black-boxes. Therefore, to leverage ANNs in CPSs, cracking open the black box through explanation is essential. The main objective of this dissertation is developing explainable ANN-based Anomaly Detection Systems for Cyber-Physical Systems (CP-ADS). The main objective was broken down into three sub-objectives: 1) Identifying key-requirements that an explainable CP-ADS should satisfy, 2) Developing supervised ANN-based explainable CP-ADSs, 3) Developing unsupervised ANN-based explainable CP-ADSs. In achieving those objectives, this dissertation provides the following contributions: 1) a set of key-requirements that an explainable CP-ADS should satisfy, 2) a methodology for deriving summaries of the knowledge of a trained supervised CP-ADS, 3) a methodology for validating derived summaries, 4) an unsupervised neural network methodology for learning cyber-physical (CP) behavior, 5) a methodology for visually and linguistically explaining the learned CP behavior. All the methods were implemented on real-world and benchmark datasets. The set of key-requirements presented in the first contribution was used to evaluate the performance of the presented methods. The successes and limitations of the presented methods were identified. Furthermore, steps that can be taken to overcome the limitations were proposed. Therefore, this dissertation takes several necessary steps toward developing explainable ANN-based CP-ADS and serves as a framework that can be expanded to develop trustworthy ANN-based CP-ADSs.

Dans les approches centrées utilisateur, les techniques, méthodes, et processus de développement utilisés visent à connaître et comprendre les utilisateurs (analyser leurs besoins, évaluer leurs manières d'utiliser les systèmes) dans le but de concevoir et développer des systèmes utilisables, c'est-à-dire, en adéquation avec leurs comportements, leurs compétences et leurs besoins. Parmi les techniques employées pour garantir l'utilisabilité, la modélisation des tâches permet de décrire les objectifs et acticités des utilisateurs. Grâce aux modèles produits, les spécialistes des facteurs humains peuvent analyser et évaluer l'efficacité des applications interactives. Cette approche d'analyse et de modélisation de tâches a toujours mis l'accent sur la représentation explicite du comportement standard de l'utilisateur. Ceci s'explique par le fait que les erreurs humaines ne font pas partie des objectifs des utilisateurs et qu'ils sont donc exclus de la description des tâches. Cette vision sans erreurs, suivie largement par la communauté en Interaction Homme-Machine, est très différente de celle de la communauté en Facteur Humain qui, depuis ses débuts, s'intéresse à comprendre les causes des erreurs humaines et leur impact sur la performance, mais aussi sur des aspects majeurs comme la sureté de fonctionnement et la fiabilité des utilisateurs et de leur travail. L'objectif de cette thèse est de démontrer qu'il est possible de décrire de façon systématique, dans des modèles de tâches, les erreurs pouvant survenir lors de l'accomplissement de tâches utilisateur. Pour cette démonstration, nous proposons une approche à base de modèles de tâches associée à un processus de description des erreurs humaines et supportée par un ensemble d'outils. Cette thèse présente les résultats de l'application de l'approche proposée à une étude de cas industrielle dans le domaine d'application de l'aéronautique. / In user-centered approaches, the techniques, methods, and development processes used aim to know and understand the users (analyze their needs, evaluate their ways of using the systems) in order to design and develop usable systems that is in line with their behavior, skills and needs. Among the techniques used to guarantee usability, task modeling makes it possible to describe the objectives and activities of the users. With task models, human factors specialists can analyze and evaluate the effectiveness of interactive applications. This approach of task analysis and modeling has always focused on the explicit representation of the standard behavior of the user. This is because human errors are not part of the users' objectives and are therefore excluded from the job description. This vision of error-free activities, widely followed by the human-machine interaction community, is very different from the Human Factor community vison on user tasks. Since its inception, Human Factor community has been interested in understanding the causes of human error and its impact on performance, but also on major aspects like the reliability of the operation and the reliability of the users and their work. The objective of this thesis is to demonstrate that it is possible to systematically describe, in task models, user errors that may occur during the performance of user tasks. For this demonstration, we propose an approach based on task models associated with a human error description process and supported by a set of tools. This thesis presents the results of the application of the proposed approach to an industrial case study in the application domain of aeronautics.

A system is safety-critical if its malfunctioning could have catastrophic consequences for people, property or the environment, e.g., the failure in a car's braking system could be potentially tragic. To produce such type of systems, special procedures, and strategies, that permit their safer deployment into society, should be used. Therefore, manufacturers of safety-critical systems comply with domain-specific safety standards, which embody the public consensus of acceptably safe. Safety standards also contain a repository of expert knowledge and best practices that can, to some extent, facilitate the safety-critical system’s engineering. In some domains, the applicable safety standards establish the accepted procedures that regulate the development processes. For claiming compliance with such standards, companies should adapt their practices and provide convincing justifications regarding the processes used to produce their systems, from the initial steps of the production. In particular, the planning of the development process, in accordance with the prescribed process-related requirements specified in the standard, is an essential piece of evidence for compliance assessment. However, providing such evidence can be time-consuming and prone-to-error since it requires that process engineers check the fulfillment of hundreds of requirements based on their processes specifications. With access to suitable tool-supported methodologies, process engineers would be able to perform their job efficiently and accurately. Safety standards prescribe requirements in natural language by using notions that are subtly similar to the concepts used to describe laws. In particular, requirements in the standards introduce conditions that are obligatory for claiming compliance. Requirements also define tailoring rules, which are actions that permit to comply with the standard in an alternative way. Unfortunately, current approaches for software verification are not furnished with these notions, which could make their use in compliance checking difficult. However, existing tool-supported methodologies designed in the legal compliance context, which are also proved in the business domain, could be exploited for defining an adequate automated compliance checking approach that suits the conditions required in the safety-critical context. The goal of this Licentiate thesis is to propose a novel approach that combines: 1) process modeling capabilities for representing systems and software process specifications, 2) normative representation capabilities for interpreting the requirements of the safety standards in an adequate machine-readable form, and 3) compliance checking capabilities to provide the analysis required to conclude whether the model of a process corresponds to the model with the compliant states proposed by the standard's requirements. Our approach contributes to facilitating compliance checking by providing automatic reasoning from the requirements prescribed by the standards, and the description of the process they regulate. It also contributes to cross-fertilize two communities that were previously isolated, namely safety-critical and legal compliance contexts. Besides, we propose an approach for mastering the interplay between highly-related standards. This approach includes the reuse capabilities provided by SoPLE (Safety-oriented Process Line Engineering), which is a methodological approach aiming at systematizing the reuse of process-related information in the context of safety-critical systems. With the addition of SoPLE, we aim at planting the seeds for the future provision of systematic reuse of compliance proofs. Hitherto, our proposed methodology has been evaluated with academic examples that show the potential benefits of its use. / AMASS

Traditionnellement, dans le domaine avionique les logiciels utilisés à bord de l’avion sont totalement séparés des logiciels utilisés au dehors afin d’éviter toutes interaction qui pourrait corrompre les systèmes critiques à bord de l’avion. Cependant, les nouvelles générations d’avions exigent plus d’interactions avec le monde ouvert avec pour objectif de proposer des services étendu, générant ainsi un flux d’information potentiellement dangereux. Dans une précédente étude, nous avons proposé l’utilisation de la virtualisation pour assurer la sûreté de fonctionnement d’applications critiques assurant des communications bidirectionnelles entre systèmes critiques et systèmes non sûr. Dans cette thèse nous proposons deux contributions.La première contribution propose une méthode de comparaison d’hyperviseur. Nous avons développé un banc de test permettant de mesurer les performances d’un système virtualisé. Dans cette étude, différentes configurations ont été expérimentées, d’un système sans OS à une architecture complète avec un hyperviseur et un OS s’exécutant dans une machine virtuelle. Plusieurs tests (processeur, mémoire et réseaux) ont été mesurés et collectés sur différents hyperviseurs.La seconde contribution met l’accent sur l’amélioration d’une architecture de sécurité existante. Un mécanisme de comparaison basé sur l’analyse des traces d’exécution est utilisé pour détecter les anomalies entre instances d’application exécutées sur diverse machines virtuelles. Nous proposons de renforcer le mécanisme de comparaison à l’exécution par l’utilisation d’un modèle d’exécution issu d’une analyse statique du bytecode Java.Afin de valider notre approche, nous avons développé un prototype basé sur un cas d’étude identifié avec Airbus qui porte sur l’utilisation d’un ordinateur portable dédié à la maintenance / Traditionally, in avionics, on-board aircraft software used to be totally separated from open-world software in order to avoid any interaction that could corrupt critical on-board systems. However, new aircraft generations require more interaction with off-board systems to provide extended services, which makes these information flows potentially dangerous.In a previous work, we have proposed the use of virtualization to ensure dependability of critical applications despite bidirectional communication between critical on-board systems and untrusted off-board systems. In this thesis, we propose two contributions.The first contribution concerns the establishment of a benchmark of hypervisors. We have developed a test bed to assess the performance impact induced by the use of virtualization. In this work, various configurations have been experimented ranging from a basic machine without an OS up to the complete architecture featuring a hypervisor and an OS running in a virtual machine. Several tests (computation, memory, and network) are carried out, and timing measures are collected on different hypervisors.The second contribution focuses on the improvement of an existing security architecture. A comparison mechanism based on the analysis of execution traces is used to detect discrepancies between replicas supported by diverse virtual machines. We proposeto strengthen the comparison mechanism at runtime by the use of an execution model, derived from a static analysis of the java bytecode

Formal verification methods have been shown to be very effective in finding corner-case bugs and ensuring the safety of embedded software systems. The use of formal verification requires a specification, which is typically a high-level mathematical model that defines the correct behavior of the system to be verified. However, embedded software requirements are typically described in natural language. Transforming these requirements into formal specifications is currently a big gap. While there is some work in this area, we proposed solutions to address this gap in the context of refinement-based verification, a class of formal methods that have shown to be effective for embedded object code verification. The proposed approach also addresses both functional and timing requirements and has been demonstrated in the context of safety requirements for software control of infusion pumps. The next step in the verification process is to develop the refinement map, which is a mapping function that can relate an implementation state (in this context, the state of the object code program to be verified) with the specification state. Actually, constructing refinement maps often requires deep understanding and intuitions about the specification and implementation, it is shown very difficult to construct refinement maps manually. To go over this obstacle, the construction of refinement maps should be automated. As a first step toward the automation process, we manually developed refinement maps for various safety properties concerning the software control operation of infusion pumps. In addition, we identified possible generic templates for the construction of refinement maps. Recently, synthesizing procedures of refinement maps for functional and timing specifications are proposed. The proposed work develops a process that significantly increases the automation in the generation of these refinement maps. The refinement maps can then be used for refinement-based verification. This automation procedure has been successfully applied on the transformed safety requirements in the first part of our work. This approach is based on the identified generic refinement map templates which can be increased in the future as the application required.

This thesis evaluates the AMLAS methodology. To support the evaluation, literature studies are conducted and a machine learning dependent system that detects people and helmets is implemented. The practical work is performed according to the documentation of AMLAS. Alongside this work, a user interface is developed. The user interface and the machine learning component is merged to create the complete system. The results show that AMLAS contributes with safety, structure and reliability to the system. However, the findings show that AMLAS is missing some aspects. / <p>Examensarbetet är utfört vid Institutionen för teknik och naturvetenskap (ITN) vid Tekniska fakulteten, Linköpings universitet</p>

Many industrial control systems use programmable logic controllers (PLCs) since they provide a highly reliable, off-the-shelf hardware platform. On the programming side, function blocks (FBs) are reusable PLC components that can be composed to implement the required system behaviour. A higher quality system may be realized if the FBs are pre-certified to be compliant with an international standard such as IEC 61131-3. Unfortunately, the set of programming notations defined in IEC 61131-3 lack well-defined formal semantics. As a result, tool vendors and users of PLCs may have inconsistent interpretations of the expected system behaviour. To address this issue, we propose an engineering method for formally verifying the conformance of candidate implementations of FBs (and their compositions) to their high-level, input-output requirements. The proposed method is sufficiently general to handle FBs supplied by IEC 61131-3, and industrial FB applications involving real-time requirements. Our method involves several steps. First, we use tabular expressions to ensure the completeness and disjointness of the requirements for the FB. Second, we formalize the candidate implementation(s) of the FB in question. Third, we state and prove theorems regarding the consistency and correctness of the FB. All three steps are performed using the Prototype Verification Systems (PVS) proof assistant. As a first case study, we apply our approach to the IEC 61131-3 standard to examine the entire library of FBs and their supplied implementations described in structured text (ST) and function block diagrams (FBDs). As a second case study, we apply our approach to two realistic sub-systems taken from the nuclear domain. Applying the proposed method, we identified three kinds of issues: ambiguous behavioural descriptions, missing assumptions, and erroneous implementations. Furthermore, we suggest solutions to these issues. / Thesis / Doctor of Philosophy (PhD) / A formal verification approach for the function block based control systems