Verificação de programas multi-tarefas baseado no framework multiplataforma QT

Abstract

With the advancement of technology, progress has been made with respect to the development of hardware and software. The result of such advances is due to the evolution of applications, which currently require more data processing and storage capacity. From this reality, the industry invests heavily in automatic and fast verification processes, in order to obtain the reduction of error rates present in the developed systems, which thus becomes necessary, during the process of development of these systems, the use of such techniques suitable for the implementation of parallelism and data synchronization, such as data race, so that it can be extracted, the maximum performance of the system being produced. With this in mind, the development process time and the robustness of these systems, are becoming smaller, with that the use of framework in the development process has been very used. A framework that is in evidence now is the Qt multi-platform development framework, which has a large set of libraries for easy deployment, maintenance and portability for multi-thread systems. In this dissertation, we propose a set of simplified Qt multi-threaded libraries, similar to the standard library for the creation and manipulation of threads within the Qt framework. These models are integrated with the Efficient SMT-Based Bounded Model Checker (ESBMC), so that through the operational models, it is possible to analyze real applications that use the Qt framework, which implements concurrent programming. Through the simplified Qt multi-threaded Operational Model, we can perform an evaluation of the methodology proposed with other model verifiers, with the purpose of evaluating the feasibility of the approach we propose. Thus, the methodology we propose here is in the state-of-the-art, being the first one to make feasible the verification of multi-thread structures of the Qt framework, and can be expanded, to other structures that have not yet been covered.