<p>Formal methods such as Event-B are a widely used approach for developing critical systems. This thesis demonstrates that creating models and proving the consistency of the models at the requirements level during software (system) development is an effective way to reduce the occurrence of faults and errors in a practical application. An insulin infusion pump (IIP) is a complicated and time critical system. This thesis uses Event-B to specify models for an IIP, based on a draft requirements document developed by the US Food and Drug Administration (FDA). Consequently it demonstrates Event-B can be used effectively to detect the missing properties, the missing quantities, the faults and the errors at the requirements level of a system development. The IIP is an active and reactive time control system. To achieve the goal of handling timing issues in the IIP system, we made extensions of an existing time pattern specified using Event-B to enrich the semantics of the Event-B language. We created several sets to model the activation times of different events and the union of these time sets defines a global time activation set. The tick of global time is specified as a progress tick event. All the actions in an event are triggered only when the global time in the time tick event matches the time specified in the event. Time is deleted from the corresponding time set, but not the corresponding global time set while the event is triggered. A time point is deleted from the global time set only when there are no pending actions for that time point. Through discharging proof obligations using Event-B, we achieved our goal of improving the requirements document.</p> / Master of Computer Science (MCS)

This thesis project, conducted in collaboration with Scandinavian Airlines (SAS), investigates how safety-critical internal systems can be designed to enhance usability and user experience through an examination of the Aerodrome Approval system at SAS. Employing a research-through-design approach and utilizing heuristic evaluations, semi-structured interviews, contextual inquiries, and a redesign process, several guidelines for improving usability and user experience have been identified. Key insights reveal that optimizing login functionalities can enhance security and role-specific access, thereby reducing errors and improving the user experience. Consistency in design elements and adherence to standards play a critical role in usability, aiding in error prevention and improving system navigation efficiency. Additionally, effective strategies for error prevention, such as contextual warnings tailored to specific conflicts, help maintain workflow efficiency and prevent user fatigue, whereas ensuring a balanced and timely presentation of information is essential to prevent information overload while still ensuring access to critical data. The project illustrates how multiple usability principles are interconnected yet sometimes conflicting and emphasizes the need to further investigate safety-critical internal systems to a broader extent to be able to identify more generalizable design guidelines in the future.

In den letzten Jahren hat die Verbreitung von Elektrofahrrädern, sogenannten Pedelecs, stark zugenommen. Dies ist vor dem Hintergrund der Umweltfreundlichkeit und Gesundheitsförderlichkeit dieser Form der Fortbewegung zunächst grundsätzlich positiv zu bewerten. Gleichzeitig besteht jedoch die Sorge, dass Elektrofahrradfahrer häufiger und in schwerere Unfälle verwickelt werden könnten als Fahrradfahrer. So bieten motorgestützte Elektrofahrräder das Potential, höhere Geschwindigkeiten zu erreichen als konventionelle Fahrräder, und werden zudem vor allem von älteren Verkehrsteilnehmern genutzt. Nicht zuletzt deswegen könnten sich durch diese neue Mobilitätsform auch neue Herausforderungen für die Verkehrs-, insbesondere Radinfrastrukturen ergeben. Tatsächlich jedoch blieben die Auswirkungen auf die Verkehrssicherheit bisher weitestgehend ungeklärt. Um dieser Problematik zu begegnen, wurde im Rahmen einer Naturalistic Cycling Studie (NCS) und mehreren experimentellen Untersuchungen folgenden Fragen nachgegangen: Fahren Elektrofahrradfahrer tatsächlich schneller als nicht-motorisierte Radfahrer? Wie wirken sich diese potentiell höheren Geschwindigkeiten darauf aus, wie Elektrofahrradfahrer von Autofahrern wahrgenommen werden? Welchen Einfluss hat das Alter der Radfahrer auf die Geschwindigkeiten und auch auf deren Neigung zu Unfällen bzw. sicherheitskritischen Situationen im Verkehr? Und welchen Einfluss hat die Infrastruktur auf die gewählten Geschwindigkeiten und die Auftretenshäufigkeit von kritischen Situationen? Diese und weitere Fragen wurden in insgesamt vier Arbeiten, die in internationalen Fachzeitschriften publiziert sind (I - IV), beleuchtet. Im ersten Artikel werden die Geschwindigkeiten von Fahrradfahrern (n = 31) im Gegensatz zu Pedelecfahrern (n = 49; Motorunterstützung bis 25 km/h) sowie S-Pedelecfahrern (n = 10; Motorunterstützung bis 45 km/h) betrachtet. Als Einflussgrößen wurden das Alter und die Nutzung verschiedener Infrastrukturtypen der Probanden ausgewertet. Alle Räder wurden mit einem Datenaufzeichnungssystem inklusive Kameras und Geschwindigkeitssensoren ausgestattet, um für vier Wochen ein Bild des natürlichen Fahrverhaltens zu erhalten. Unabhängig von der Infrastruktur waren S-Pedelecfahrer schneller unterwegs waren als Fahrrad- und Pedelecfahrer. Pedelecfahrer fuhren ebenfalls signifikant schneller als konventionelle Fahrradfahrer. Die höchsten Geschwindigkeiten wurden für alle Radtypen auf der (mit dem motorisierten Verkehr geteilten) Fahrbahn sowie der Radinfrastruktur gemessen. Das Alter der Fahrer hatte ebenfalls einen signifikanten Einfluss auf die Geschwindigkeit: Unabhängig vom Fahrradtyp waren ältere Fahrer (65 Jahre und älter) deutlich langsamer als Probanden jüngerer Altersgruppen (41-64 Jahre sowie 40 Jahre und jünger). Die beiden jüngeren Altersgruppen fuhren selbst ohne Motorunterstützung (konventionelles Fahrrad) schneller als die älteren Pedelecfahrer. Genauere Analysen (wie etwa das Verhalten beim Bergabfahren) legen nahe, dass dieser Befund nicht allein der physischen Leistungsfähigkeit zugeschrieben werden kann. Es scheint vielmehr so, als ob ältere Fahrrad- und Elektroradfahrer durch die geringere Geschwindigkeit versuchen, Defizite in der Reaktionsgeschwindigkeit auszugleichen bzw. generell vorsichtiger fahren. Der zweite Artikel beschäftigt sich mit der Frage, inwieweit sich die Art und Häufigkeit von Unfällen und kritischen Situationen bei den drei verschiedenen Altersgruppen unterscheiden. Auch hier wurde auf die Daten aus der NCS zurückgegriffen, auf deren Basis eine umfassende Videokodierung durchgeführt wurde. Es zeigten sich keine Unterschiede zwischen den Altersgruppen hinsichtlich des Auftretens kritischer Situationen; weder in Bezug auf die absolute Anzahl, noch gemessen an der relativen Häufigkeit (pro 100 km). Ebenfalls keine Zusammenhänge fanden sich zwischen dem Alter der Fahrer und der Art von Konfliktpartnern oder der Tageszeit der kritischen Situationen. Auch hier scheint es so, dass Ältere keinem erhöhten Risiko unterliegen, und etwaige altersbedingte Einschränkungen kompensieren können. Bei der Betrachtung des Einflusses des Infrastrukturtyps auf das Auftreten von kritischen Situationen zeigte sich, dass, bezogen auf die zurückgelegten Wegstrecken, die Nutzung der mit dem motorisierten Verkehr geteilten Fahrbahn als relativ sicher einzustufen ist. Demgegenüber ergab sich ein erhöhtes Risiko für Unfälle oder kritische Situationen auf designierter Radinfrastruktur. Dies widerspricht der Wahrnehmung vieler Radfahrer, die diese Infrastruktur als besonders sicher empfinden. Es ist allerdings anzunehmen, dass diese Wahrnehmung nicht nur auf der vermeintlichen Auftretenshäufigkeit, sondern auch auf dem angenommenen Schweregrad einer möglichen Kollision beruht. Zwei weitere Artikel beschäftigen sich damit, wie Autofahrer die Geschwindigkeit beziehungsweise die Annäherung von Elektrofahrrädern wahrnehmen. Dies ist insbesondere in Kreuzungssituationen relevant, in denen Autofahrer abschätzen müssen, ob sie noch rechtzeitig vor einem Fahrrad abbiegen können ohne mit diesem zu kollidieren. Es wurde vermutet, dass die fehlende Erfahrung mit Elektrofahrrädern und der von ihnen erreichbaren Geschwindigkeit vermehrt zu entsprechenden Unfällen führen könnte. Der Frage wurde mit einem Experiment zur Lückenakzeptanz auf der Teststrecke (Artikel III) und einer Videostudie zu Schätzungen von Zeitlückengrößen (Artikel IV) nachgegangen. Es zeigte sich, dass Autofahrer die verbleibende Zeit bis zur Kollision für Elektrofahrradfahrer geringer einschätzten als für konventionelle Radfahrer. Zudem wählten Autofahrer bei einem herannahenden Elektrofahrrad signifikant kleinere Zeitlücken zum Abbiegen, als bei einem konventionellen Fahrrad. Dieser Effekt verstärkte sich sogar noch, wenn die Geschwindigkeit des herannahenden Zweirades zunahm. Diese Befunde legen nahe, dass die Einschätzung der Geschwindigkeit beziehungsweise Annäherung von Elektrofahrrädern durchaus risikobehaftet ist. Die Ergebnisse dieser Arbeit helfen dabei, die Auswirkungen der steigenden Verbreitung von Elektrofahrrädern auf die Verkehrssicherheit einzuschätzen. Auch erlauben es die Erkenntnisse, Maßnahmen zur Erhöhung der Verkehrssicherheit für Fahrrad- und Elektrofahrradfahrern aller Altersgruppen abzuleiten. Damit leistet diese Arbeit einen Beitrag zur Unterstützung einer sicheren, gesunden und umweltfreundlichen Mobilität. / Electric bicycles (e-bikes) are a relatively new form of transport. The aim of this dissertation is to investigate their effects on road safety. In 2012, at the beginning of this dissertation project, knowledge of e-bikes in general and their impact on road safety in particular was relatively scarce. As a starting point of this work, the influence of e-bikes on road safety was investigated compared relative to the road safety of conventional bicycles. Additionally, the influence of the age of the rider on safety is considered as a supplementary factor. Special attention is paid to the impact of the infrastructure utilised by riders and its characteristics. This cumulative dissertation consists of four research articles, labelled Paper I to IV accordingly. Papers I to IV have been published in peer reviewed journals. The synopsis provides an overview of previous research as well as a theoretical framework of the safety of cyclists and e-bike riders. Speed, and its perception through other road users (measured with experiments to gap acceptance and time to arrival (TTA) estimates) are considered as relevant factors for road safety. In Chapter 4, the research objectives are presented in detail. The methodology is clarified in Chapter 5, and in Chapter 6 and 7 the results are summarised and discussed. The implications of the results are considered in Chapter 8. In Paper I, the differences in speed between bicycles, pedelecs (pedal electric cycle, motor assistance up to 25 km/h) and S-pedelecs (pedal electric cycle, motor assistance up to 45 km/h) were investigated. Additionally the influence of infrastructure type, road gradient and the age of the rider were taken into account. Paper II is concerned with the influence of different conflict partners in crashes, and the utilisation of infrastructure on the safety of cyclists. For this purpose, safety critical events (SCE) involving cyclists were examined, with a special focus on the differences between younger, middle aged, and older cyclists. Papers III and IV focus on the perception of speed of e-bike and bicycle riders through other road users and its implications for road safety. Paper III specifically deals with the gap acceptance of car drivers at intersections in the presence of cyclists and e-bike riders with different speeds and under varying conditions (e.g. at intersections with different road gradients). Paper IV looks at drivers TTA estimates of approaching bicycles and e-bikes in combination with other influencing factors (e.g. speed, cyclist age).

Cette thèse présente une nouvelle approche pour la modélisation des systèmes de sécurité fonctionnelle qui prend en compte plusieurs modes de défaillance pour les composants et le système global. Les diagrammes de flux d'information (IFDs) ont été initialement développé dans un thèse précédent. Dans ce travail, l'évaluation si l'approche flux d'information être rendue plus efficace par utiliser les diagrammes de décision binaires (BDD).Cette thèse sera d'expliquer pourquoi ce modèle est nécessaire et pratique, suivie d'une explication détaillée des IFDs. Cela inclut sa structure hiérarchique et comment ce modèle peut être appliqué.La prochaine étape est la formalisation du modèle IFD original pour permettre l'utilisation des techniques d'évaluation plus efficaces. Il sera expliqué pourquoi ces étapes de formalisation ont été prises et les avantages de leur utilisation.Ensuite une explication détaillée des algorithmes développés est présenté. Ces algorithmes sont basés sur une combinaison de différentes techniques de BDD. Zero Suppressed BDDs (ZBDDs) sont combinées avec des Boolean Expression Diagrams (BEDs). En outre, la structure des IFD est utilisé pour construire un BDD global sur plusieurs petits BDDs. Cela augmente l'efficacité du processus d'évaluation.Les techniques présentées sont évaluées par l'analyse de plusieurs cas d'utilisation qui sont expliqués dans ce travail / This thesis presents a novel approach for modelling safety critical systems which takes into account several failure modes both for components and the global system. The so called Information Flow Diagrams (IFDs) were originally developed in a previous PhD-thesis. In this work, the evaluation if the IFD-approach should be made more efficient by using Binary Decision Diagrams (BDDs).This thesis will explain why such a model is necessary and practical, followed by a detailed explanation of the IFD-model. This includes its hierarchical structure and how this model can be applied. The next step is to formalise the original IFD-model in order to enable more efficient evaluation techniques. It will be explained why these formalisation steps were taken and what was gained by using them. Afterwards a detailed explanation of the developed algorithms is presented. These algorithms are based on a combination of different BDD-techniques. Zero Suppressed BDDs (ZBDDs) are combined with Boolean Expression Diagrams (BEDs). Furthermore, the structure of the IFDs is used in order to construct a large BDD out of several smaller BDDs. This increases the efficiency of the evaluation process.The presented techniques are evaluated by analysing several use cases which are explained in this work

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.

The ever-increasing functional and nonfunctional requirements in real-time safety-critical embedded systems call for new design flows that solve the specification, validation, and synthesis problems. Ensuring key properties, such as functional determinism and temporal predictability, has been the main objective of many embedded system design models. Dataflow models of computation (such as KPN, SDF, CSDF, etc.) are widely used to model stream-based embedded systems due to their inherent functional determinism. Since the introduction of the (C)SDF model, a considerable effort has been made to solve the static-periodic scheduling problem. Ensuring boundedness and liveness is the essence of the proposed algorithms in addition to optimizing some nonfunctional performance metrics (e.g. buffer minimization, throughput maximization, etc.). However, nowadays real-time embedded systems are so complex that real-time operating systems are used to manage hardware resources and host real-time tasks. Most of real-time operating systems rely on priority-driven scheduling algorithms (e.g. RM, EDF, etc.) instead of static schedules which are inflexible and difficult to maintain. This thesis addresses the real-time scheduling problem of dataflow graph specifications; i.e. transformation of the dataflow specification to a set of independent real-time tasks w.r.t. a given priority-driven scheduling policy such that the following properties are satisfied: (1) channels are bounded and overflow/underflow-free; (2) the task set is schedulable on a given uniprocessor (or multiprocessor) architecture. This problem requires the synthesis of scheduling parameters (e.g. periods, priorities, processor allocation, etc.) and channel capacities. Furthermore, the thesis considers two performance optimization problems: buffer minimization and throughput maximization.

Les arguments de sécurité sont couramment utilisés pour montrer que des efforts suffisants ont été faits pour atteindre les objectifs de sécurité. Ainsi, la sécurité du système est souvent justifiée par l'évaluation des arguments de sécurité. L'évaluation de tels arguments repose généralement sur l’avis d’experts sans s’appuyer sur des outils ou des méthodes dédiés. Ceci pose des questions sur la validité des résultats. Dans cette thèse, une approche quantitative est proposée, basé sur la théorie de Dempster-Shafer (théorie D-S) pour évaluer notre confiance dans les arguments de sécurité. Cette approche gère le problème à travers les aspects suivants: 1) Définition formelle de la confiance dans les arguments basée sur la théorie D-S; 2) Développement de règles d'agrégation des paramètres de confiance; 3) Proposition d'un cadre d'évaluation quantitatif des arguments de sécurité. Une application dans le domaine ferroviaire conduit à l'estimation des paramètres du cadre par une enquête auprès d'experts en sécurité. / Safety arguments, also called Safety Cases, are commonly used to present that adequate efforts have been made to achieve the safety goals. Thus, the system safety is often justified through assessing the safety arguments. The assessment of such arguments is usually implemented by experts without any dedicated tool or method. This leads to a questionable validity of the results. In this thesis, a quantitative framework is proposed based on Dempster-Shafer theory (D-S theory) to assess our confidence in Safety Cases. This framework manages the issue in following aspects: 1) Formal definition of confidence in arguments based on D-S theory; 2) Development of confidence aggregation rules; 3) Proposition of a quantitative assessment framework of safety arguments. An application in railway domain realises the parameter estimation of the framework by a survey with safety experts.

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 number of logical code coverage criteria have been used throughout the years in the testing of safety-critical software. Kaminski, et al. proposed Relational Operator Replacement Global (RORG), a method to bring benefits from ROR mutation to Modified Condition / Decision Coverage (MCDC), which is widely used in the avionics industry. However, there is a lack of studies in the industry to support this method. In this thesis, we report on the results of applying RORG to avionic code, augmenting an MCDC adequate test set to satisfy RORG, evaluating its ability to find real faults in industrial software. Conclusions drawn from this thesis are: (1) Faults in relational operators in avionic code are rare, no faults were found in this study. (2) 24% of the relational operators in our study would require additional software requirements to be verified for RORG coverage. (3) 37% of the relational operators in our study were infeasible to test due to program semantics. (4) 84% of the tests added covered enumeration comparisons.

The number and complexity of the systems realizing the functionality of the machines in the automotive domain are growing. In this arises the need for a systematic way to manage their development. As the technologies advance, the vehicles introduce an increasing range of capabilities. However, they have similar functions, which have the potential to be reused. One of the widely used approaches that manages the commonality and variability of the development artifacts in a systematic manner is Product Line Engineering (PLE). Consequently, PLE reduces the time to market and the development cost. The machines, realized in the automotive domain, interact with their operators and the surrounding environment. Possible malfunctions of the machines may introduce a risk of accidents with fatal consequences. Therefore, the products should be analyzed, developed and managed in a safe manner and certified according to different relevant safety standards like ISO 15998, ISO 61508 and ISO 26262. There is a diversity of functions in a Product Line (PL). Some of them are mandatory for all machines and others are optional for some models. This gives the opportunity to combine the functions in multiple configurations. However, not all combinations are possible due to dependencies among the functions. Furthermore, the configurations should be valid from a safety perspective, and the developed products should satisfy the requirements identified during the safety analysis. The above mentioned factors emphasize the need for explicit representation of the systems' characteristics, such as commonality and variability, functional dependencies and quality attributes. The purpose of the current work is to find an efficient way to satisfy this need. The scope of our research is limited to the automotive domain. In order to gain familiarity with the state of practice, we collaborated with Volvo Construction Equipment (Volvo CE) as an industrial partner. In particular, we: conducted an informal interview study with the practitioners, analyzed the requirements management tool used in Volvo CE and studied products typical for the domain in detail, examined the deliverables defined in the related domain specific safety standards. We gained knowledge on how variability is managed in an industrial context today, which safety aspects need to be considered and how functional safety artifacts are managed with regards to variability. We synthesized the characteristics that are explicitly represented during the development and safety certification of the products in a safety-critical product line. We identified the challenges that the practitioners meet today and the areas that need to be improved. As a result, we formulated evaluation criteria for search and assessment of possible solutions. Subsequently we searched in the literature for different modeling techniques, that are able to respond to the industrial needs, and found the following to be relevant in our context: Feature modeling techniques consider the different variability types and dependencies among the features. Model-based development techniques can represent different views of the system on each level of the development process. Orthogonal modeling techniques extract the variability and dependencies in a different view. Furthermore, we evaluated the methods found during the literature study, based on the proposed criteria. We concluded that the examined techniques alone cannot represent all characteristics needed to support the development of a safety-critical product line, especially the impact of the variability on the safety and vice versa. However, each of them focuses on the presentation of certain aspect of the product line, which can help in building a more complete representation. Thus we focused on the approaches that may be extended and integrated into a complete solution. As a result, we propose a model and graphical notation for variability management in safety-critical product lines, which takes the identified industrial needs into account. The concept is depicted graphically by several model-based diagrams, which represent the different aspects of the product line, on each development level. Special attention is paid to the representation of the safety and variability aspects of the systems. The method is exemplified on an industrial example, in order to show how it achieves the defined goals.