Made available in DSpace on 2015-04-11T14:03:20Z (GMT). No. of bitstreams: 1 HERBERT OLIVEIRA.pdf: 512075 bytes, checksum: acc5d05442df938abdfa025f9db23367 (MD5) Previous issue date: 2011-02-04 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The use of computer-based systems in several domains has increased significantly over the last years, one of the main challenges in software development of these systems is to ensure the correctness and reliability of these. So that software verification now plays an important role in ensuring the overall product quality, aimed mainly the characteristics of predictability and reliability. In the context of software verification, with respect to the use of model checking technique, Bounded Model Checkers have already been applied to discover subtle errors in actual systems projects, contributing effectively in this verification process. The value of the counterexample and safety properties generated by Bounded Model Checkers to create test case and to debug these systems is widely recognized. When a Bounded Model Checking (BMC) finds an error it produces a counterexample. Thus, the value of counterexamples to debug software systems is widely recognized in the state-of-the-practice. However, BMCs often produce counterexamples that are either large or difficult to be understood and manipulated mainly because of both the software size and the values chosen by the respective solver. In this work we aim to demonstrate and analyze the use of formal methods (through using the model checking technique) in the process of developing programs in C language, exploring the features already provided by the model checking as the counterexample and the identification and verification of safety properties. In view of this we present two approaches: (i) we describe a method to integrate the bounded model checker ESBMC with the CUnit framework. This method aims to extract the safety properties generated by ESBMC to generate automatically test cases using the rich set of assertions provided by the CUnit framework and (ii) a method aims to automate the collection and manipulation of counterexamples in order to instantiate the analised C program for proving the root cause of the identified error. Such methods may be seen as a complementary technique for the verification performed by BMCs. We show the effectiveness of our proposed method over publicly available benchmarks of C programs. / A utilização de sistemas baseados em computador em diversos domínios aumentou significativamente nos últimos anos. Um dos principais desafios no desenvolvimento de software de sistemas críticos é a garantia da sua correção e confiabilidade. Desta forma, a verificação de software exerce um papel importante para assegurar a qualidade geral do produto, visando principalmente características como previsibilidade e confiabilidade. No contexto de verificação de software, os Bounded Model Checkers estão sendo utilizados para descobrir erros sutis em projetos de sistemas de software atuais, contribuindo eficazmente neste processo de verificação. O valor dos contra-exemplos e propriedades de segurança gerados pelo Bounded Model Checkers para criar casos de testes e para a depuração de sistemas é amplamente reconhecido. Quando um Bounded Model Checking (BMC) encontra um erro ele produz um contra-exemplo. Assim, o valor dos contra-exemplos para depuração de software é amplamente reconhecido no estado da prática. Entretanto, os BMCs frequentemente produzem contra-exemplos que são grandes ou difíceis de entender ou manipular, principalmente devido ao tamanho do software e valores escolhidos pelo solucionador de satisfabilidade. Neste trabalho visamos demonstrar e analisar o uso de método formal (através da técnica model checking) no processo de desenvolvimento de programas na linguagem C, explorando as características já providas pelo model checking como o contra-exemplo e a identificação e verificação de propriedades de segurança. Em face disto apresentamos duas abordagens: (i) descrevemos um método para integrar o Bounded Model Checker ESBMC como o framework de teste unitário CUnit, este método visa extrair as propriedades geradas pelo ESBMC para gerar automaticamente casos de teste usando o rico conjunto de assertivas providas pelo framework CUnit e (ii) um método que visa automatizar a coleta e manipulação dos contra-exemplos, de modo a instanciar o programa C analisado, para comprovar a causa raiz do erro identificado. Tais métodos podem ser vistos como um método complementar para a verificação efetuada pelos BMCs. Demonstramos a eficácia dos métodos propostos sobre benchmarks públicos de código C.

Submitted by Wagner Junior (wagner.junior@unioeste.br) on 2018-11-30T17:04:04Z No. of bitstreams: 2 Claudia_Beatriz_Bozz_2018.pdf: 4791914 bytes, checksum: 0affba2e984ec7e6beefa83d0c3bdfeb (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2018-11-30T17:04:04Z (GMT). No. of bitstreams: 2 Claudia_Beatriz_Bozz_2018.pdf: 4791914 bytes, checksum: 0affba2e984ec7e6beefa83d0c3bdfeb (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2018-07-26 / Real time systems that have continuous behavior associated with discrete elements are called hybrid systems. Among them, in this master’s research, a hydraulic system has been chosen as an object of study in order to perform the reliability analysis of it through modeling and formal verification. Much as several models for the reliability analysis of complex systems have been proposed in the literature, most of them are not suitable to represent the system when its behavior needs to be expressed by means of continuous variables, like the case of hybrid systems. Generally, simulation and experimental testing are used to analyze systems, and they give only approximate results from a large amount of samples. To eliminate the limitations of these techniques, the formal verification is an effective alternative, since it is characterized by performing a sweep in all possible states of the system automatically, verifying the behavior as a whole. The UPPAAL STRATEGO toolkit for modelling by stochastic hybrid automata and model checking has been used in this work, both classic formal verification and statistical formal verification. A benckmark has been used as object of study. Initially, the system has been modelling and its behavior (physical and controlled) verified through simulation and formal verification (property specification and model checking). The reliability parameters obtained in the statistical analysis of the system failures have been compared with results of literature, presenting a dispersion less than 2.5%, so it can be verify that the methodology used and the models constructed were adequate to analyze the reliability of this system hybrid.In a second step of this work, the probability distribution of failure of the components have been modified, in order to become the system more reliable with real hydraulic systems, and estimate the optimum mean time between maintenance (MTBM) of this system. Thus, it’s possible to conclude that the methodology is adequate to perform the reliability analysis of the hydraulic system, being that model checking is effective to estimate the reliability parameters of the hydraulic system. / Sistemas de tempo real que possuem comportamento contínuo associado com elementos de características discretas são chamados de sistemas híbridos. Dentre estes, nesta pesquisa de mestrado, optou-se pelo emprego de um sistema hidráulico como objeto de estudo a fim de realizar a análise de confiabilidade do mesmo a partir de modelagem e verificação formal. Por mais que diversos modelos para a análise de confiabilidade de sistemas complexos tenham sido propostos na literatura, a maioria não são adequados para representar sistemas em que o comportamento é expresso em variáveis contínuas, como é o caso dos sistemas híbridos. De modo geral, para a análise de sistemas, a simulação e os testes experimentais são comumente utilizados, e geram apenas resultados aproximados a partir de uma grande quantidade de amostras. Para eliminar as limitações destas técnicas, a verificação formal é uma alternativa eficaz, visto que é caracterizada por realizar uma varredura em todos os estados possíveis do sistema de forma automática, verificando o comportamento como um todo do mesmo. Neste trabalho, foi utilizada a ferramenta computacional UPPAAL STRATEGO para a modelagem por autômatos estocásticos híbridos e verificação dos modelos, tanto verificação formal clássica como estatística. Um modelo padrão (benchmark) foi utilizado como objeto de estudo. Inicialmente o sistema foi modelado e seu comportamento (físico e controlado) verificado através da simulação e verificação formal (especificação de propriedades e verificação de modelos). Os parâmetros de confiabilidade obtidos na análise estatística de falha do sistema foram comparados com outros existentes na literatura, apresentado uma dispersão inferior a 2,5%, logo pôde se verificar que a metodologia empregada e os modelos construídos foram adequados para análise de confiabilidade deste sistema hibrido. Em uma segunda etapa do trabalho, foi modificada a distribuição de probabilidade de falha dos componentes, a fim de tornar o sistema mais fidedigno com sistemas hidráulicos reais, e estimar o tempo médio entre manutenções (MTBM – Mean Time Between Maintenance) ideal deste sistema. Portanto, conclui-se que a metodologia empregada foi adequada para realizar a análise de confiabilidade do sistema hidráulico, sendo efetivo levantar os parâmetros de confiabilidade através da verificação de modelos.

La gestion de l'évolution des processus métier exige une compréhension approfondie des cause des changements, de leurs niveaux d'application ainsi que de leurs impacts sur le reste du système. Dans cette thèse, nous proposons une approche de gestion et de contrôle de l'éolution des processus métier permettant d'analyser ces changements et de comprendre leurs impacts. Cela assistera les concepteurs et les chargés de l'évolution des processus métier à établir une évaluation a priori de l'impact pour réduire les risques et les coûts liés à ces changements et d'améliorer le service et la qualité des processus métier. Ce travail consiste à proposer un ensemble de contributions permettant une vérification de la cohérence et de la conformité des modèles de processus métier après chaque changement, mais aussi d'établir une éaluation a priori de l'impact structurel et qualificatif des modifications. Les différentes approches proposées sont en cours d'expérimentation et de validation à travers le développement d'une plate-forme basée sur l'environnement Eclipse / The evolution management of the business processes requires an exhaustive understanding of the change. An evolution engineer needs to understand reasons of a change, its application levels, and subsequently its impact on the whole system. In this thesis, we propose an approach for an a priori change impact analysis, to better control the business process evolution. This may help the business experts and the process designers to evaluate change impact in order to reduce the associated risks and estimate the related costs. It may also help to improve the service and quality of the business processes. This work contributes an eventual improvement, in regard, to verify the coherence and the compliance of the business process models, after each change. It leads to evaluate an a priori change impact analysis in structural and qualitatie aspects. The multiple-perspectives of the proposed approach have been reviewed experimentally. The validation of the approach is evaluated by exteding the Eclipse Development Environment, with the help of a set of plug-ins, as a prototype plate-form.

Ce travail appartient au domaine de la simulation numérique sur des plates-formes d'exécution distribuées hétérogènes telles que des grilles de calcul. Ce type de plate-forme se caractérise par des possibles changements de condition d'exécution et par une probabilité importante de défaillance de certains composants. Une application qui s'exécute dans un tel environnement se doit d'être adaptable à son contexte d'exécution et tolérante aux pannes. Face à la complexité croissante de la mise en place de cas de calcul sur des grilles de calcul, nous proposons une plateforme logicielle pour la résolution de cas de calcul numérique dans un environnement distribué hétérogène. Nos travaux apportent une solution qui se base sur un système d'agents mobiles, ce qui permet à une application de s'adapter au changement de son environnement d'exécution. Dans un premier temps, nous utilisons le langage pi calcul d'ordre supérieur pour spécifier une « ferme de travailleurs » capable de participer à la résolution de tout type de cas de calcul. Ensuite, nous énonçons des propriétés qui caractérisent le bon fonctionnement de ce système avec une logique temporelle TCTL. Pour cela, nous souhaitons modéliser notre système à l'aide d'automates temporisés à partir des termes définis par la spécification formelle en pi calcul. Dans ce but, nous définissons une transformation de termes écrits en pi calcul en automates temporisés. Les propriétés sont alors vérifiées avec l'outil UppAal. Pour valider ce travail de modélisation, nous avons réalisé le framework MCA (pour Mobile Computing Architecture). Celui-ci propose un ensemble d'outils facilitant la mise en place de composants sur un environnement distribué hétérogène dans le but d'effectuer la résolution de cas de calcul. La librairie avec laquelle sont développés ces composants, qu'ils soient mobiles ou non, est implantée en Java et se base les technologies Jini et JavaSpaces. Enfin, nous réalisons l'évaluation du framework MCA en procédant à la résolution de trois cas de calcul différents. Chacune de ces expériences, réalisées sur une grappe de 20 noeuds, nous permet de montrer les caractéristiques essentielles de notre framework : une simplicité de programmation, un faible surcoût en temps d'exécution sans l'activation de la tolérance aux pannes et une tolérance aux pannes efficace / This work belongs to the domain of numerical simulation on heterogeneous distributed platforms such as grids. This type of platform is characterized by possible changes in execution conditions and a significant probability of some components failure. An application running in such an environment must be adaptable to its execution context and fault tolerant. Facing the growing complexity of implementing computation cases on grid computing, we propose a software platform which solves numerical computation cases in a distributed heterogeneous environment. Our work provides a solution based on a mobile agent system, which allows an application to adapt to change in its execution environment. At first, we use the higher-order pi calculus language to specify a « farm of workers » able to take part in solving any type of computation case. Then we set the properties that characterize the system's correct execution with a temporal logic TCTL. In order to do this, we perform a temporal modeling system based on terms defined by the formal specification in pi calculus. To achieve this transformation, we define a translation of terms written in pi calculus into timed automata. The properties are verified with the UppAal tool. To validate this modeling work, we develop the MCA (for Mobile Computing Architecture) framework. It offers a set of tools which facilitate the implementation of distributed heterogeneous components in order to solve computation cases. These components, mobile or not, are developed with a library written in Java and which uses Jini and JavaSpaces technologies. Finally, our framework is evaluated through the resolution of three different computation cases. Each of these experiments, performed on a 20 node cluster allow us to highlight our framework's main characteristics : programming simplicity, low overhead in execution time without the fault tolerance activation and efficient fault tolerance

Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.

Nous proposons de nouveaux algorithmes et de nouvelles structures de données pour la vérification formelle de systèmes réactifs finis sur architectures parallèles. Ces travaux se basent sur les techniques de vérification model checking. Notre approche cible des architectures multi-processeurs et multi-cœurs, avec mémoire partagée, qui correspondent aux générations de serveurs les plus performants disponibles actuellement.Dans ce contexte, notre objectif principal est de proposer des approches qui soient à la fois efficaces au niveau des performances, mais aussi compatibles avec les politiques de partage dynamique du travail utilisées par les algorithmes de génération d’espaces d'états en parallèle; ainsi, nous ne plaçons pas de contraintes sur la manière dont le travail ou les données sont partagés entre les processeurs.Parallèlement à la définition de nouveaux algorithmes de model checking pour machines multi-cœurs, nous nous intéressons également aux algorithmes de vérification probabiliste. Par probabiliste, nous entendons des algorithmes de model checking qui ont une forte probabilité de visiter tous les états durant la vérification d’un système. La vérification probabiliste permet des gains importants au niveau de la mémoire utilisée, en échange d’une faible probabilité de ne pas être exhaustif; il s’agit donc d’une stratégie permettant de répondre au problème de l’explosion combinatoire / In this thesis, we propose and study new algorithms and data structures for model checking finite-state, concurrent systems. We focus on techniques that target shared memory, multi-cores architectures, that are a current trend in computer architectures.In this context, we present new algorithms and data structures for exhaustive parallel model checking that are as efficient as possible, but also ``friendly'' with respect to the work-sharing policies that are used for the state space generation (e.g. a work-stealing strategy): at no point do we impose a restriction on the way work is shared among the processors. This includes both the construction of the state space as the detection of cycles in parallel, which is is one of the key points of performance for the evaluation of more complex formulas.Alongside the definition of enumerative, model checking algorithms for many-cores architectures, we also study probabilistic verification algorithms. By the term probabilistic, we mean that, during the exploration of a system, any given reachable state has a high probability of being checked by the algorithm. Probabilistic verification trades savings at the level of memory usage for the probability of missing some states. Consequently, it becomes possible to analyze part of the state space of a system when there is not enough memory available to represent the entire state space in an exact manner

Dans cette thèse, nous nous intéressons à la problématique de la vérification formelle des systèmes critiques temps réel, c’est-à-dire des systèmes dont l’exécution dépend de certaines contraintes temporelles. La spécification formelle des exigences pour de tels systèmes, ainsi que leur vérification, reste une tâche très compliquée, surtout pour les non experts. Plusieurs solutions ont été proposées pour faciliter la spécification et la vérification des systèmes temps-réels. Un premier type d’approche est basée sur la définition d’un ensemble de patrons de spécification qui représentent les propriétés les plus utilisées en pratique. Cependant, ce type de solutions n’est pas toujours supporté par un outillage de vérification efficace, dans le sens que les auteurs de ces langages de patrons ne fournissent pas directement une implantation pour leur langage. Un second type d’approches repose sur l’utilisation du formalisme des logiques temporelles pour spécifier les propriétés à vérifier et sur les techniques de model-checking pour leur vérification. S’agissant de systèmes temps-réels, il est dans ce cas nécessaire d’utiliser des extensions temporisées des logiques temporelles. Cependant, ces approches donnent le plus souvent lieu à des problèmes de model-checking qui sont indécidable, ou dont la complexité en pratique est très élevée. Dans ce travail, nous suivons la première approche et proposons un langage de patrons de propriétés temps-réels accompagnés d’un outil de vérification par model- checking. Nous apportons plusieurs contributions à ce domaine. Nous proposons un cadre théorique complet pour la spécification et la vérification de patrons de propriétés temps réel. Notre approche a été implantée dans le contexte du langage de modélisation Fiacre. Enfin, nous définissons deux méthodes complémentaires permettant de vérifier la correction de notre approche de vérification / The formal verification of critical, reactive systems is a very complicated task, especially for non experts. In this work, we more particularly address the problem of real time systems, that is in the situation where the correctness of the system depends upon timing constraints, such as the “timeliness” of some interactions. Many solutions have been proposed to ease the specification and the verification of such systems. An interesting approach—that we follow in this thesis—is based on the definition of specification patterns, that is sets of general, reusable templates for commonly occurring classes of properties. However, patterns are rarely implemented, in the sense that the designers of specification languages rarely provide an effective verification method for checking a pattern on a system. The most common technique is to rely on a timed extension of a temporal logic to define the semantics of patterns and then to use a model-checker for this logic. However, this approach may be inadequate, in particular if patterns require the use of a logic associated to an undecidable model-checking problem or to an algorithm with a very high practical complexity. We make several contributions. We propose a complete theoretical framework to specify and check real time properties on the formal model of a system. First, our framework provides a set of real time specification patterns. We provide a verification technique based on the use of observers that has been implemented in a tool for the Fiacre modelling language. Finally, we provide two methods to check the correctness of our verification approach; a “semantics”—theoretical— method as well as a “graphical”-practical- method

This thesis deals with the application of bounded model checking method for self-healing assurance of concurrency related problems. The self-healing is currently interested in the Java programming language. Therefore, it concetrate mainly on the model checker Java PathFinder which is built for handling Java programs. The verification method is implemented like the Record&Replay trace strategy for navigation through a state space and performance bounded model checking from reached state through the use of Record&Replay trace strategy. Java PathFinder was extended by new moduls and interfaces in order to perform the bounded model checking for self-healing assurance. Bounded model checking is applied at the neighbourhood of self-healing.

Bit flips are known to be a source of strange system behavior, failures, and crashes. They can cause dramatic financial loss, security breaches, or even harm human life. Caused by energized particles arising from, e.g., cosmic rays or heat, they are hardly avoidable. Due to transistor sizes becoming smaller and smaller, modern hardware becomes more and more prone to bit flips. This yields a high scientific interest, and many techniques to make systems more resilient against bit flips are developed. Fault-tolerance techniques are techniques that detect and react to bit flips or their effects. Before using these techniques, they typically need to be configured for the particular system they shall protect, the grade of resilience that shall be achieved, and the environment. State-of-the-art configuration approaches have a high risk of being imprecise, of being affected by undesired side effects, and of yielding questionable resilience measures. In this thesis we encourage the usage of formal methods for resiliency configuration, point out advantages and investigate difficulties. We exemplarily investigate two systems that are equipped with fault-tolerance techniques, and we apply parametric variants of probabilistic model checking to obtain optimal configurations for pre-defined resilience criteria. Probabilistic model checking is an automated formal method that operates on Markov models, i.e., state-based models with probabilistic transitions, where costs or rewards can be assigned to states and transitions. Probabilistic model checking can be used to compute, e.g., the probability of having a failure, the conditional probability of detecting an error in case of bit-flip occurrence, or the overhead that arises due to error detection and correction. Parametric variants of probabilistic model checking allow parameters in the transition probabilities and in the costs and rewards. Instead of computing values for probabilities and overhead, parametric variants compute rational functions. These functions can then be analyzed for optimality. The considered fault-tolerant systems are inspired by the work of project partners. The first system is an inter-process communication protocol as it is used in the Fiasco.OC microkernel. The communication structures provided by the kernel are protected against bit flips by a fault-tolerance technique. The second system is inspired by the redo-based fault-tolerance technique \haft. This technique protects an application against bit flips by partitioning the application's instruction flow into transaction, adding redundance, and redoing single transactions in case of error detection. Driven by these examples, we study challenges when using probabilistic model checking for fault-tolerance configuration and present solutions. We show that small transition probabilities, as they arise in error models, can be a cause of previously known accuracy issues, when using numeric solver in probabilistic model checking. We argue that the use of non-iterative methods is an acceptable alternative. We debate on the usability of the rational functions for finding optimal configurations, and show that for relatively short rational functions the usage of mathematical methods is appropriate. The redo-based fault-tolerance model suffers from the well-known state-explosion problem. We present a new technique, counter-based factorization, that tackles this problem for system models that do not scale because of a counter, as it is the case for this fault-tolerance model. This technique utilizes the chain-like structure that arises from the counter, splits the model into several parts, and computes local characteristics (in terms of rational functions) for these parts. These local characteristics can then be combined to retrieve global resiliency and overhead measures. The rational functions retrieved for the redo-based fault-tolerance model are huge - for small model instances they already have the size of more than one gigabyte. We therefor can not apply precise mathematic methods to these functions. Instead, we use the short, matrix-based representation, that arises from factorization, to point-wise evaluate the functions. Using this approach, we systematically explore the design space of the redo-based fault-tolerance model and retrieve sweet-spot configurations.

Probabilistic model checking is a powerful technique used to ensure the correct functioning of systems which exhibit real-time and stochastic behaviours. Many such systems are embedded and used in safety-critical situations, to mention implantable medical devices. This thesis aims to develop a formal model-based framework that is tailored for the analysis and verification of cardiac pacemakers. The contributions are novel approaches for the automatic verification and validation of real-time properties over continuous-time models, which are applicable to software embedded in medical devices. First, we address the problem of model checking continuous-time Markov chain (CTMC) models against real-time specifications given in the form of temporal logic, namely, metric temporal logic (MTL) and linear duration properties (LDP), or as timed automata (TA). The main question that we address is “given a continuous-time Markov chain, what is the probability of the set of timed paths that satisfy the real-time property under consideration?”. We provide novel algorithms to approximate the probability through generating systems of linear inequalities over variables that represent the waiting times in system states, and then solving multidimensional integrals over this set. Second, we present a model-based framework to support the design and verification of pacemakers against real-time properties. The pacemaker is modelled as a network of timed automata, whereas the human heart is modelled either as a network of timed automata or as a network of hybrid automata. Our framework can be instantiated with personalised heart models whose parameters can be learnt from patient data, and we have done so to validate our approach. We introduce property patterns and the counting metric temporal logic (CMTL) in order to specify the properties of interest. We provide new verification algorithms for networks of timed or hybrid automata against property patterns and CMTL. Finally, we pose and solve the parameter synthesis problem, i.e., given a network of timed automata containing model parameters, an objective function and a CMTL formula, find the set of parameter valuations, whenever existing, which satisfy the CMTL formula and maximise the objective function. The framework has been implemented using Simulink, Matlab and Python code. Extensive experimental results on pacemaker models have been carried out and discussed in detail. The techniques developed in this thesis can assist in the design and verification of software embedded in medical devices.