This thesis belongs to the domain of software verification. The goalof verifying software is to ensure that an implementation, a program,satisfies the requirements, the specification. This is especiallyimportant for critical computer programs, such as control systems forair planes, trains and power plants. Here a malfunctioning occurringduring operation would have catastrophic consequences. Software requirements can concern safety or functioning. Safetyrequirements, such as not accessing memory locations outside validbounds, are often implicit, in the sense that any implementation isexpected to be safe. On the other hand, functional requirementsspecify what the program is supposed to do. The specification of aprogram is often expressed informally by describing in English or someother natural language the mission of a part of the program code.Usually program verification is then done by manual code review,simulation and extensive testing. But this does not guarantee that allpossible execution cases are captured. Deductive program proving is a complete way to ensure soundness of theprogram. Here a program along with its specificationis a mathematical object and its desired properties are logicaltheorems to be formally proved. This way, if the underlying logicsystem is consistent, we can be absolutely sure that the provenproperty holds for the program in any case.Generation of verification conditions is a technique helpingthe programmer to prove the properties he wants about his programs.Here a VCG tool analyses a program and its formal specification andproduces a mathematical formula, whose validity implies the soundnessof the program with respect to its specification. This is particularlyinteresting when the generated formulas can be proved automatically byexternal SMT solvers.This approach is based on works of Hoare and Dijkstra and iswell-understood and shown correct in theory. Deductive verificationtools have nowadays reached a maturity allowing them to be used inindustrial context where a very high level of assurance isrequired. But implementations of this approach must deal with allkinds of language features and can therefore become quite complex andcontain errors -- in the worst case stating that a program correcteven if it is not. This raises the question of the level ofconfidence granted to these tools themselves. The aim of this thesis is to address this question. We develop, inthe Coq system, a certified verification-condition generator (VCG) forACSL-annotated C programs.Our first contribution is the formalisation of an executableVCG for the Whycert intermediate language,an imperative language with loops, exceptions and recursive functionsand its soundness proof with respect to the blocking big-step operational semantics of the language.A second contribution is the formalisation of the ACSL logicallanguage and the semantics of ACSL annotations of Compcert's Clight.From the compilation of ACSL annotated Clight programs to Whycertprograms and its semantics preservation proof combined with a Whycertaxiomatisation of the Compcert memory model results our maincontribution: an integrated certified tool chainfor verification of C~programs on top of Compcert. By combining oursoundness result with the soundness of the Compcert compiler we obtaina Coq theorem relating the validity of the generated proof obligationswith the safety of the compiled assembly code.

Depuis plusieurs années, le marché des circuits intégrés numériques requiert des systèmes de plus en plus complexes dans un temps toujours plus réduit. Afin de répondre à ses deux exigences, les industriels de la conception font appel à des fournisseurs externes proposant des circuits fonctionnant sur des signaux d'horloge dédiés. Lorsque ces derniers communiquent entre eux, les horloges d'émission et de réception ne sont pas les mêmes, on parle de « Clock Domain Crossing » (CDC).Les CDC correspondent à des communications asynchrones et peuvent provoquer des dysfonctionnements critiques. Par ailleurs, ces problèmes étant intermittents et complexes à analyser, ils ne peuvent pas être exhaustivement vérifiés avec des méthodes telles que l’analyse de timing ou la simulation fonctionnelle. Avec l'augmentation du nombre de CDC dans les circuits, les industriels de la conception assistée par ordinateur (EDA) ont proposé des solutions logicielles spécialisées dans la vérification statique des CDC. Cependant, les circuits développés étant en constante évolution, les outils ne sont pas en mesure de s’adapter. Pour pallier ces problèmes, la vérification industrielle des CDC est basée sur la spécification de contraintes et d'exclusions par l'utilisateur. Ces actions, qui se substituent aux outils, peuvent masquer des bugs. De plus, l’effort humain requis par cette approche n’est pas compatible avec le temps alloué au développement de circuits industriels. Nous avons donc cherché à automatiser la vérification en proposant des solutions basées sur des propriétés formelles. Les travaux ont consisté à analyser les différentes techniques de conception et de vérification des CDC à travers l’évaluation des principaux outils du marché. A partir des résultats obtenus, nous avons formalisé les problèmes pratiques et proposé des modèles permettant d’obtenir des résultats exhaustifs automatiquement. Les essais ont été réalisés sur un sous-système à base de processeurs (CPUSS) développé chez STMicroelectronics. L'adoption de nos modèles permet une vérification complète des CPUSS de manière automatique ce qui est essentiel dans un environnement industriel compétitif. En effet, le nombre d’informations devant être spécifiées par l’utilisateur a été réduit de moitié pour chacun des outils évalués. Par ailleurs, ces travaux ont montré que l’axe de développement des outils CDC avec l’ajout de fonctionnalités telles que les flots hiérarchiques ou l’injection de fautes n’améliore pas la qualité de résultats. Une collaboration ayant été mise en place avec les principaux fournisseurs outils, certaines solutions seront probablement intégrées aux outils dans les années à venir. / For several years now, the digital IC market has been requiring both more complex systems and reduced production times. In this context, the semiconductor chip maker companies call on external IP providers offering components working on dedicated clock signals. When these IPs communicate between them, the source and destination clocks are not the same, we talk about "Clock Domain Crossing" (CDC).CDC correspond to asynchronous communications and can cause critical failures. Furthermore, due to the complexity and the random nature of CDC issues, they can not be exhaustively checked with methods such as timing analysis or functional simulation. With the increase of CDC in the digital designs, EDA tools providers have developed software solutions dedicated to CDC static verification.Whereas, the designs are subject to continuous change, the verification tools are not able to be up to date. To resolve these practical issues, the CDC industrial verification is based on the specification of constraints and exclusions by the user. This manual flow, which replaces the tools, can mask bugs. Moreover, the human effort required by this approach is incompatible with the time allowed to industrial designs development.Our goal has been to automate the verification submitting solutions based on formal properties.The work consisted in the analysis of the different CDC design and verification approaches through the evaluation of main CDC checker tools. From the results obtained, we have formalized the practical problems and proposed models to obtain automatically exhaustive results. The tests have been performed on a processor-based subsystem (CPUSS) developed at STMicroelectronics.Adopting our models enables a complete checking of CPUSS in an automatic way, which is essential within a competitive industrial environment. Actually, the amount of information to be specified by the user has been reduced by half for each one of the evaluated tools. Otherwise, this work has shown that the development axis of the CDC tools despite the addition of functionalities such as hierarchical flows or fault injection, doesn’t improve the quality of results (QoR). Since a collaboration has been established with the main tool providers some solutions would probably be included into the tools over the coming years.

This thesis describes the primary goal of the HelenOS microkernel multiserver operating system. The primary goal of the HelenOS project is to create a comprehensive research and development platform in the domain of general-purpose operating systems that would support state-of-the-art approaches and methods (such as verification of correctness) while at the same time focusing on practical relevance. The text of the thesis describes what specific means in terms of design (based on software components), implementation, development process and verification are used to achieve the primary goal. The thesis also evaluates the current state of HelenOS. Powered by TCPDF (www.tcpdf.org)

This work presents a method to perform formal and dynamic verification of concurrent software. The objective is to provide a method capable of identifying problems in programs whose execution is based on multiple threads, and analyze behavioral properties. The method is able to detect problems in concurrent software, as well as check conformity of the concurrent software with desirable behavior, based on information collected dynamically, i.e. at runtime. The information collected consists of the software execution flow as well as data about the way communicate the software components during this run. The data collected reflect the software's execution, which ensures greater confidence to the information collected. This information is analyzed to identify deadlocks and race conditions in a process called Dynamic Analysis. In addition, this information is also used to automatically generate a model that describes the behavior of a software, which is used for verification of behavioral properties. This process is called Formal Verification. The automatic model generation eliminates the need for manual construction of the model, which requires much effort and knowledge of formal methods, this can increase costs and development time software. However, the dynamic analysis is known to only perform coverage of the current behavior of competing software systems. Current behavior is one that occurs only during an execution of concurrent software systems, without considering all other possible behaviors from the non-determinism. Due to the non-determinism, concurrent software can produce different results for the same input to each execution of software. Therefore reproduce the behavior that leads to competitive software failure is a complex task. This paper proposes a method to perform formal verification and dynamic concurrent software capable of capturing the non-deterministic behavior of these systems and provide reduced development costs by eliminating the need for manual construction of concurrent software system models. The method is validated by a case study consists of three test software systems. / Fundação de Amparo a Pesquisa do Estado de Alagoas / Neste trabalho é apresentado um método para verificação formal e dinâmica de software concorrentes. O objetivo é oferecer um método capaz de identificar problemas inerentes a programas cuja execução baseia-se em múltiplas threads, além de analisar propriedades comportamentais descritas com base nos preceitos da lógica temporal. Propõe-se um método capaz de detectar problemas e verificar formalmente a adequação da execução de sistemas de software concorrentes com relação ao comportamento desejável a tais sistemas, baseando-se em informações coletadas dinamicamente, ou seja, em tempo de execução. As informações coletadas correspondem às sequências de execução de sistemas de software, bem como dados sobre a maneira como se comunicam seus componentes durante sua execução. Os dados colhidos refletem a execução do sistema de software propriamente dito, o que garante maior confiança às informações coletadas. Tais informações são analisadas de modo a identificar impasses e condições de corrida em um processo denominado Análise Dinâmica. Ademais, estas informações também são utilizadas para geração automática de um modelo que descreve o comportamento do sistema de software, o qual é utilizado para verificação de propriedades comportamentais. A este processo de verificação dá-se o nome de Verificação Formal. A geração automática do modelo elimina a necessidade de construção manual do mesmo, que requer muito esforço e conhecimento acerca de métodos formais, isso pode aumentar custos e tempo de desenvolvimento do sistema de software. Entretanto, a análise dinâmica é conhecida por apenas realizar cobertura sobre o comportamento atual de sistemas de software concorrentes, sem considerar a análise de todas as outras possíveis sequências de execuções devido ao não determinismo. Em razão do comportamento não determinístico, sistemas de software concorrentes são capazes de produzir resultados diferentes para a mesma entrada a cada nova execução. Deste modo, reproduzir o comportamento que leva sistemas de software concorrente à falha é uma tarefa complexa. O presente trabalho propõe um método para realizar verificação formal e dinâmica de sistemas de software concorrente capaz de capturar o comportamento não determinístico desses sistemas, além de proporcionar a redução de custos de desenvolvimento através da eliminação da necessidade de construção manual de modelos de sistemas de software concorrente. O método é validado através de um estudo de caso composto por testes em três sistemas de software.

Problems in formal verification are often stated in terms of finite automata and extensions thereof. In this thesis we investigate several such algorithmic problems. In the first part of the thesis we develop a theory of completeness thresholds in Bounded Model Checking. A completeness threshold for a given model M and a specification φ is a bound k such that, if no counterexample to φ of length k or less can be found in M, then M in fact satisfies φ. We settle a problem of Kroening et al. [KOS⁺11] in the affirmative, by showing that the linearity problem for both regular and ω-regular specifications (provided as finite automata and Buchi automata respectively) is PSPACE-complete. Moreover, we establish the following dichotomies: for regular specifications, completeness thresholds are either linear or exponential, whereas for ω-regular specifications, completeness thresholds are either linear or at least quadratic in the recurrence diameter of the model under consideration. Given a formula in a temporal logic such as LTL or MTL, a fundamental problem underpinning automata-based model checking is the complexity of evaluating the formula on a given finite word. For LTL, the complexity of this task was recently shown to be in NC [KF09]. In the second part of the thesis we present an NC algorithm for MTL, a quantitative (or metric) extension of LTL, and give an AC¹ algorithm for UTL, the unary fragment of LTL. We then establish a connection between LTL path checking and planar circuits which, among others, implies that the complexity of LTL path checking depends on the Boolean connectives allowed: adding Boolean exclusive or yields a temporal logic with P-complete path-checking problem. In the third part of the thesis we study the decidability of the reachability problem for parametric timed automata. The problem was introduced over 20 years ago by Alur, Henzinger, and Vardi [AHV93]. It is known that for three or more parametric clocks the problem is undecidable. We translate the problem to reachability questions in certain extensions of parametric one-counter machines. By further reducing to satisfiability in Presburger arithmetic with divisibility, we obtain decidability results for several classes of parametric one-counter machines. As a corollary, we show that, in the case of a single parametric clock (with arbitrarily many nonparametric clocks) the reachability problem is NEXP-complete, improving the nonelementary decision procedure of Alur et al. The case of two parametric clocks is open. Here, we show that the reachability is decidable in this case of automata with a single parameter.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

Gramática de grafos é uma linguagem formal bastante adequada para sistemas cujos estados possuem uma topologia complexa (que envolvem vários tipos de elementos e diferentes tipos de relações entre eles) e cujo comportamento é essencialmente orientado pelos dados, isto é, eventos são disparados por configurações particulares do estado. Vários sistemas reativos são exemplos desta classe de aplicações, como protocolos para sistemas distribuídos e móveis, simulação de sistemas biológicos, entre outros. A verificação de gramática de grafos através da técnica de verificação de modelos já é utilizada por diversas abordagens. Embora esta técnica constitua um método de análise bastante importante, ela tem como desvantagem a necessidade de construir o espaço de estados completo do sistema, o que pode levar ao problema da explosão de estados. Bastante progresso tem sido feito para lidar com esta dificuldade, e diversas técnicas têm aumentado o tamanho dos sistemas que podem ser verificados. Outras abordagens propõem aproximar o espaço de estados, mas neste caso não é possível a verificação de propriedades arbitrárias. Além da verificação de modelos, a prova de teoremas constitui outra técnica consolidada para verificação formal. Nesta técnica tanto o sistema quanto suas propriedades são expressas em alguma lógica matemática. O processo de prova consiste em encontrar uma prova a partir dos axiomas e lemas intermediários do sistema. Cada técnica tem argumentos pró e contra o seu uso, mas é possível dizer que a verificação de modelos e a prova de teoremas são complementares. A maioria das abordagens utilizam verificadores de modelos para analisar propriedades de computações, isto é, sobre a seqüência de passos de um sistema. Propriedades sobre estados alcançáveis só são verificadas de forma restrita. O objetivo deste trabalho é prover uma abordagem para a prova de propriedades de grafos alcançáveis de uma gramática de grafos através da técnica de prova de teoremas. Propõe-se uma tradução (da abordagem Single-Pushout) de gramática de grafos para uma abordagem lógica e relacional, a qual permite a aplicação de indução matemática para análise de sistemas com espaço de estados infinito. Definiu-se gramática de grafos utilizando estruturas relacionais e aplicações de regras com linguagens lógicas. Inicialmente considerou-se o caso de grafos (tipados) simples, e então se estendeu a abordagem para grafos com atributos e gramáticas com condições negativas de aplicação. Além disso, baseado nesta abordagem, foram estabelecidos padrões para a definição, codificação e reuso de especificações de propriedades. O sistema de padrões tem o objetivo de auxiliar e simplificar a tarefa de especificar requisitos de forma precisa. Finalmente, propõe-se implementar definições relacionais de gramática de grafos em estruturas de event-B, de forma que seja possível utilizar os provadores disponíveis para event-B para demonstrar propriedades de gramática de grafos. / Graph grammars are a formal language well-suited to applications in which states have a complex topology (involving not only many types of elements, but also different types of relations between them) and in which behaviour is essentially data-driven, that is, events are triggered basically by particular configurations of the state. Many reactive systems are examples of this class of applications, such as protocols for distributed and mobile systems, simulation of biological systems, and many others. The verification of graph grammar models through model-checking is currently supported by various approaches. Although model-checking is an important analysis method, it has as disadvantage the need to build the complete state space, which can lead to the state explosion problem. Much progress has been made to deal with this difficulty, and many techniques have increased the size of the systems that may be verified. Other approaches propose to over- and/or under-approximate the state-space, but in this case it is not possible to check arbitrary properties. Besides model checking, theorem proving is another wellestablished approach for verification. Theorem proving is a technique where both the system and its desired properties are expressed as formulas in some mathematical logic. A logical description defines the system, establishing a set of axioms and inference rules. The process of verification consists of finding a proof of the required property from the axioms or intermediary lemmas of the system. Each verification technique has arguments for and against its use, but we can say that model-checking and theorem proving are complementary. Most of the existing approaches use model checkers to analyse properties of computations, that is, properties over the sequences of steps a system may engage in. Properties about reachable states are handled, if at all possible, only in very restricted ways. In this work, our main aim is to provide a means to prove properties of reachable graphs of graph grammar models using the theorem proving technique. We propose an encoding of (the Single-Pushout approach of) graph grammar specifications into a relational and logical approach which allows the application of the mathematical induction technique to analyse systems with infinite state-spaces. We have defined graph grammars using relational structures and used logical languages to model rule applications. We first consider the case of simple (typed) graphs, and then we extend the approach to the non-trivial case of attributed-graphs and grammars with negative application conditions. Besides that, based on this relational encoding, we establish patterns for the presentation, codification and reuse of property specifications. The pattern has the goal of helping and simplifying the task of stating precise requirements to be verified. Finally, we propose to implement relational definitions of graph grammars in event-B structures, such that it is possible to use the event-B provers to demonstrate properties of a graph grammar.

abstract: Cyber-Physical Systems (CPS) are being used in many safety-critical applications. Due to the important role in virtually every aspect of human life, it is crucial to make sure that a CPS works properly before its deployment. However, formal verification of CPS is a computationally hard problem. Therefore, lightweight verification methods such as testing and monitoring of the CPS are considered in the industry. The formal representation of the CPS requirements is a challenging task. In addition, checking the system outputs with respect to requirements is a computationally complex problem. In this dissertation, these problems for the verification of CPS are addressed. The first method provides a formal requirement analysis framework which can find logical issues in the requirements and help engineers to correct the requirements. Also, a method is provided to detect tests which vacuously satisfy the requirement because of the requirement structure. This method is used to improve the test generation framework for CPS. Finally, two runtime verification algorithms are developed for off-line/on-line monitoring with respect to real-time requirements. These monitoring algorithms are computationally efficient, and they can be used in practical applications for monitoring CPS with low runtime overhead. / Dissertation/Thesis / Doctoral Dissertation Computer Science 2017

Dans la conception basée sur des modèles on construit un modèle mathématique du système que l'on utilise pour concevoir le système de sorte qu'il présente les propriétés souhaitées. Pour les systèmes de sûreté critique, il peut être d'une importance capitale de vérifier ces propriétés de sûreté sur le modèle, par exemple, pour tenir compte des variations des paramètres. Le calcul d'un nombre fini de comportements du système par le biais de simulation ne suffit pas à garantir des propriétés de sécurité. Avec une analyse d'atteignabilité on peut calculer une couverture de tous les comportements possibles du système, possiblement infinis. Cette analyse peut prendre en compte de non-déterminisme dans le modèle et peut garantir des propriétés de sécurité. Les systèmes d'intérêt présentent souvent à la fois un comportement continu et discret et de tels systèmes sont appelés systèmes hybrides. Le calcul d'atteignabilité est considéré comme difficile pour les systèmes continus et hybrides. Ce n'est que récemment que des méthodes pour le calcul d'accessibilité ont été développées qui peuvent être mis à l'échèlle. Ils sont basés sur des représentations implicites d'ensembles continus à l'aide du concepte mathématique de la fonction de support. Dans cette thèse, nous développons un outil extensible appelé SpaceEx pour le calcul d'atteignabilité des systèmes hybrides. Deux algorithmes d'atteignabilité ont été mis en œuvre dans SpaceEx, l'un basé sur l'outil PHAVer pour les automates linéaires hybrides et l'autre basé sur les fonctions de support pour les dynamiques affines par morceaux. L'algorithme de fonction support a été mis au point et sa mise à l'échelle a été amélioré en basculant entre différentes représentations d'ensembles continus. Nous proposons un algorithme de calcul d'image des transition discrètes amélioré qui réduit l'erreur de sur-approximation et nous illustrons sa précision et son efficacité avec plusieurs études de cas. / In model based design, one constructs a mathematical model of the system and uses it to design the system so that it exhibits the desired properties. For safety critical systems, it can be of utmost importance to verify these safety properties on the model, e.g., to account for parameter variations. Computing a finite number of system behaviors via simulation is not sufficient to guarantee safety properties. With a reachability analysis one can compute a cover of all possible system behaviors, potentially infinite, accounting for any non-determinism in the model, and with which one can guarantee safety properties. Systems of interest often exhibit both continuous and discrete behavior and such systems are called hybrid systems. Reachability computation is considered hard for continuous and hybrid systems. Only recently, scalable methods for reachability computation have been developed based on implicit set representations using the mathematical construct of support functions. In this thesis, we develop an extendable tool called SpaceEx for reachability of hybrid systems. Two reachability algorithms have been implemented in SpaceEx, one based on the PHAVer tool for linear hybrid automata and the other based on support functions for piecewise affine dynamics. The support function based algorithm has been tuned and its scalability has been improved by switching set representations. We propose an improved image computation algorithm for discrete transition that further reduces the over-approximation error and illustrate its accuracy and efficiency with several case studies.

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.