Возможности и ограничения инструментов верификации моделей программ
https://doi.org/10.15514/ISPRAS-2021-33(6)-1
Аннотация
Инструменты верификации моделей программ позволяют автоматически искать нарушения специфицированных требований в программах, а также доказывать их корректность формально при выполнении определенных условий. Данные инструменты развивались достаточно активно два последних десятилетия. За это время они были успешно использованы в ходе верификации нескольких промышленных проектов, в первую очередь ядра и драйверов различных операционных систем. Данная статья рассматривает интерфейс инструментов верификации моделей программ, их уникальные возможности, а также ограничения, которые затрудняют их широкомасштабное практическое применение.
Об авторе
Евгений Михайлович НОВИКОВ
Институт системного программирования им. В.П. Иванникова РАН
Россия
Россия
Кандидат физико-математических наук, ведущий научный сотрудник и руководитель программных проектов отдела технологий программирования
Список литературы
1. P.E. Black, L. Badger et al. Dramatically reducing software vulnerabilities: report to the White House Office of Science and Technology Policy. Technical Report NISTIR 8151, National Institute of Standards and Technology, Gaithersburg, MD, 2016.
2. G. Klein, J. Andronick et al. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, volume 32, issue 1, 2014, pp. 1-70.
3. D. Efremov, M. Mandrykin, A. Khoroshilov. Deductive verification of unmodified Linux kernel library functions. Lecture Notes in Computer Science, vol. 11245, 2018, pp. 216-234.
4. D. Beyer. Competition on software verification. Lecture Notes in Computer Science, vol. 7214, 2012, pp. 504-524.
5. D. Beyer. Software verification: 10th comparative evaluation (SV-COMP 2021). Lecture Notes in Computer Science, vol. 12652, 2021, pp. 401–422.
6. Definitions and Rules of 10th International Competition on Software Verification. URL: https://sv-comp.sosy-lab.org/2021/rules.php, accessed 12.12.2021.
7. V. Mutilin, E. Novikov, A. Khoroshilov. Analysis of typical faults in Linux operating system drivers. Trudy ISP RAN/Proc. ISP RAS, vol. 22, 2012, pp. 349-374 (in Russian). https://doi.org/10.15514/ISPRAS-2012-22-19.
8. P. Andrianov. Analysis of correct synchronization of operating system components. Programming and Computer Software, vol. 46, issue 8, 2020, pp. 712-730. https://doi.org/10.1134/S0361768820080022.
9. I. Zakharov. A survey of high-performance computing for software verification. Communications in Computer and Information Science, vol. 779, 2017, pp. 196-208.
10. I. Zakharov, E. Novikov. Compositional environment modelling for verification of GNU C programs. In: Proc. of the Ivannikov Ispras Open Conference, 2018, pp. 39–44.
11. Exchange Format for Violation Witnesses and Correctness Witnesses. URL: https://github.com/sosy-lab/sv-witnesses, accessed 12.12.2021.
12. D. Beyer, M. Dangl et al. Correctness witnesses: exchanging verification results between verifiers. In Proc. of the 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2016, pp. 326-337.
13. D. Beyer, M. Dangl et al. Witness validation and stepwise testification across software verifiers. In Proc. of the 10th Joint Meeting on Foundations of Software Engineering, 2015, pp. 721-733.
14. D. Beyer, M.E. Keremoglu. CPAchecker: a tool for configurable software verification. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 184–190.
15. R. Castaño, V. Braberman et al. Model checker execution reports. In Proc. of the 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017, pp. 200-205.
16. LCOV – the LTP GCOV extension. URL: https://github.com/linux-test-project/lcov, accessed 12.12.2021.
17. T. Ball, V. Levin, S.K. Rajamani. A decade of software model checking with SLAM. Communications of the ACM, vol. 54, issue 7, 2011, pp. 68-76.
18. Klever: a software verification framework. URL: https://forge.ispras.ru/projects/klever, accessed 12.12.2021.
19. E. Novikov and I. Zakharov. Towards automated static verification of GNU C programs. Lecture Notes in Computer Science, vol. 10742, 2018, pp. 402-416.
20. VerifierCloud Web Interface. URL: https://vcloud.sosy-lab.org, accessed 12.12.2021.
Рецензия
Для цитирования:
НОВИКОВ Е.М. Возможности и ограничения инструментов верификации моделей программ. Труды Института системного программирования РАН. 2021;33(6):7-14. https://doi.org/10.15514/ISPRAS-2021-33(6)-1
For citation:
NOVIKOV E.M. Capabilities and Restrictions of Software Model Checkers. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(6):7-14. https://doi.org/10.15514/ISPRAS-2021-33(6)-1
Послать статью по эл. почте 