O desenvolvimento de sistemas críticos é atualmente um dos problemas mais desafiadores enfrentados pela Engenharia. Há frequentemente uma pressão para se reduzir o tempo total de desenvolvimento, o que dificulta a entrega de sistemas com um mínimo aceitável de defeitos. Nos últimos anos, houve um aumento no tráfego aéreo, o que demanda uma modernização dos sistemas de tráfego aéreo atuais, muito dependentes na figura do controlador. Sistemas de tráfego aéreo são sistemas considerados críticos em segurança e de tempo real. O objetivo do presente trabalho é estabelecer um método de modelagem e verificação formal para sistemas críticos, com aplicação no domínio de tráfego aéreo. Com a adoção de técnicas de modelagem e verificação formal, pretende-se garantir a corretude dos sistemas frente aos requisitos inicialmente especificados e a detecção de erros em fases mais iniciais do projeto, o que resultaria em menores custos envolvidos na sua correção. São fornecidas diretivas para a aplicação do método através de um estudo de caso, baseado em três módulos de um sistema ATC em baixo nível de abstração, para a validação do funcionamento de módulos de software. Para verificação formal, é utilizada a ferramenta NuSMV e as propriedades a serem verificadas são descritas na lógica computacional de árvore (CTL) para garantir que o sistema satisfaça requisitos dos tipos vivacidade e segurança. / Developing safety critical systems is one of the most challenging problems in Engineering nowadays. There is usually a pressure to reduce the total time of the development, what makes it difficult to deliver systems with an acceptable low level of defects. In the recent years, there has been an increase in air trffic, what demands a modernization in the current air traffic systems, which are very dependent on the human controller. Air traffic systems are considered safety critical and real time systems. The objective of the present work is to establish a modeling and formal verification method for critical systems, applicable to the air traffic domain. By adopting modeling and formal verification techniques, it is expected to ensure the systems\' correctness compared with the initially specified requirements and the error detection in the initial phases of the project. Guidelines are provided for applying the method by means of a case study, based in three modules of and ATC system in a low abstraction level, for the validation of the operation of software modules. For the formal verification, it is used the NuSMV tool and the properties to be checked are described in the computational tree logic (CTL) to ensure that the system satisfies requirements of liveness and safety types.

Component-based software development has emerged as a promising approach for developing complex software systems by composing smaller independently developed components into larger component assemblies. This approach offers means to increase software reuse, achieve higher flexibility and shorter time-to-market by the use of off-the-shelf components (COTS). However, the use of COTS in safety-critical system is highly unexplored. This thesis addresses the problems appearing in component-based development of safety-critical systems. We aim at efficient reasoning about safety at system level while adding or replacing components. For safety-related reasoning it does not suffice to consider functioning components in their intended environments but also the behaviour of components in presence of single or multiple faults. Our contribution is a formal component model that includes the notion of a safety interface. It describes how the component behaves with respect to violation of a given system-level property in presence of faults in its environment. This approach also provides a link between formal analysis of components in safety-critical systems and the traditional engineering processes supported by model-based development. We also present an algorithm for deriving safety interfaces given a particular safety property and fault modes for the component. The safety interface is then used in a method proposed for compositional reasoning about component assemblies. Instead of reasoning about the effect of faults on the composed system, we suggest analysis of fault tolerance through pair wise analysis based on safety interfaces. The framework is demonstrated as a proof-of-concept in two case studies; a hydraulic system from the aerospace industry and an adaptive cruise controller from the automotive industry. The case studies have shown that a more efficient system-level safety analysis can be performed using the safety interfaces.

No description available.

Safety-critical systems are systems in which failure may lead to serious harm for humans or the environment. Due to the nature of these systems, there exist regulatory standards that recommend a set of safety mechanisms that should be included in these systems, e.g., IEC 61508. However, these standards offer little to no implementation assistance for these mechanisms. This thesis provides such development assistance, by proposing an approach for the automatic generation of safety mechanisms via Model-Driven Development (MDD). Such an automation of previously manual activities has been known to increase developer productivity and to reduce the number of bugs in the implementation. In the context of safety-critical systems, the latter also means an improvement in safety. The approach introduces a novel way to define safety requirements as structured sentences. This structure allows for the automatic parsing of these requirements in order to subsequently generate software-implemented safety mechanisms, as well as to initially configure hardware-implemented safety mechanisms. The generation approach for software-implemented safety mechanisms uses Unified Modeling Language (UML) stereotypes to represent these mechanisms in the application model. Automated model-to-model transformations parse this model representation and realize the safety mechanisms within an intermediate model. From this intermediate model, code may be generated with simple 1:1 mappings. For the generation of hardware-implemented safety mechanisms, this thesis introduces a novel Graphical User Interface (GUI) tool for representing the configuration of hardware interfaces. A template-based code snippet repository is used for generating the code responsible for the configuration of the hardware-implemented safety mechanisms. The presented approach is validated by applying it to the development of a safety-critical fire detection application example. Furthermore, the runtime overhead of the respective transformation steps of the code generation process is measured. The results indicate a linear scalability and a runtime that is no impediment to the workflow of the developer. Furthermore, the memory and runtime overhead of the generated code is evaluated. The results show that the inclusion of a single safety mechanism for a single system element has a negligible overhead. However, the relative overhead indicates that the application of safety mechanisms should be limited to those system elements that are strictly safety-critical, as their arbitrary application to all system elements would have large effects on the runtime and memory usage of the application.

<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)

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

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.

AirSim is a new simulator developed as a plugin for the Unreal Engine, aiming to be a useful tool aiding the development and testing of algorithms for autonomous vehicles. Due to AirSim still being in its infancy there is little to none research available of its possibilities or detailed guidelines and tutorials on how to use its APIs.Rust is a new systems programming language with the purpose of being safe, practical and concurrent which through design choices can solve some of the major drawbacks of the C programming language such as memory leaks, thread management, and segmentation faults.Researching the features of AirSim and its different ways of communicating, we determine the possibility of implementing a custom flight controller in Rust and C able to control a drone in the simulator and evaluate the capabilities of Rust compared to C. This is conducted by reading available documentation for AirSim, studying the source code and learning about the communication protocols used by AirSim.This thesis results in an implementation of a custom flight controller in Rust and C that controls a drone in AirSim using a communication protocol named MAVLink which enables fine-grained control of the motors. The conclusion made about the comparison of Rust and C is that both languages were able to implement the safety-critical functionality of the flight controller and that Rust provided capabilities which could be useful when developing safety-critical systems. / AirSim är en ny simulator utvecklad som ett plugin för Unreal Engine, med målet att fungera som ett hjälpmedel inom utveckling och testning av algoritmer för autonoma fordon. På grund av att AirSim fortfarande är väldigt ungt finns väldigt lite forskning tillgänglig om dess möjligheter eller detaljerade riktlinjer och beskrivningar för användningen av dess APIer.Rust är ett nytt programmeringsspråk med målet att vara säkert, praktiskt och parallellt vilket genom designval kan lösa några av de största problemen med programmeringsspråket C som till exempel minnessläckor, trådhantering och segmenteringsfel.Genom att undersöka funktionerna i AirSim och dess olika sätt att kommunicera, utforskar vi möjligheten av att utveckla en egen flygkontroller i Rust och C som kan styra en drönare i simulatorn och utvärdera Rust i förhållande till C. Detta genomförs genom att läsa tillgänglig dokumentation för AirSim, studera källkoden och lära oss de kommunikationsprotokoll som används av AirSim.Denna avhandling resulterar i implementationen av en egen flygkontroller i Rust och C som styr en drönare i AirSim med kommunikationsprotokollet MAVLink, vilket möjliggör en noggrann kontroll av motorerna. Slutsatsen gällande Rust och C är att båda språken fungerade väl för implementationen av säkerhetsritiska funktioner i flygkontrollern samt att Rust erbjöd förmågor som kan visa sig vara användbara vid utveckling av säkerhetskritiska system.

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.

Made available in DSpace on 2014-12-17T15:48:03Z (GMT). No. of bitstreams: 1 HanielMB_DISSERT.pdf: 4925062 bytes, checksum: b4c15cc32318b96fa9ccd3be61b6e7e6 (MD5) Previous issue date: 2012-11-01 / PLCs (acronym for Programmable Logic Controllers) perform control operations, receiving information from the environment, processing it and modifying this same environment according to the results produced. They are commonly used in industry in several applications, from mass transport to petroleum industry. As the complexity of these applications increase, and as various are safety critical, a necessity for ensuring that they are reliable arouses. Testing and simulation are the de-facto methods used in the industry to do so, but they can leave flaws undiscovered. Formal methods can provide more confidence in an application s safety, once they permit their mathematical verification. We make use of the B Method, which has been successfully applied in the formal verification of industrial systems, is supported by several tools and can handle decomposition, refinement, and verification of correctness according to the specification. The method we developed and present in this work automatically generates B models from PLC programs and verify them in terms of safety constraints, manually derived from the system requirements. The scope of our method is the PLC programming languages presented in the IEC 61131-3 standard, although we are also able to verify programs not fully compliant with the standard. Our approach aims to ease the integration of formal methods in the industry through the abbreviation of the effort to perform formal verification in PLCs / Controladores L?gico Program?veis (PLCs Programmable Logic Controllers, em ingl?s) desempenham fun??es de controle, recebendo informa??es do ambiente, processando-as e modificando este ambiente de acordo com os resultados obtidos. S?o comumente utilizados na ind?stria nas mais diversas aplica??es, do transporte de massa ? ind?stria do petr?leo, g?s e energias renov?veis. Com o crescente aumento da complexidade dessas aplica??es e do seu uso em sistemas cr?ticos, faz-se necess?ria uma forma de verifica??o que propicie mais confian?a do que testes e simula??o, padr?es mais utilizados na ind?stria, mas que podem deixar falhas n?o tratadas. M?todos formais podem prover maior seguran?a a este tipo de sistema, uma vez que permitem a sua verifica??o matem?tica. Neste trabalho fazemos uso do M?todo B, que ? usado com sucesso na ind?stria para a verifica??o de sistemas cr?ticos, possui amplo apoio ferramental e suporte ? decomposi??o, refinamento e verifica??o de corretude em rela??o ? especifica??o atrav?s de obriga??es de prova. O m?todo desenvolvido e apresentado aqui consiste em gerar automaticamente modelos B a partir de programas para PLCs e verific?-los formalmente em rela??o a propriedades de seguran?a, estas derivadas manualmente a partir dos requisitos do sistema. O escopo do trabalho s?o as linguagens de programa??o para PLCs do padr?o IEC 61131-3, mas sistemas com linguagens que apresentem modifica??es em rela??o ao padr?o tamb?m s?o suportados. Esta abordagem visa facilitar a integra??o de m?todos formais na ind?stria atrav?s da diminui??o do esfor?o para realizar a verifica??o formal de PLCs