Поиск новых ошибок методом верификации моделей с помощью подхода дельта отладки
https://doi.org/10.15514//ISPRAS-2023-35(3)-11
Аннотация
Зачастую инструмент формальной верификации моделей программ не может получить вердикт за ограниченное время из-за комбинаторного взрыва пространства состояний. Чтобы найти ошибки в верифицируемой программе за выделенное время, может быть проанализирована упрощённая её версия. В этой работе представлены алгоритмы DD**, основанные на подходе Delta Debugging, с помощью которых производится перебор упрощённых версий программы. Эти алгоритмы были реализованы в инструменте статической верификации программ CPAchecker. Наши эксперименты показали, что предложенный метод может быть использован для нахождения ошибок в программных системах, используемых на практике.
При поддержке: Автор благодарит своих коллег А.А. Васильева и В.С. Мутилина за советы по теме статьи.
Об авторе
Олег Максимович ПЕТРОВ
Московский государственный университет имени М.В. Ломоносова, Институт системного программирования им. В.П. Иванникова РАН.
Россия
Россия
Cтарший лаборант, магистр факультета вычислительной математики и кибернетики
Список литературы
1. A. V. Aho, R. Sethi, and J. D. Ullman, Compilers: Principles, Techniques, and Tools. Addison-Wesley, 1986.
2. D. Beyer and M. E. Keremoglu, “CPAchecker: A tool for configurable software verification,” in Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23. Springer, 2011, pp. 184–190.
3. D. Beyer, S. Gulwani, and D. A. Schmidt, Combining Model Checking and Data-Flow Analysis. in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018, pp. 493–540.
4. A. Khoroshilov, V. Mutilin, A. Petrenko, and V. Zakharov, “Establishing linux driver verification process,” in Perspectives of Systems Informatics: 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers 7. Springer, 2010, pp. 165–176.
5. I. S. Zakharov, M. U. Mandrykin, V. S. Mutilin, E. Novikov, A. K. Petrenko, and A. V. Khoroshilov, “Configurable toolset for static verification of operating systems kernel modules,” Programming and Computer Software, vol. 41, pp. 49–64, 2015.
6. D. Beyer, “Software verification: 10th comparative evaluation (SVCOMP 2021),” Tools and Algorithms for the Construction and Analysis of Systems, vol. 12652, pp. 401 – 422, 2021.
7. “Progress on software verification: SV-COMP 2022,” in International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2022.
8. “Competition on software verification and witness validation: SVCOMP 2023,” in International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2023.
9. N. Piterman and A. Pnueli, Temporal Logic and Fair Discrete Systems, in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018, p. 27–73.
10. A. V. Khoroshilov, M. U. Mandrykin, and V. S. Mutilin, “Introduction to CEGAR — counter-example guided abstraction refinement”, Trudy ISP RAN/Proc. ISP RAS, vol. 24, 2013, (in Russian).
11. D. A. Peled, Partial-Order Reduction, in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018.
12. E. M. Clarke, E. A. Emerson, S. Jha, and A. P. Sistla, “Symmetry reductions in model checking,” in International Conference on Computer Aided Verification, 1998.
13. S. Chaki and A. Gurfinkel, BDD-Based Symbolic Model Checking, in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018, p. 219–245.
14. A. Biere and D. Kröning, SAT-based model checking, in E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, eds. Handbook of Model Checking, 1st ed. Cham: Springer International Publishing, 2018, ch. 10, pp. 277–303.
15. F. Nejati, A. A. A. Ghani, N. K. Yap, and A. B. Jafaar, “Handling state space explosion in component-based software verification: A review,” IEEE Access, vol. 9, pp. 77 526–77 544, 2021.
16. S. Apel, D. Beyer, V. O. Mordan, V. S. Mutilin, and A. Stahlbauer, “On-the-fly decomposition of specifications in software model checking,” Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016.
17. T. A. Henzinger, R. Jhala, R. Majumdar, and M. A. A. Sanvido, “Extreme model checking,” in Theory and Practice, 2003.
18. D. Beyer, S. Lo¨we, E. Novikov, A. Stahlbauer, and P. Wendler, “Precision reuse for efficient regression verification,” in ESEC/FSE 2013, 2013.
19. D. Beyer, T. A. Henzinger, M. E. Keremoglu, and P. Wendler, “Conditional model checking: a technique to pass information between verifiers,” in SIGSOFT FSE, 2012.
20. D. Beyer and S. Kanav, “CoVeriTeam: On-demand composition of cooperative verification systems,” in International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2022.
21. M. Weiser, “Program slicing,” IEEE Transactions on Software Engineering, vol. SE-10, no. 4, pp. 352–357, 1984.
22. M. Chalupa and J. Strejček, “Evaluation of program slicing in software verification,” in International Conference on Integrated Formal Methods, 2019.
23. P. Andrianov, V. Mutilin, M. Mandrykin, and A. Vasilyev, “CPA-BAM-Slicing: Block-abstraction memoization and slicing with region-based dependency analysis,” in Tools and Algorithms for the Construction and Analysis of Systems, D. Beyer and M. Huisman, Eds. Cham: Springer International Publishing, 2018, pp. 427–431.
24. M. Spiessl, “Configurable software verification based on slicing abstractions,” Master’s thesis, Ludwig-Maximilians-Universita¨t Mu¨nchen (LMU Munich), Mu¨nchen, Germany, Jun. 2018.
25. A. Zeller and R. Hildebrandt, “Simplifying and isolating failure-inducing input,” IEEE Trans. Software Eng., vol. 28, pp. 183–200, 2002.
26. G. Misherghi and Z. Su, “HDD: hierarchical delta debugging,” Proceedings of the 28th international conference on Software engineering, 2006.
27. D. Vince, R. Hodován, D. Bársony, and Á. Kiss, “The effect of hoisting on variants of Hierarchical Delta Debugging,” Journal of Software: Evolution and Process, vol. 34, 2022.
28. C. G. Kalhauge and J. Palsberg, “Binary reduction of dependency graphs,” Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2019.
29. D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, D. Beyer, M. Dangl, D. Dietsch, M. Heizmann, and T. Lemberger, “Verification witnesses,” ACM Transactions on Software Engineering and Methodology (TOSEM), vol. 31, pp. 1 – 69, 2022.
30. M. Dangl, S. Löwe, and P. Wendler, “CPAchecker with support for recursive programs and floating-point arithmetic,” in Tools and Algorithms for the Construction and Analysis of Systems, C. Baier and C. Tinelli, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2015, pp. 423– 425.
31. E. Novikov and I. Zakharov, “Towards automated static verification of GNU C programs,” in Perspectives of System Informatics: 11th International Andrei P. Ershov Informatics Conference, PSI 2017, Moscow, Russia, June 27-29, 2017, Revised Selected Papers 11. Springer, 2018, pp. 402–416.
32. A. A. Vasilyev and V. S. Mutilin, “Predicate extension of symbolic memory graphs for the analysis of memory safety correctness,” Programming and Computer Software, vol. 46, pp. 747 – 754, 2020.
Рецензия
Для цитирования:
ПЕТРОВ О.М. Поиск новых ошибок методом верификации моделей с помощью подхода дельта отладки. Труды Института системного программирования РАН. 2023;35(3):151-162. https://doi.org/10.15514//ISPRAS-2023-35(3)-11
For citation:
PETROV O.M. Finding More Bugs with Software Model Checking using Delta Debugging. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2023;35(3):151-162. https://doi.org/10.15514//ISPRAS-2023-35(3)-11
Послать статью по эл. почте 