Um método para verificação formal e dinâmica de sistemas de software concorrentes

Abstract

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.