Verificação de Programas Embarcados ANSI-C baseada em indução Matemática e Invariantes

Abstract

The use of embedded systems, i.e., computer systems focused on performing specific functions in larger (electronic or mechanical) systems, has been growing lately, and ensuring the robustness of such systems has become increasingly important. There are several techniques to ensure that a system is released without errors. In particular, formal verification of programs is proving itself to be effective in the search for failures. In this work, an induction-proof algorithm is described, which combines k-induction and invariants to verify and refute safety properties in embedded ANSI-C software. Moreover, the proposed k-induction-based approach infers invariants in the program to assist in verification tasks, using constraint refinement (i.e., polyhedral) to specify pre- and post-conditions. We adopted two invariant generators to produce such and feed the k-induction algorithm, which is implemented in the Efficient SMT-Based Context-Bounded Model Checker tool. Public benchmarks were used to assess the effectiveness of our approach. In addition, a comparison to other state-of-the-art verification tools using a set of benchmarks from the International Competition for Software Verification in addition to embedded systems applications. Experimental results have shown that the proposed approach, with and without invariants, can verify a wide variety of safety properties in programs with loops and embedded software from telecommunications, control systems, and medical domains.