O presente trabalho trata da verificação e design de sistemas complexos, especificamente da verificação de sistemas de tempo real concorrentes e distribuídos. Propõe-se uma técnica enumerativa para a verificação formal de modelos que permite determinar a validade de propriedades quantitativas, além das qualitativas. A técnica proposta separa a construção do espaço de estados dos algoritmos de rotulação das fórmulas temporais, o que possibilita a diminuição da complexidade do processo de verificação, tornando-o viável para aplicações práticas. A técnica proposta foi inicialmente aplicada sobre modelos de redes de Petri temporizadas e depois em uma rede unificada chamada GHENeSys para aproveitar as características de abstração, hierarquia e de elementos de interação chamados pseudo-boxes. A definição da rede GHENeSys foi modificada para permitir a modelagem de sistemas onde os requisitos temporais devem ser expressos através de atrasos e prazos como e o caso dos sistemas de tempo real. A rede suporta ainda mecanismos de refinamento tanto para os elementos ativos quanto os passivos. A demonstração da manutenção de propriedades como invariantes, vivacidade, limitação assim como da validade de fórmulas lógicas no processo de refinamento constitui um aspecto fundamental no projeto de sistemas complexos, e foi portanto revista em detalhes para a rede GHENeSys. Alguns exemplos práticos são apresentados para avaliar o desempenho dos algoritmos e um estudo de caso finaliza a apresentação, onde se pode contrastar os algoritmos propostos com os implementados na ferramenta UPPAAL. / This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.

Submitted by Geyciane Santos (geyciane_thamires@hotmail.com) on 2015-07-23T14:25:32Z No. of bitstreams: 1 Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:35:05Z (GMT) No. of bitstreams: 1 Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2015-07-23T15:38:02Z (GMT) No. of bitstreams: 1 Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) / Made available in DSpace on 2015-07-23T15:38:02Z (GMT). No. of bitstreams: 1 Dissertação - Renato Barbosa Abreu.pdf: 745859 bytes, checksum: aedacf2a1901d7a7fb83eb1ddb429e77 (MD5) Previous issue date: 2014-06-17 / Não Informada / Currently, digital filters are employed in a wide variety of signal processing applications, using floating- and fixed-point processors. Regarding the latter, some filter implementations may be prone to errors, due to problems related to finite word-length. In particular, signal processing modules present in such realizations can produce overflows and unwanted noise caused by the quantization and round-off effects, during accumulativeaddition and multiplication operations. The present work addresses this problem and proposes a new methodology to verify digital filters, based on a state-of-the-art bounded model checker called ESBMC, which supports full C/C++ and employs satisfiabilitymodulo- theories solvers. In addition to verifying overflow and limit-cycle occurrences, the present approach can also check design properties, like stability and frequency response, as well as output errors and time constraints, based on discrete-time models implemented in C. The experiments conducted during this work show that the proposed methodology is effective, when finding realistic design errors related to fixed-point implementations of digital filters. It is worth noting that the proposed method, in addition to helping the designer to determine the number of bits for fixedpoint representations, can also aid to define details of filter realization and structure. / Atualmente, os filtros digitais são empregados em uma ampla variedade de aplicações para processamento de sinais, utilizando tanto processadores de ponto flutuante quanto de ponto fixo. No que diz respeito a este último, algumas implementações de filtro podem estar mais propensas a erros, devido a problemas relacionados com a palavra de dados de comprimento finito. Em particular, o processamento de sinais utilizando tais realizações pode produzir o problema de estouro aritmético e ruídos indesejados causados pela quantização e efeitos de arredondamento, durante operações acumulativas de adição e multiplicação. O presente trabalho aborda este problema e propõe uma nova metodologia para a verificação de filtros digitais, com base em um verificador de modelos no estado da arte, chamado ESBMC, que suporta linguagens C/C++ e emprega solucionadores baseados em teoria do módulo da satisfatibilidade. Além de verificar a ocorrência de estouro aritmético e ciclo limite, a presente abordagem também pode verificar propriedades de projeto, como estabilidade e resposta em frequência, bem como restrições temporais e erro de saída, com base em modelos de tempo discreto implementados em C. Os experimentos realizados durante este trabalho mostram que a metodologia proposta é eficaz, pois encontra erros de projeto realistas, que estão relacionados a implementações de filtros digitais em ponto fixo. Vale ressaltar que os resultados apresentados evidenciam que o método proposto, além de auxiliar o projetista a determinar o número de bits da representação de ponto fixo, também pode ajudar a definir detalhes de realização e estrutura de filtro.

Modern software systems are increasingly characterized by uncertainties in the operating context and user requirements. These uncertainties are difficult to predict at design time. Achieving the quality goals of such systems depends on the ability of the software to deal with these uncertainties at runtime. A self-adaptive system employs a feedback loop to continuously monitor and adapt itself to achieve particular quality goals (i.e., adaptation goals) regardless of uncertainties. Current research applies formal techniques to provide guarantees for adaptation goals, typically using exhaustive verification techniques. Although these techniques offer strong guarantees for the goals, they suffer from well-known state explosion problem. In this thesis, we take a broader perspective and focus on two types of guarantees: (1) functional correctness of the feedback loop, and (2) guaranteeing the adaptation goals in an efficient manner. To that end, we present ActivFORMS (Active FORmal Models for Self-adaptation), a formally founded model-driven approach for engineering self-adaptive systems with guarantees. ActivFORMS achieves functional correctness by direct execution of formally verified models of the feedback loop using a reusable virtual machine. To efficiently provide guarantees for the adaptation goals with a required level of confidence, ActivFORMS applies statistical model checking at runtime. ActivFORMS supports on the fly changes of adaptation goals and updates of the verified feedback loop models that meet the changed goals. To demonstrate the applicability and effectiveness of the approach, we applied ActivFORMS in several domains: warehouse transportation, oceanic surveillance, tele assistance, and IoT building security monitoring. / Marie Curie CIG, FP7-PEOPLE-2011-CIG, Project ID: 303791

Cette thèse traite de la vérification formelle de systèmes critiques où la correction du système dépend du respect des contraintes temporelles. La première partie étudie la modélisation et la vérification formelle par model-checking de systèmes temps réel dans le contexte de l’industrie aéronautique et spatiale. La deuxième partie décrit notre méthode d’exploitation des symétries pour les réseaux de Petri temporels. Nous définissons un opérateur de composition symétrique pour la construction de réseaux. Puis nous proposons des solutions pour la construction d’espaces d’états quotients par la relation d’équivalence induite par les symétries. Notre méthode s’applique aux réseaux de Petri, temporels ou non. A notre connaissance il s’agit de la première méthode applicable aux réseaux de Petri temporels. Des résultats expérimentaux encourageants sont présentés. / This thesis deals with formal verification of critical systems where the system’s correction depends on compliance with time constraints. The first part studies the formal modeling and verification by model-checking of realtime systems in the context of the aerospace industry. The second part describes our method for symmetry reduction of Time Petri Net. We define a symmetric composition operator for building Net. Then we present our solution for construction of quotients of the state spaces by the equivalence relation induced by symmetries. Our method applies to Petri nets, temporal or not, but to our knowledge this is the first methodology for Time Petri Nets. Encouraging experimental results are presented.

Cette thèse s'intéresse à l'étude des méthodes formelles de spécification et de vérification dans le cadre des systèmes d'information. Les systèmes d'informations sont des systèmes dynamiques constitués d'entités et d'associations représentées par la composition en parallèle de processus répliqués issus de différentes classes. De plus, ces systèmes font partie de la classe des systèmes paramétrés. On propose un modèle de spécification de systèmes paramétrés, nommé PASTD, qui est adapté aux systèmes d'information et qui est basé sur la notation des diagrammes états-transitions algébriques (ASTD). Puis, on étudie le problème de sûreté pour les PASTD, à travers la méthode de vérification de couverture pour les systèmes de transitions bien structurés (WSTS). Cette méthode repose sur trois conditions principales : la monotonie, le beau préordre et la pred-base effective. Les PASTD sont montrés comme étant monotones et on définit une sous-classe vérifiant la propriété de beau préordre. Enfin, on décrit une nouvelle méthode, adaptée aux systèmes paramétrés, qui explicite un ensemble de conditions permettant de prouver la pred-base effective. Ces conditions définissent une nouvelle classe appelée RMTS (\emph{Ranked Monotone Transition Systems}). Cette méthode est appliquée aux PASTD.

This thesis discusses autonomous vehicles. At first it contains describing development of these type of vehicles, how they work and discuss their future development. Further it describe tools which can be used for create model of autonomous vehicle. The thesis includes design, description of the development and testing of the model in the UPPAAL Stratego verification environment. The resulting model is a system of intercommunicating timed automata. The analysis of the model properties is based on the method of statistical verification. The model allows us to investigate behavior of an autonomous vehicle in situations which correspond to regular traffic.

Safety in human in the loop systems, systems that change behavior with human input, is difficult to achieve. This difficulty can cost lives. As desired system capability grows, so too does the requisite complexity of the system. This complexity can result in designers not accounting for every use case of the system and unintentionally designing in unsafe behavior. Furthermore, complexity of operation and control can result in operators becoming confused during use or receiving insufficient training in the first place. All these cases can result in unsafe operations. One method of improving safety is implementing the use of formal models during the design process. These formal models can be analyzed mathematically to detect dangerous conditions, but can be difficult to produce without time, money, and expertise.<br> This document details the study of potential methods for constructing formal models autonomously from recorded observations of system use, minimizing the need for system expertise, saving time, money, and personnel in this safety critical process. I first discuss how different system characteristics affect system modeling, isolating specific traits that most clearly affect the modeling process Then, I develop a technique for modeling a simple, digital, menu-based system based on a record of user inputs. This technique attempts to measure the availability of different inputs for the user, and then distinguishes states by comparing input availabilities. From there, I compare paths between states and check for shared behaviors. I then expand the general procedure to capture the behavior of a flight simulator. This system more closely resembles real-world safety critical systems and can therefore be used to approximate a real use case of the method outlined. I use machine learning tools for statistical analysis, comparing patterns in system behavior and user behaviors. Last, I discuss general conclusions on how the modeling approaches outlined in this document can be improved and expanded upon.<br> For simple systems, we find that inputs alone can produce state machines, but without corresponding system information, they are less helpful for determining relative safety of different use cases than is needed. Through machine learning, we find that records of complex system use can be decomposed into sets of nominal and anomalous states but determining the causal link between user inputs and transitions between these conditions is not simple and requires further research.

Tato práce analyzuje hrozby pro protokoly využívající bezkontaktní čipové karty a představuje metodu pro poloautomatické hledání zranitelností v takových protokolech pomocí model checkingu. Návrh a implementace bezpečných aplikací jsou obtížné úkoly, i když je použit bezpečný hardware. Specifikace na vysoké úrovni abstrakce může vést k různým implementacím. Je důležité používat čipovou kartu správně, nevhodná implementace protokolu může přinést zranitelnosti, i když je protokol sám o sobě bezpečný. Cílem této práce je poskytnout metodu, která může být využita vývojáři protokolů k vytvoření modelu libovolné čipové karty, se zaměřením na bezkontaktní čipové karty, k vytvoření modelu protokolu a k použití model checkingu pro nalezení útoků v tomto modelu. Útok může být následně proveden a pokud není úspěšný, model je upraven pro další běh model checkingu. Pro formální verifikaci byla použita platforma AVANTSSAR, modely jsou psány v jazyce ASLan++. Jsou poskytnuty příklady pro demonstraci použitelnosti navrhované metody. Tato metoda byla použita k nalezení slabiny bezkontaktní čipové karty Mifare DESFire. Tato práce se dále zabývá hrozbami, které není možné pokrýt navrhovanou metodou, jako jsou útoky relay.

The correctness of a workflow specification is critical for the automation of business processes. For this reason, errors in the specification should be detected and corrected as early as possible - at specification time. In this paper, we present a validation method for workflow specifications using model-checking techniques. A formalized workflow specification, its properties and the correctness requirements are translated into a timed state machine that can be analyzed with the Uppaal model checker. The main contribution of this paper is the use of timed model checking for verifying time-related properties of workflow specifications. Using only one tool (the model checker) for verifying these different kinds of properties gives an advantage over using different specialized algorithms for verifying different kinds of properties.

Data race in parallel programs can be difficult to precisely detect, and doing so manually can often prove unsuccessful. Task parallel programming models can help reduce defects introduced by the programmer by restricting concurrent functionalities to fork-join operations. Typical data race detection algorithms compute the happens-before relation either by tracking the order that shared accesses happen via a vector clock counter, or by grouping events into sets that help classify which heap locations are accessed sequentially or in parallel. Access sets are simple and efficient to compute, and have been shown to have the potential to outperform vector clock approaches in certain use cases. However, they do not support arbitrary thread synchronization, are limited to fork-join or similar structures, and do not support mutual exclusion. Vector clock approaches do not scale as well to many threads with many shared interactions, rendering them inefficient in many cases. This work combines the simplicity of access sets with the generality of vector clocks by grouping heap accesses into access sets, and attaching the vector clock counter to those groupings. By combining these two approaches, access sets can be utilized more generally to support programs that contain mutual exclusion. Additionally, entire blocks can be ordered with each other rather than single accesses, producing a much more efficient algorithm for data race detection. This novel algorithm, ZipperOTF, is compared to the Computation Graph algorithm (an access set algorithm) as well as FastTrack (a vector clock algorithm) to show comparisons in empirical results and in both time and space complexity.