A utilização de sistemas embarcados, sistemas computacionais especializados para realizar uma função em sistemas maiores, eletrônicos ou mecânicos, vem crescendo no dia a dia das pessoas, e vem se tornando cada vez mais importante garantir a robustez desses sistemas. Existem diversas técnicas para garantir que um sistema seja lançado sem erros. Em especial, a verificação formal de programas está se mostrando efetiva na busca por falhas. Neste trabalho, serão descritos a verificação formal de programas C++ e a prova de corretude por indução matemática. Ambas as técnicas serão desenvolvidas utilizando a ferramenta Efficient SMTBased Context-Bounded Model Checker (ESBMC), um verificador de modelos que se baseia
em teorias de satisfabilidade de fórmulas proposicionais e de lógica de primeira ordem. Os experimentos mostram que a ferramenta pode ser utilizada para verificar uma ampla gama de aplicações, de casos simples à aplicações comerciais. A ferramenta também mostrou-se superior em comparação com outros verificadores na verificação de programas C++, encontrando um maior número de erros e suportando um número superior das funcionalidades que a linguagem C++ tem a oferecer, além de ser capaz de provar diversas propriedades (por exemplo, laços invariantes), utilizando a técnica de indução matemática.
|
