Bounded Model Checking of C++ Programs Based on the Qt Framework (extended version)

TL;DR

This paper introduces a simplified Qt framework integrated with an SMT-based bounded model checker to verify C++ applications, achieving a 94.45% success rate in testing embedded systems.

Contribution

It presents a novel simplified Qt framework and its integration into a bounded model checking tool for verifying C++ embedded applications.

Findings

Success rate of 94.45% on test suite

Effective verification of C++ Qt-based applications

Enhanced verification process for embedded systems

Abstract

The software development process for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification processes, in order to create robust systems and reduce product recall rates. Because of that, the present paper proposes a simplified version of the Qt framework, which is integrated into the Efficient SMT-Based Bounded Model Checking tool to verify actual applications that use the mentioned framework. The method proposed in this paper presents a success rate of 94.45%, for the developed test suite.