Verificação de sistemas de software baseada em transformações de código usando Bounded Model Checking

Abstract

Oneofthemainchallenges insoftwaredevelopment istoensurethesafetyofthesoftwaresystems, especially in critical embedded systems, such as aircraft or healthcare, where several constraints (e.g., response time and data accuracy) must be met and measured in accordance with the user requirements, otherwise a failure can lead to catastrophic situations. Thus, software verification and testing techniques are essential items for the software development with quality, where such techniques aim to confirm the user requirements, as well as, the predetermined behaviors for the software. In the software verification context, aiming the product quality, the formal verification technique called model checking has been used to find subtle errors in actual projects of the software systems. However, the use of the model checking technique presents some challenges such as dealing with the model’s state explosion problem, integration with software testing environments more familiar to designers, and handling counter-examples to reproduce the identified errors. In order to deal with these problems, a possible solution is to explore the characteristics already provided by the model checkers, e.g., verification of the safety properties and generation of counter-examples. Exploring this set of characteristics, coupled with the use of program invariants inference and a special kind of model checking, called Bounded Model Checking (BMC), this thesis presents a set of methods to complement and enhance the scalability and accuracy of the verification performed by Bounded Model Checkers. These methods adopted code transformation techniques to explore the characteristics of Bounded Model Checkers to analyze the safety properties and demonstrate errors in programs written inthe C programming language. The methods presented in this thesis are: (1) The automatic generation and verification of the test cases based on safety properties generated by a Bounded Model Checker for unit tests; (2) Automating thecollection andmanipulation of thedatafrom thecounter-examples, todemonstrate the main cause of the identified error; and (3) Adopting program invariants dynamically/statically inferred from the analyzed program, to restrict the exploration of the states sets while performing the verification by the BMC. This way, helping to improve the verification performed by a BMC, related to assist in the verification and accuracy of results, by adoption of the program invariants. The proposed approaches when used separately, provide additional options to the verification, and interconnected, improving the code verification. Theexperimental results of theproposed methods show to be efficient over public available benchmarks of C programs, finding errors not previously found byother methods that are state-of-the-art.