Software product line engineering is a proposed methodology that enables software products and software-intensive systems to be developed at lower cost, higher quality and less time to market. The structured and managed artifacts reuse among different products in development is the main target of software product line engineering. As a key-method of the product line engineering approach, the commonality and variability analysis is a technique that identifies the potential artifacts for reuse. But the reuse poses challenges for delivering safety-critical products from the product line and achieving product line functional safety. In order to analyze the product line and provide more valuable information for its safety analysis, we make use of established product line modeling techniques, which model the product line commonality and variability from different perspectives. In this report, we investigate the product line modeling techniques. The product modeling analysis process covers two aspects: 1. Study different product line modeling techniques and find the ones suitable for product line modeling. We choose the modeling techniques that can be implemented to discuss in detail. 2. We implement the industrial wheel loader product line with two modeling techniques. Comprehensive models and detailed modeling process explanation are presented. The product line functional safety analysis covers three aspects: 1. Investigate the different safety analysis techniques and choose the fault tree analysis as the main technique. 2. Extend the single system fault tree to the product line fault tree. 3. Investigate the contributions of the product line modeling techniques to the product line functional safety analysis. Specifically, we map the product line models to the product line fault tree. Furthermore, we evaluate the product line modeling techniques from their performance in domain analysis and safety analysis.

Context: With the development of artificial intelligence, autonomous vehicles are becoming more and more feasible and the safety of Automated Driving (AD) system should be assured. This creates a need to analyze the feasibility of verification and validation approaches when testing safety-critical system that contains machine learning (ML) elements. There are many studies published in the context of verification and validation (V&V) research area related to safety-critical components. However, there are still blind spots of research to identify which test methods can be used to test components with deep learning elements for AD system. Therefore, research should focus on researching the relation of test methods and safety-critical components, also need to find more feasible V&V testing methods for AD system with deep learning structure. Objectives: The main objectives of this thesis is to understand the challenges and solution proposals related to V&V of safety-critical systems that rely on machine learning and provide recommendations for future V&V of AD based on deep learning, both for research and practice. Methods: We performed a Systematic Literature Review (SLR) through a snowballing method, based on the guidelines from Wohlin [1], to identify research on V&V methods development for machine learning. A web-based survey was used to complement the result of literature review and evaluate the V&V challenge and methods for machine learning system. We identified 64 peer-reviewed papers and analysed the methods and challenges of V&V for testing machine learning components. We conducted an industrial survey that was answered by 63 subjects. We analyzed the survey results with the help of descriptive statistics and Chi-squared tests. Result: Through the SLR we identified two peaks for research on V&V of machine learning. Early research focused on the aerospace field and in recent years the research has been more active in other fields like automotive and robotics. 21 challenges during V&V safety-critical systems have been described and 32 solution proposals are addressing the challenges have been identified. To find the relationship between challenges and methods, a classification has been done that seven different type of challenges and five different type of solution proposals have been identified. The classification and mapping of challenges and solution methods are included in the survey questionnaire. From the survey, it was observed that some solution proposals which have attracted much research are not considered as particularly promising by practitioners. On the other hand, some new solution methods like simulated test cases are extremely promising to support V&V for safety-critical systems. Six suggestions are provided to both researchers and practitioners. Conclusion: To conclude the thesis, our study presented a classification of challenges and solution methods for V&V of safety-critical ML-based systems. We also provide a mapping for helping practitioners understand the different kinds of challenges the respective solution methods address. Based on our findings, we provide suggestions to both researchers and practitioners. Thus, through the analysis, we have given the most concern on types of challenges and solution proposals for AD systems that use deep learning, which provides certain help to design processes for V&V of safety-critical ML-based systems in the future.

An increased focus on the development of autonomous safety-critical systems requiresmore attention at ensuring safety of humans and the environment. The mainobjective of this thesis is to explore the state of the art and to identify the safetyrelatedchallenges being addressed for using autonomy in safety-critical systems. Inparticular, the thesis explores the nature of these challenges, the different autonomylevels they address and the type of safety measures as proposed solutions. Above all,we focus on the safety measures by a degree of adaptiveness, time of being activeand their ability of decision making. Collection of this information is performedby conducting a Systematic Literature Review of publications from the past 9 years.The results showed an increase in publications addressing challenges related to theuse of autonomy in safety-critical systems. We managed to identify four high-levelclasses of safety challenges. The results also indicate that the focus of research wason finding solutions for challenges related to full autonomous systems as well assolutions that are independent of the level of autonomy. Furthermore, consideringthe amount of publications, results show that non-learning solutions addressing theidentified safety challenges prevail over learning ones, active over passive solutionsand decisive over supportive solutions.

A evolução de sistemas de gerenciamento de tráfego aéreo é pesquisada para suportar o crescimento na demanda por transporte aéreo. Uma alternativa para essa evolução é o aumento no grau de automação. Os sistemas automatizados precisam ser tão seguros quanto os sistemas em operação atualmente. Com o uso de técnicas de especificação e verificação formal é possível avaliar os requisitos de sistemas. Neste trabalho, é proposto um ciclo de especificação formal, que consiste em um conjunto de diretrizes para aplicação de técnicas de métodos formais em requisitos escritos em linguagem natural. O resultado esperado da aplicação deste ciclo é um conjunto de requisitos escritos em linguagem natural verificados formalmente. O ciclo é composto pelas etapas: levantamento de requisitos do sistema e classificação em padrões de especificação; mapeamento dos requisitos para as linguagens de especificação formal LTL (Linear Temporal Logic) e CTL (Computation Tree Logic); verificação formal da especificação com o verificador NuSMV; ajustes na especificação baseada nos resultados da verificação; ajustes nos requisitos baseados nos ajustes na especificação. As diretrizes propostas são definidas com a análise da verificação formal do Automated Airspace Concept (AAC), padrões de especificação e diretrizes para uso do verificador NuSMV. Os resultados esperados são obtidos na aplicação do ciclo de especificação em dois estudos de caso. A principal contribuição do trabalho é o conjunto de diretrizes para elaboração de expressões escritas em linguagem de especificação formal baseadas em requisitos escritos em linguagem natural e que podem ser verificadas formalmente. / Air traffic management systems evolution is being researched to support air transportation demand growth. An evolution alternative is system automation degree increase. Automated systems need to be as safe as current operating systems. It is possible to analyze system requirements with the application of formal specification and formal verification techniques. In this work, a specification cycle is proposed. The specification cycle is a set of guidelines to use formal method techniques on requirements written in natural language. The specification cycle application expected result is a set of formally verified requirements written in natural language. This cycle is comprised of the following stages: system requirements elicitation and specification pattern classification; requirements mapping to LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) formal specification languages; specification formal verification using the NuSMV verifier; formal specification adjustment based on verification results; requirements adjustment based on formal specification adjustment. The proposed guidelines are defined with the Automated Airspace Concept (AAC) formal verification analysis, specification patterns and guidelines for the NuSMV formal verifier use. The expected results are accomplished in the specification cycle application on two study cases. The main contribution of this work is the set of guidelines applied to formulate formally verifiable expressions specified in formal specification languages based on system requirements written in natural language.

A evolução de sistemas de gerenciamento de tráfego aéreo é pesquisada para suportar o crescimento na demanda por transporte aéreo. Uma alternativa para essa evolução é o aumento no grau de automação. Os sistemas automatizados precisam ser tão seguros quanto os sistemas em operação atualmente. Com o uso de técnicas de especificação e verificação formal é possível avaliar os requisitos de sistemas. Neste trabalho, é proposto um ciclo de especificação formal, que consiste em um conjunto de diretrizes para aplicação de técnicas de métodos formais em requisitos escritos em linguagem natural. O resultado esperado da aplicação deste ciclo é um conjunto de requisitos escritos em linguagem natural verificados formalmente. O ciclo é composto pelas etapas: levantamento de requisitos do sistema e classificação em padrões de especificação; mapeamento dos requisitos para as linguagens de especificação formal LTL (Linear Temporal Logic) e CTL (Computation Tree Logic); verificação formal da especificação com o verificador NuSMV; ajustes na especificação baseada nos resultados da verificação; ajustes nos requisitos baseados nos ajustes na especificação. As diretrizes propostas são definidas com a análise da verificação formal do Automated Airspace Concept (AAC), padrões de especificação e diretrizes para uso do verificador NuSMV. Os resultados esperados são obtidos na aplicação do ciclo de especificação em dois estudos de caso. A principal contribuição do trabalho é o conjunto de diretrizes para elaboração de expressões escritas em linguagem de especificação formal baseadas em requisitos escritos em linguagem natural e que podem ser verificadas formalmente. / Air traffic management systems evolution is being researched to support air transportation demand growth. An evolution alternative is system automation degree increase. Automated systems need to be as safe as current operating systems. It is possible to analyze system requirements with the application of formal specification and formal verification techniques. In this work, a specification cycle is proposed. The specification cycle is a set of guidelines to use formal method techniques on requirements written in natural language. The specification cycle application expected result is a set of formally verified requirements written in natural language. This cycle is comprised of the following stages: system requirements elicitation and specification pattern classification; requirements mapping to LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) formal specification languages; specification formal verification using the NuSMV verifier; formal specification adjustment based on verification results; requirements adjustment based on formal specification adjustment. The proposed guidelines are defined with the Automated Airspace Concept (AAC) formal verification analysis, specification patterns and guidelines for the NuSMV formal verifier use. The expected results are accomplished in the specification cycle application on two study cases. The main contribution of this work is the set of guidelines applied to formulate formally verifiable expressions specified in formal specification languages based on system requirements written in natural language.

These days, a wide range of autonomous systems, such as automobiles, delivery drones, and embedded household systems, are becoming more and more common in our society. This trend is projected to continue in the future. To effectively manage these dynamic systems, ensuring their safe operation is crucial for the well-being of our lives. Control of safety-critical systems has gained significant attention in recent years, particularly in the field of nonlinear control. While the mathematical tools for characterizing safety are well-established, there are still numerous challenges to be addressed when it comes to developing methodologies for synthesizing nonlinear control systems. This report investigates the similarity between the two control schemes, the prescribed performance control and control barrier function. Its purpose is to shed light on the development of control methodology in safetycritical systems. While both methods have been successfully constructed and developed recently, there is no existing report that clarifies their similarities. To gain a deeper understanding of the latest safety-critical control and investigate these similarities, this report aims to provide interesting insights and contribute to the further development of methodology. The key insight arises from the fact that the prescribed performance control can be considered a method based on barrier functions. Consequently, it can be regarded as a control barrier-based controller. In order to demonstrate the similarities and make a comparison between the two, a unified problem setting is presented. Once we have properly converted the problem, we can proceed with a comparison using numerical simulations. The results presented in this report demonstrate that the prescribed performance controller can be implemented using separate reciprocal CBF methods. Furthermore, it shows that the performance achieved is comparable to that of the CLF-CBF QP, which utilizes optimization techniques to ensure stability and safety requirements. These findings raise new questions regarding the relationship between these two approaches. Ultimately, the report delves into a deeper understanding of how model-free methods achieve superior performance compared to model-based methods that heavily rely on optimization. / Idag blir ett brett spektrum av autonoma system, som bilar, leveransdrönare och inbyggda hushållssystem, allt vanligare i vårt samhälle. Denna trend förväntas fortsätta i framtiden. För att effektivt hantera dessa dynamiska system är det avgörande att säkerställa att de fungerar på ett säkert sätt. Styrning av säkerhetskritiska system har fått stor uppmärksamhet under de senaste åren, särskilt inom området icke-linjär styrning. Även om de matematiska verktygen för att karakterisera säkerhet är väletablerade, finns det fortfarande många utmaningar att ta itu med när det gäller att utveckla metoder för att syntetisera olinjära styrsystem. Denna rapport undersöker likheten mellan de två kontrollsystemen, den föreskrivna prestandakontrollen och kontrollbarriärfunktionen. Syftet är att belysa utvecklingen av styrmetodik i säkerhetskritiska system. Även om båda metoderna har konstruerats och utvecklats framgångsrikt på senare tid, finns det ingen befintlig rapport som klargör deras likheter. För att få en djupare förståelse för den senaste säkerhetskritiska kontrollen och undersöka dessa likheter, syftar denna rapport till att ge intressanta insikter och bidra till den fortsatta utvecklingen av metodiken. Den viktigaste insikten härrör från det faktum att den föreskrivna prestandakontrollen kan betraktas som en metod baserad på barriärfunktioner. Följaktligen kan den betraktas som en styrbarriärbaserad styrenhet. För att visa på likheterna och göra en jämförelse mellan de två presenteras en enhetlig problemställning. När vi har omvandlat problemet på rätt sätt kan vi gå vidare med en jämförelse med hjälp av numeriska simuleringar. De resultat som presenteras i denna rapport visar att den föreskrivna prestandaregulatorn kan implementeras med separata reciproka CBF-metoder. Dessutom visar de att den uppnådda prestandan är jämförbar med den för CLFCBF QP, som använder optimeringstekniker för att säkerställa stabilitets- och säkerhetskrav. Dessa resultat väcker nya frågor om förhållandet mellan dessa två metoder. I slutändan ger rapporten en djupare förståelse för hur modellfria metoder uppnår överlägsen prestanda jämfört med modellbaserade metoder som i hög grad förlitar sig på optimering.

No description available.

The importance and requirements of certifying safety critical software is today more apparent than ever. This study focuses on the standards and practices used within the avionics, automotive and medical domain when it comes to safety critical software. We identify critical problems and trends when certifying safety critical software and propose a proof-of-concept using static analysis, model checking and incremental SAT solving as a contribution towards solving the identified problems. We present quantitative execution times and code coverage results of our proposed solution. The proposed solution is developed under the assumptions of safety critical software standards and compared to other studies proposing similar methods. Lastly, we conclude the issues and advantages of our proof-of-concept in perspective of the software developer community

Ce travail de thèse doctorale traite l'analyse de la vulnérabilité des systèmes critiques pour la sécurité (par exemple, les centrales nucléaires) dans un cadre qui combine les disciplines de l'analyse des risques et de la prise de décision de multi-critères.La contribution scientifique suit quatre directions: (i) un modèle hiérarchique et quantitative est développé pour caractériser la susceptibilité des systèmes critiques pour la sécurité à plusieurs types de danger, en ayant la vue de `tous risques' sur le problème actuellement émergeant dans le domaine de l'analyse des risques; (ii) l'évaluation quantitative de la vulnérabilité est abordé par un cadre de classification empirique: à cette fin, un modèle, en se fondant sur la Majority Rule Sorting (MR-Sort) Méthode, généralement utilisés dans le domaine de la prise de décision, est construit sur la base d'un ensemble de données (en taille limitée) représentant (a priori connu) des exemples de classification de vulnérabilité; (iii) trois approches différentes (à savoir, une model-retrieval-based méthode, la méthode Bootstrap et la technique de validation croisée leave-one-out) sont élaborées et appliquées pour fournir une évaluation quantitative de la performance du modèle de classification (en termes de précision et de confiance dans les classifications), ce qui représente l'incertitude introduite dans l'analyse par la construction empirique du modèle de la vulnérabilité; (iv) basé sur des modèles développés, un problème de classification inverse est résolu à identifier un ensemble de mesures de protection qui réduisent efficacement le niveau de vulnérabilité du système critique à l’étude. Deux approches sont développées dans cet objectif: le premier est basé sur un nouvel indicateur de sensibilité, ce dernier sur l'optimisation.Les applications sur des études de cas fictifs et réels dans le domaine des risques de centrales nucléaires démontrent l'efficacité de la méthode proposée. / This Ph. D. work addresses the vulnerability analysis of safety-critical systems (e.g., nuclear power plants) within a framework that combines the disciplines of risk analysis and multi-criteria decision-making. The scientific contribution follows four directions: (i) a quantitative hierarchical model is developed to characterize the susceptibility of safety-critical systems to multiple types of hazard, within the needed `all-hazard' view of the problem currently emerging in the risk analysis field; (ii) the quantitative assessment of vulnerability is tackled by an empirical classification framework: to this aim, a model, relying on the Majority Rule Sorting (MR-Sort) Method, typically used in the decision analysis field, is built on the basis of a (limited-size) set of data representing (a priori-known) vulnerability classification examples; (iii) three different approaches (namely, a model-retrieval-based method, the Bootstrap method and the leave-one-out cross-validation technique) are developed and applied to provide a quantitative assessment of the performance of the classification model (in terms of accuracy and confidence in the assignments), accounting for the uncertainty introduced into the analysis by the empirical construction of the vulnerability model; (iv) on the basis of the models developed, an inverse classification problem is solved to identify a set of protective actions which effectively reduce the level of vulnerability of the critical system under consideration. Two approaches are developed to this aim: the former is based on a novel sensitivity indicator, the latter on optimization.Applications on fictitious and real case studies in the nuclear power plant risk field demonstrate the effectiveness of the proposed methodology.

In der vorliegenden Arbeit werden eine sichere FPGA-Stellwerksplattform und ein Transformationsverfahren entwickelt, mit dem die Schaltungen bestehender Relaisstellwerke in eine FPGA-Logik überführt werden können. Die FPGA-Stellwerksplattform ersetzt die Innenanlage eines Relaisstellwerks. Ihre Schnittstellen entsprechen den bisherigen Schnittstellen am Kabelabschlussgestell und zur Bedien- und Meldeeinrichtung. Damit ist eine einfache Migration bestehender Stellwerke möglich. Das Sicherheitskonzept basiert auf einer zweikanaligen Struktur mit sicherem Vergleicher und zusätzlichen Selbsttests zur schnellen, datenflussunabhängigen Ausfalloffenbarung. Die erreichbare Gefährdungsrate liegt im Bereich von SIL 4 und entspricht damit dem Sicherheitsziel für Stellwerke der Deutschen Bahn. Die Transformation sieht eine Trennung der Stellwerkslogik in Logik- und Leistungsteil vor. Der Logikteil wird auf dem FPGA realisiert. Die im Leistungsteil verbliebenen Kontakte und Überwacherrelais werden durch sichere Stellteile ersetzt. Die logischen Ansteuerbedingungen der Relais werden in Schaltnetze überführt. Die gesteuerten Relais werden durch Instanzen generischer Zustandsmodelle ersetzt. Für jeden verwendeten Relaistyp wurde ein entsprechendes Modell entwickelt, das bei der Transformation als Baustein eingesetzt werden kann. Die generischen Zustandsmodelle berücksichtigen auch die sicherheitsrelevanten konstruktiven Eigenschaften der Relais. So wird bei der Auftrennung einer Schaltung in Logik- und Leistungsteil sichergestellt, dass die in getrennte Schaltungsteile überführten Öffner und Schließer eines Relais nie gleichzeitig geschlossen sein können (Zwangsführung der Kontakte). Dies ist eine Voraussetzung für die Beibehaltung der sicherheitsrelevanten Funktionsbedingungen der Originalschaltung. Das Transformationsverfahren und die implementierten Mechanismen zur Ausfalloffenbarung sind unabhängig von der Anwenderlogik und vom gewählten Schaltkreistyp. Damit kann der generierte VHDL-Code bei Obsoleszenz eines Schaltkreises auch auf andere FPGA-Typen portiert werden. In einer Ressourcenabschätzung wird gezeigt, dass der gewählte Lösungsansatz geeignet ist, die Schaltungen kleinerer Relaisstellwerke vollständig auf einem FPGA zu realisieren. Die Anwendung des vorgestellten Verfahrens wird am Beispiel der Weichengruppe des Stellwerkstyps GS II DR demonstriert. Das Transformationsverfahren ist aber auch für andere Stellwerksbauformen geeignet. Dabei ist es unerheblich, ob diese nach dem tabellarischen Verschlussplanprinzip oder dem Spurplanprinzip arbeiten.