A utilização de sistemas baseados em computador em diversos domínios aumentou
significativamente nos últimos anos. Um dos principais desafios no desenvolvimento
de software de sistemas críticos é a garantia da sua correção e confiabilidade. Desta
forma, a verificação de software exerce um papel importante para assegurar a qualidade
geral do produto, visando principalmente características como previsibilidade e confiabilidade.
No contexto de verificação de software, os Bounded Model Checkers estão
sendo utilizados para descobrir erros sutis em projetos de sistemas de software atuais,
contribuindo eficazmente neste processo de verificação. O valor dos contra-exemplos e
propriedades de segurança gerados pelo Bounded Model Checkers para criar casos de
testes e para a depuração de sistemas é amplamente reconhecido. Quando um Bounded
Model Checking (BMC) encontra um erro ele produz um contra-exemplo. Assim,
o valor dos contra-exemplos para depuração de software é amplamente reconhecido no
estado da prática. Entretanto, os BMCs frequentemente produzem contra-exemplos
que são grandes ou difíceis de entender ou manipular, principalmente devido ao tamanho
do software e valores escolhidos pelo solucionador de satisfabilidade. Neste
trabalho visamos demonstrar e analisar o uso de método formal (através da técnica
model checking) no processo de desenvolvimento de programas na linguagem C, explorando
as características já providas pelo model checking como o contra-exemplo e a
identificação e verificação de propriedades de segurança. Em face disto apresentamos
duas abordagens: (i) descrevemos um método para integrar o Bounded Model Checker
ESBMC como o framework de teste unitário CUnit, este método visa extrair as
propriedades geradas pelo ESBMC para gerar automaticamente casos de teste usando
o rico conjunto de assertivas providas pelo framework CUnit e (ii) um método que
visa automatizar a coleta e manipulação dos contra-exemplos, de modo a instanciar o
programa C analisado, para comprovar a causa raiz do erro identificado. Tais métodos
podem ser vistos como um método complementar para a verificação efetuada pelos
BMCs. Demonstramos a eficácia dos métodos propostos sobre benchmarks públicos de
código C.
|
