НАУКА и ОБРАЗОВАНИЕ

Файл статьи: SE-BMSTU...o251.pdf (928.63Кб)

УДК 004.3+519.6

1 МГТУ им. Н.Э. Баумана, Москва, Россия

Данная статья посвящена актуальной проблеме верификации программного обеспечения (ПО). Методы верификации ПО предназначены для проверки программного обеспечения на соответствие заявленным требованиям. Таким как корректность, безопасность системы, адаптируемость системы к небольшим изменениям окружения, переносимость и совместимость и.т.д. Такие методы разнообразны по способу работы и способу достижения конечного результата. В статье рассмотрены статические и динамические методы верификации программного обеспечения и уделено внимание методу символьного выполнения. В рамках обзора статического анализа, рассмотрены и описаны дедуктивный метод и методы проверки модели. Уделено внимание актуальному вопросу о преимуществах и недостатках того или иного методы. Рассмотрена классификация методов тестирования для каждого метода. В работе представлены и проанализированы характеристики статического анализа и механизмы зависимостей, а также их виды, который позволяют сократить число ложных срабатываний в ситуациях, когда текущее состояние программы объединяет два или более состояний, полученных на различных путях выполнения, а также при работе с множественными значениями объектов. Зависимости связывают различные типы программных объектов: одиночные переменные, элементы составных переменных (поля структур, элементы массивов), размеры участков динамической памяти, длины строк, количества инициализированных элементов массивов, при верификации кода с помощью статических методов. В стать уделено внимание выявлению зависимостей в рамках метода абстрактной интерпретации, а так обзор и анализ средств логического вывода.
Представлены и проанализированы методы динамического анализа. Такие как тестирование, мониторинг и профилирование так же рассмотрены виды инструментованы, который могут быть применены к программному обеспечения при использовании методов динамического анализа. На основе проведенной работы сформировано заключение, в котором описаны наиболее актуальные проблемы методов анализы, способы их решения и то на каких этапах разработки целесообразно применять тот или иной метод.

1. Бурякова Н.А., Чернов А.В. Классификация частично формализованных и формальных моделей и методов верификации программного обеспечения // Инженерный Вестник Дона. 2010. № 4. C. 129-134.
2. Кулямин В.В. Методы верификации программного обеспечения. 2008. 117 с. // Единое окно доступа к информационным ресурсам: интернет-портал. Режим доступа: http://window.edu.ru/resource/168/56168 (дата обращения 01.09.2015).
3. Карпов Ю . Г . MODEL CHECKING. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2010. 560 с.
4. Pasareanu C.S., Visser W. A survey of new trends in symbolic execution for software testing and analysis // International Journal on Software Tools for Technology Transfer. 2009. Vol.11, no. 2. P. 339-353. DOI: 10.1007/s10009-009-0118-1
5. Boyer R.S., Elspas B., Levitt K.N. SELECT - a formal system for testing and debugging programs by symbolic execution // Proceedings of the International Conference on Reliable Software, Los Angeles, California, 1975. ACM New York , NY , USA , 1975. P . 234-254. DOI:10.1145/800027.808445
6. Лаврищева Е.М., Петрухин В.А. Методы и средства инженерии программного обеспечения: учебник. М.: МФТИ, 2006. 304 с.
7. Boehm B., Basili V. Top 10 list [software development] // IEEE Computer. 2001. Vol. 34, no. 1. P. 135-137. DOI: 10.1109/2.962984
8. Beyer D. Status report on software verification (competition summary SV-COMP 2014) // Tools and Algorithms for the Construction and Analysis of Systems / ed. by E. Ábrahám, K. Havelund. Springer Berlin Heidelberg , 2014. P. 373-388. DOI: 10.1007/978-3-642-54862-8_25 (Ser. Lecture Notes in Computer Science; vol. 8413.).
9. Вельдер С.Э., Шалыто А.А. Верификация простых автоматных программ на основе метода Model Checking // XV Международная научно-методическая конференция «Высокие интеллектуальные технологии и инновации в образовании и науке»: матер. СПб.: СПбГПУ, 2008. С. 285-288.
10. Лифшиц Ю. Верификация программ и темпоральные логики. Лекция № 3 курса «Современные задачи теоретической информатики». СПб., ИТМО, 2005. C . 3-8. Режим доступа: http://yury.name/modern/03modernnote.pdf (дата обращения 01.09.2015).
11. Мандрыкин М.У., Мутилин В.С., Новиков Е.М., Хорошилов А.В. Обзор инструментов статической верификации Си программ в применении к драйверам устройств операционной системы Linux // Сборник трудов Института системного программирования РАН. Т. 22. М .: ИСП РАН , 2012. C. 293-294. DOI:10.15514/ISPRAS-2012-22-17
12. Глухих М.И., Ицыксон В.М., Цесько В.А. Использование зависимостей для повышения точности статического анализа программ // Моделирование и анализ информационных систем. 2011. № 4. C. 68-79.
13. Nielson F., Nielson N., Hankin C. Principles of Program Analysis. Corr. 2^nd printing. Springer, 2005. 452 p.
14. Cousot P. Abstract Interpretation // ACM Computing Surveys. 1996. Vol . 28, no . 2. P . 324-328. DOI:10.1145/234528.234740
15. Гурин Р.Е. Обзор и анализ инструментов, который осуществляют верификацию бинарного кода программы // Новые информационные технологии в автоматизированных системах: материалы 17-го научно-практического семинара. Вып. 17. М.: ИПМ им. М.В. Келдыша, 2014. C. 514-518.
16. Рудаков И.В., Гурин Р.Е., Ребриков А.В. Верификация программного обеспечения: обзор методов и характеристик // Национальная ассоциация ученых (НАУ). Ежемесячный журнал. 2014. № 3, ч. 2. C. 22-26.