Bounded model checking of C++ programs based on the Qt cross‐platform framework
Bounded model checking of C++ programs based on the Qt cross‐platform framework
复制标题
基于Qt跨平台框架的C++程序有界模型检查
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Eddie Filho
中科院分区：
文献类型：
--
作者：
Felipe R. Monteiro;Mário A. P. Garcia;L. Cordeiro;Eddie Filho
嵌入式系统的软件开发过程越来越快，这通常会导致相关复杂性的增加。因此，技术公司倾向于投资快速和自动验证机制，以创建强大的系统并降低产品召回率。此外，通过跨平台框架（如Qt）可以进一步减少开发时间和系统健壮性，这有利于将软件堆栈可靠地移植到不同的设备。在此基础上，本文提出了一个简化版本的Qt框架，它被集成到一个基于可满足性模理论（SMT）的检查器中，称为基于有效SMT的上下文有界模型验证器，用于验证实际的基于Qt的应用程序，成功率为89%，用于开发的基准测试套件。此外，Qt框架的简化版本，称为Qt操作模型，也使用其他最先进的C++程序验证器进行了评估。事实上，Qt操作模型在实验评估期间结合了两种不同的验证方法：显式状态模型检查和符号（有界）模型检查，这突出了其灵活性。该方法是第一个正式验证基于Qt的应用程序的方法，它有可能为可移植代码的软件验证设计新的方向。
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.