No description available.

No description available.

Title: Analysis of a File System Using the Verifying C Compiler Author: Bc. David Škorvaga Department: Department of Distributed and Dependable Systems Supervisor: RNDr. Jan Kofroň, Ph.D. Abstract: Formal verification is a way to improve reliability of software systems. One approach of formal verification is focused on proving correctness of annotat- ed source code of an established programming language. Verifying C Compiler (VCC) is a verifier for concurrent C that accepts an annotated code in C language and automatically verifies its correctness with respect to the given annotation. There have been successful attempts to verify some critical systems, including the operating system kernel. Another critical part of operating system is its file system. In the thesis, we choose FatFs file system, a simple device-independent implementation of the FAT file system. We specify a part of it using the VCC annotation and successfully verify its correctness. Keywords: Formal Verification, File System, VCC

Due to the increasing complexity of today\'s cyber-physical systems, defects become inevitable and harder to detect. The complexity of such software is generally huge, with millions of lines of code. The impact of failure of such systems could be hazardous. The reliability of the system depends on the effectiveness and rigor of the testing procedures. Verification of the software behind such cyber-physical systems is required to ensure stability and reliability before the systems are deployed in field. We have investigated the verification of the software for Autonomous Underwater Vehicles (AUVs) to ensure safety of the system at any given time in the field. To accomplish this, we identified useful invariants that would aid as monitors in detecting abnormal behavior of the software. Potential invariants were extracted which had to be validated. The investigation attempts to uncover the possibility of performing this method on existing Software verification platforms. This was accomplished on Cloud9, which is built on KLEE and using the Microsoft\'s VCC tool. Experimental results show that this method of extracting invariants can help in identifying new invariants using these two tools and the invariants identified can be used to monitor the behavior of the autonomous vehicles to detect abnormality and failures in the system much earlier thereby improving the reliability of the system. Recommendations for improving software quality were provided. The work also explored safety measures and standards on software for safety critical systems and Autonomous vehicles. Metrics for measuring software complexity and quality along with the requirements to certify AUV software were also presented. The study helps in understanding verification issues, guidelines and certification requirements. / Master of Science

The present research evaluates the social inclusion component of the Brazilian National Program for the Production and Use of Biodiesel’s (PNPB) by studying its impact on the livelihoods of family farmers in the country’s Northeast region of Bahia. The overall objective is to critically analyze the social sustainability aspect of the program by including different dimensions of social exclusion in its analysis. More specifically, this thesis examines the PNPB’s effectiveness in helping family farmers in Bahia achieve positive livelihood outcomes. In terms of theoretical perspective, the Sustainable Livelihoods Framework (SLF) is employed while existing research and government data are analyzed using a descriptive method. The findings of this thesis indicate that the PNPB is predominantly designed in economic terms, largely ignoring the multi-dimensional nature of social exclusion. In this sense, the results suggest that the lack of success of the program in the country’s Northeast region can be in part explained by its failure to adopt coherent and sustainable strategies that go beyond market insertion and income generation. In particular, the research demonstrated that the PNPB’s lack of participatory approach and the absence of social and cultural considerations, along with inadequate technical extension services, hampered the program’s success in the region. Based on these results, this research highlights the need for a broader approach when it comes to promoting social inclusion, as well as the importance of taking into account and developing the cultural, social and political capital of family farmers in Bahia. In this sense, this thesis emphasizes the importance of recognizing that social exclusion is a complex and multi-faceted phenomenon, which calls for improving the ways with which we evaluate and deepen the understanding of the livelihoods of family farmers in Bahia.

The aim of the study was to evaluate the effect of human immunodeficiency virus infection (HIV) and antiretroviral treatment on the retinal nerve fibre layer (RNFL). The RNFL hickness defined by standard parameters(TSNIT average, Superior average and Inferior average) was assessed in 48 HIV positive patients using scanning laser polarimeter, GDx VCC device. Results were compared to normal values and tested against factors suspected to affect the RNFL thickness. The mean values of the RNFL standard parameters were for TSNIT average, Superior average and Inferior average, 57,65 ± 6,18  m, 69,38 ± 8,34  m, 68,89 ± 9,50  m respectively, in our cohort. The RNFL thinning was not confirmed in our HIV positive group compared to values on healthy population. No significant correlation between the RNFL thickness and the immune profile or antiretroviral therapy was detected. However, a significant negative correlation between the RNFL thickness with increasing duration of HIV infection was foundin our study that is hypothesized to be possibly on an immune pathological basis. Powered by TCPDF (www.tcpdf.org)

No description available.

PURPOSE. Confocal laser scanning ophthalmoscopy (HRT; Heidelberg retinal tomograph II) and scanning laser polarimetry (GDx-variable corneal compensator [VCC]) were used to investigate whether early indicators of retinal nerve fiber layer (RNFL) thickness loss could be observed in patients infected with the human immunodeficiency virus (HIV) that had no associated retinopathy or optic neuropathy and were concomitantly receiving antiretroviral medications. METHODS. HRT and GDx-VCC parameters obtained from a group of 13 HIV-positive subjects (n = 26 eyes) on antiretroviral therapy examined with HRT, with a subgroup of six subjects (n = 12 eyes) examined with both HRT and GDx-VCC, were compared with those of a matched HIV-negative control cohort (13 subjects, n = 26 eyes) examined with HRT, with a subgroup of five subjects (n = 10 eyes) examined with both HRT and GDx-VCC. We employed generalized estimating equations for statistical analysis. RESULTS. Reduced mean values for the HRT height variation contour (p < 0.045) and HRT mean RNFL thickness (p < 0.023) were observed in HIV-positive subjects controlling for age, sex, and race. A significantly reduced mean value corresponding to the GDx-VCC superior maximum (p < 0.014) and inferior maximum (p < 0.016) were also observed for the HIV-positive cohort analyzed controlling for age, sex, and race. CONCLUSION. HRT and GDx-VCC indicators of RNFL thickness appear to be significantly reduced in HIV-positive subjects without retinopathy or optic nerve disease using antiretroviral medication, suggesting RNFL loss occurs in this population of HIV-positive patients. The lack of correlation between CD4 counts, viral load, number of antiretroviral medications used, or years from diagnosis of HIV and RNFL thinning, suggests that possibly other factors associated with HIV infection may contribute to the apparent RNFL thickness loss.

Este trabalho visa estudar e implementar a integração entre o domínio de comutação de circuitos e o IP Multimedia Subsystem (IMS) para suportar handovers verticais, ou seja, entre redes de acesso distintas, por exemplo, Global System for Mobile communications (GSM) e WiFi, em especial no Serviço Voice Call Continuity (VCC). Entretanto muito pouco é especificado sobre a integração entre os domínios nas normas das diversas entidades de padronização que tratam sobre o assunto. Assim, apresenta-se uma proposta para essa integração, criando-se uma nova entidade funcional para realizá-la, o Call Data Storage Function (CDSF), que interage com os demais módulos do Serviço VCC e garante que algumas informações que devem ser trocadas entre os módulos não sejam perdidas, devido à conversão de protocolos de sinalização na interface entre tais domínios. O CDSF auxilia também no controle da alocação de endereços de referência utilizados no encaminhamento de chamadas de um domínio para o outro. São definidos os protocolos de acesso ao CDSF, bem como os métodos disponíveis. Em sua concepção, recorre-se a uma modelagem modular, que permite futuras melhorias, apenas por troca de módulos. Como estudos de caso para validar a proposta são apresentados cenários de chamadas que utilizam o Serviço VCC, passando pelo CDSF. Por fim, conclui-se que a integração entre os domínios é viável se a proposta deste trabalho for utilizada. Também se demonstra que a separação dos planos de controle dos planos de dados (de usuário) é uma das contribuições fundamentais da arquitetura NGN para o sucesso de suas implementações, como por exemplo o IMS.Além disso, destacam-se as vantagens que o Serviço VCC pode agregar ao IMS, contribuindo para sua adesão em menor prazo pelas operadoras de telecomunicações, dado que esse serviço contribui para a integração de redes, cada vez mais convergentes, agregando mobilidade e continuidade à sua utilização. / This work intends to study and implement the integration between the circuit switching domain and the IP Multimedia Subsystem (IMS) to support vertical handovers that are between different access networks, such as Global System for Mobile communications (GSM) and WiFi. Therefore the specifications are incomplete about this topic in standards from the entities who works with this subject. Then, is presented a new proposal for this integration: a new functional entity to realize this integration: the Call Data Storage Function (CDSF), which interacts with other modules of VCC Service and guarantees that some information shared between modules are not lost, due to conversion of signalling protocols in the interface between domains. Besides that, CDSF helps in the control of allocation of reference address that are used to route calls from one domain to another. Access protocols to CDSF are defined and CDSF methods are exposed. The CDSF design uses a modular approach, which allows future improvements, just changing modules. As case studies to validate this work proposal, call scenarios are presented that uses the VCC Service, using CDSF. Finally, it is concluded that the integration between domains is viable if this work proposal is used. It is presented, as well, that the separation between control plans and data plans is one of the main contributions of NGN architecture to the success of its implementations, like IMS. Furthermore, it is exposed the advantages that VCC Service can aggregate to IMS, contributing for more rapidly adoption by telecommunications operators, considering that this service helps the networks integration, adding convergence, mobility and continuity.

Este trabalho visa estudar e implementar a integração entre o domínio de comutação de circuitos e o IP Multimedia Subsystem (IMS) para suportar handovers verticais, ou seja, entre redes de acesso distintas, por exemplo, Global System for Mobile communications (GSM) e WiFi, em especial no Serviço Voice Call Continuity (VCC). Entretanto muito pouco é especificado sobre a integração entre os domínios nas normas das diversas entidades de padronização que tratam sobre o assunto. Assim, apresenta-se uma proposta para essa integração, criando-se uma nova entidade funcional para realizá-la, o Call Data Storage Function (CDSF), que interage com os demais módulos do Serviço VCC e garante que algumas informações que devem ser trocadas entre os módulos não sejam perdidas, devido à conversão de protocolos de sinalização na interface entre tais domínios. O CDSF auxilia também no controle da alocação de endereços de referência utilizados no encaminhamento de chamadas de um domínio para o outro. São definidos os protocolos de acesso ao CDSF, bem como os métodos disponíveis. Em sua concepção, recorre-se a uma modelagem modular, que permite futuras melhorias, apenas por troca de módulos. Como estudos de caso para validar a proposta são apresentados cenários de chamadas que utilizam o Serviço VCC, passando pelo CDSF. Por fim, conclui-se que a integração entre os domínios é viável se a proposta deste trabalho for utilizada. Também se demonstra que a separação dos planos de controle dos planos de dados (de usuário) é uma das contribuições fundamentais da arquitetura NGN para o sucesso de suas implementações, como por exemplo o IMS.Além disso, destacam-se as vantagens que o Serviço VCC pode agregar ao IMS, contribuindo para sua adesão em menor prazo pelas operadoras de telecomunicações, dado que esse serviço contribui para a integração de redes, cada vez mais convergentes, agregando mobilidade e continuidade à sua utilização. / This work intends to study and implement the integration between the circuit switching domain and the IP Multimedia Subsystem (IMS) to support vertical handovers that are between different access networks, such as Global System for Mobile communications (GSM) and WiFi. Therefore the specifications are incomplete about this topic in standards from the entities who works with this subject. Then, is presented a new proposal for this integration: a new functional entity to realize this integration: the Call Data Storage Function (CDSF), which interacts with other modules of VCC Service and guarantees that some information shared between modules are not lost, due to conversion of signalling protocols in the interface between domains. Besides that, CDSF helps in the control of allocation of reference address that are used to route calls from one domain to another. Access protocols to CDSF are defined and CDSF methods are exposed. The CDSF design uses a modular approach, which allows future improvements, just changing modules. As case studies to validate this work proposal, call scenarios are presented that uses the VCC Service, using CDSF. Finally, it is concluded that the integration between domains is viable if this work proposal is used. It is presented, as well, that the separation between control plans and data plans is one of the main contributions of NGN architecture to the success of its implementations, like IMS. Furthermore, it is exposed the advantages that VCC Service can aggregate to IMS, contributing for more rapidly adoption by telecommunications operators, considering that this service helps the networks integration, adding convergence, mobility and continuity.