We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
Bounded model checking of C++ programs based on the Qt cross-platform framework.
- Authors
Monteiro, Felipe R.; Garcia, Mário A. P.; Cordeiro, Lucas C.; Lima Filho, Eddie B.
- 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, technology companies tend to invest in fast and automatic verification mechanisms, to create robust systems and reduce product recall rates. In addition, further development-time reduction and system robustness can be achieved through cross-platform frameworks, such as Qt, which favor the reliable port of software stacks to different devices. Based on that, the present paper proposes a simplified version of the Qt framework, which is integrated into a checker based on satisfiability modulo theories (SMT), known as the Efficient SMT-based Context-Bounded Model Checker, for verifying actual Qt-based applications, with a success rate of 89%, for the developed benchmark suite. Furthermore, the simplified version of the Qt framework, named as Qt Operational Model, was also evaluated using other state-of-the-art verifiers for C++ programs. In fact, Qt Operational Model was combined with 2 different verification approaches: explicit-state model checking and also symbolic (bounded) model checking, during the experimental evaluation, which highlights its flexibility. The proposed methodology is the first one to formally verify Qt-based applications, which has the potential to devise new directions for software verification of portable code.
- Subjects
C++; OBJECT-oriented programming languages; PROGRAMMING languages; C (Computer program language); COMPUTER software development
- Publication
Software Testing: Verification & Reliability, 2017, Vol 27, Issue 3, pn/a
- ISSN
0960-0833
- Publication type
Article
- DOI
10.1002/stvr.1632