Комбинация методов статической верификации композиции требований
https://doi.org/10.15514/ISPRAS-2017-29(3)-9
Аннотация
Статическая верификация программного обеспечения доказывает выполнение требований в программах, однако для этого необходимо большое количество вычислительных ресурсов, кроме того, соответствующая задача не всегда может быть решена. На данный момент не существует универсальный метод статической верификации, который мог бы эффективно проверять произвольные программы, поэтому на практике необходимо выбирать более подходящий метод и настраивать его под конкретную задачу. В данной статье предлагается комбинировать различные методы для повышения производительности и улучшения результата верификации, что можно рассматривать как первый шаг в создании универсального метода статической верификации. Предложенные методы были реализованы для комбинации активно развивающихся в настоящее время методов верификации композиции требований. Апробация реализованных методов на модулях ядра операционной системы Linux продемонстрировала их преимущества относительно отдельного применения методов верификации композиции требований.
Список литературы
1. Turing A. M. On Computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, pp. 230-265, 1936.
2. Corbet J., Kroah-Hartman G., McPherson A. Linux kernel development. How Fast it is Going, Who is Doing It, What They are Doing, and Who is Sponsoring It. https://www.linux.com/publications/linux-kernel-development-how-fast-it-going-who-doing-it-what-they-are-doing-and-who-5, дата обращения 10.06.2017.
3. Мутилин В. С., Новиков Е. М., Хорошилов А. В. Анализ типовых ошибок в драйверах операционной системы Linux. Труды ИСП РАН, т. 22, с. 349-374, 2012. DOI: 10.15514/ISPRAS-2012-22-19.
4. Mordan V., Novikov E. Minimizing the number of static verifier traces to reduce time for finding bugs in Linux kernel modules. Proceedings of 8th Spring/Summer Young Researchers Colloquium on Software Engineering, vol. 1, 2014. DOI: 10.15514/syrcose-2014-8-5.
5. Mordan V., Mutilin V. Checking several requirements at once by CEGAR. LNCS, vol. 9609, pp. 218-232, 2016. DOI: 10.1007/978-3-319-41579-6_17.
6. Мордань В. О., Мутилин В. С. Проверка нескольких требований за один запуск инструмента статической верификации с помощью CEGAR. Программирование, т. 4. с. 225-238, 2016.
7. Apel S., Beyer D., Mordan V., Mutilin V., Stahlbauer A. On-The-Fly Decomposition of Specifications in Software Model Checking. Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, pp. 349-361, 2016. DOI: 10.1145/2950290.2950349.
8. Beyer D., Henzinger T. A., Keremoglu M. E., Wendler P. Conditional model checking: a technique to pass information between verifiers. Proceedings ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering (FSE 2012), article 57, 2012. DOI: 10.1145/2393596.2393664.
9. Новиков Е. М. Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы Linux. Диссертация на соискание ученой степени кандидата физико-математических наук. ИСП РАН, 2013.
10. Beyer D., Chlipala A., Henzinger T. A., Jhala R., Majumdar R. The BLAST query language for software verification. Proceedings of SAS. LNCS, vol. 3148, pp. 2-18, 2004. DOI: 10.1007/978-3-540-27864-1_2.
11. Clarke E., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-guided abstraction refinement. Proceedings of CAV, LNCS, vol. 1855, pp. 154-169, 2000. DOI: 10.1007/10722167_15.
12. Beyer D. Reliable and Reproducible Competition Results with BenchExec and Witnesses (Report on SV-COMP 2016). Proceedings of TACAS. LNCS, vol. 9636, pp. 887-904, 2016. DOI: 10.1007/978-3-662-49674-9_55.
13. Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST. International Journal on Software Tools for Technology Transfer, vol. 9, issue 5, pp. 505-525, 2007. DOI: 10.1007/s10009-007-0044-z.
14. Beyer D., Keremoglu M. CPAchecker: A tool for configurable software verification. Proceedings of Computer Aided Verification. LNCS, vol. 6806, pp. 184–190, 2011. DOI: 10.1007/978-3-642-22110-1_16.
15. Khoroshilov A., Mutilin V., Novikov E., Shved P., Strakh A. Towards an open framework for C verification tools benchmarking. Perspectives of Systems Informatics. LNCS, vol. 7162, pp. 179-192, 2012. DOI: 10.1007/978-3-642-29709-0_17.
16. Ball T., Rajamani S. K. The SLAM project. Debugging system software via static analysis. Proceedings of Symposium on Principles of Programming Languages (POPL), pp. 1–3, 2002. DOI: 10.1145/565816.503274.
17. Мордань В. О. Методы верификации программ на основе композиции задач достижимости. Диссертация на соискание ученой степени кандидата физико-математических наук. ИСП РАН, 2017.
18. Beyer D., Wendler P. Reuse of verification results. Proceedings of the 20th International Workshop on Model Checking Software (SPIN 2013). LNCS, vol. 7976, pp. 1-17, 2013. DOI: 10.1007/978-3-642-39176-7_1.
19. Beyer D., Keremoglu M., Wendler P. Predicate abstraction with adjustable-block encoding. Proceedings of Formal Methods in Computer-Aided Design, pp. 189-198, 2010.
20. Beyer D., Löwe S. Explicit-state software model checking based on CEGAR and interpolation. Proceedings of the 16th International Conference on Fundamental Approaches to Software Engineering (FASE 2013). LNCS, vol. 7793, pp. 146-162, 2013. DOI: 10.1007/978-3-642-37057-1_11.
Рецензия
Для цитирования:
Мордань В.О. Комбинация методов статической верификации композиции требований. Труды Института системного программирования РАН. 2017;29(3):151-170. https://doi.org/10.15514/ISPRAS-2017-29(3)-9
For citation:
Mordan V.O. Combination of static verification methods for checking requirements composition. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(3):151-170. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(3)-9
Послать статью по эл. почте 