В статье идет речьобисследовании и классификации методов верификации программного обеспечения (ПО). Осуществлен обзор имеющихся статических методов верификации, исследованы характеристики методов и осуществлено исследование на обнаружение зависимостей в рамках метода абстрактной интерпретации. В статье показан обзор и классификация динамических методов верификации ПО. Классификация выполнена по ряду главных критериев, таких как: вид метода, уровень автоматизации, уровень функциональной применимости, точность, типы обнаруживаемых ошибок, эффективность, область соответствия метода, время выполнения и способ достижения результата. Выполнен обзор видов тестирования и средств логического вывода и рассмотрены основные особенности методов верификации. Обнаружены недостатки имеющихся способов верификации программ.
Ключевые слова:верификация, статический анализ, динамический анализ, интерпретация, символьное выполнение, проверка модели
Одна из главных проблем при разработке программного обеспечения является верификация программного обеспечения. Средства верификации программного обеспечения создаются специально для подтверждения требованиям заявленного конечного программного продукта, сама цель верификации программного обеспечения является обнаружение ошибок, некорректных свойств и уязвимость программы [1, с. 129–134]. Актуальной проблемой является формирование новой классификации способов верификациипрограммного обеспечения, и дает возможность рассмотреть существующие в настоящее время методы верификации ПО, обнаружить их преимущество и недостатки. Классификация и анализ существующих способов дает создать список требований и рекомендаций для будущего исследования и разработкисинтетического метода верификации программного обеспечения, по принципу SMT — решателя.
Современные способы верификации можно поделить на эмпирические (те, которые используют экспертизу), формальные (которые используют математический аппарат верификации ПО) и формальные (которые проверяют работу программу с помощью запуска), уровни автоматизации делятся на ручные, автоматические и автоматизированные.
Одна из главных целей верификации программного обеспечения является проверка созданного программного кода техническому заданию и ее требования функциональности [2, с. 285–288].
Проверки документации и кода программного обеспечения с нормами и стандартам проведение оформлениями использует экспертиза, которые установлены в стране, отрасли и организации. Сама экспертиза может быть специализированной и общей.
Понятие верификации программного обеспечения в одной из нотаций [3, с. 272] обозначает символьное выполнение программы или проверку кода на наличие ошибок и уязвимости способов проверки модели.
Широко используется в настоящее время техника символьного выполнения [4–5, с. 68–79, 374], что позволяет проводить моделирование выполнения программы, при этом часть переменных представляются в символьном виде. Символ переменной показывает, что большинство значении входной переменны программы из области ее определения. Каждое символьное выполнение равноценно выполнению ПО, в наборе конкретных текстовых значении переменных, котороесокращает мощность множества изобретаемых тестов. Тоже самое означает альтернативная семантика исполнения программы — семантика условного выполнение для языка программирования, в котором объекты данных представлены в виде символов. Для работы с символьными значениями для этого семантика показывает пути расширения основных конструкции языков программирования.
Главные этапы верификации программного обеспечения — это тестирование программ на пригодность провозглашенным качественным характеристикам. Самые важные характеристики ПО перечислены ниже:
- Корректность (аналогично системе своего назначение);
- Безопасность системы;
- Устойчивость системы в случае недетерминированного поведения окружения (например, неправильные входные данные);
- Эффективность использования ресурсов времени и памяти;
- Адаптируемость системы к небольшим преобразованиям окружения;
- Переносимость и совместимость.
Экспертиза является самым популярным методом тестирование программ [2, с. 285–288]. Другими словами, это анализ ПО, проводимым экспертом, который может быть и разработчиком так же лицом, или группой лиц, привлеченных со стороны, для оценки ПО.
Тестирование программного обеспечения выполняется группой квалифицированных специалистов, но невозможно выполнить автоматически потому, что все этапы выполняются экспертами. При том что этот способ имеет высокую функциональную пригодность и способен решать огромный круг задач тестирование программного обеспечения, при этом может быть применим к любым свойствам ПО на любом этапе тестирование программ. Качество экспертизы зависит от опыта специалистов, выполняющих ее. С помощью метода экспертизы обнаруживают от 50 до 90 % ошибок и уязвимостей ПО [7, с. 560]. Такой метод помогает обнаружить фактически любые виды ошибок и считается одним из лучших способов, но только если экспертизу проводят опытные специалисты. И самым главным преимуществом является то что тестирование возможно проводить на любом этапе разработки проекта. Срок выполнение тестирование зависит от сложности программы и опытности команды специалистов. Из чего следует, что приоритетом этого метода является возможность использовать на любом этапе проекта и быстро устранить ошибки и уязвимости.
Формальные методы верификации — это верификация математической модели программы, а не ее исходный код. Требования к программе определяется в виде спецификации, то есть проверяется требование спецификации на модели программы. [1, с. 129–134]
Если сравнивать с экспертизой, то формальный метод является более выгодным для авторизации процесса верификации и создание моделей программ. Для создание математической модели всегда нужен опытный специалист. Формальные методы наделены отличительной особенностью это высокой функциональной пригодностью и точностью, если только создана адекватная формальная модель.
Изъян формального верификации — это не всегда возможность создать более адекватную математическую модель, при этом сохранить эффективность работы ее в промышленных проектах. Этот метод можно использовать к тем проверенным участкам, которые можно учесть в формальной модели.
Преимуществом проверки моделей является допустимость автоматизации процесса тестирования и строение модели. Создание формальной модели дает увидеть код программы в виде ряд логических выражений, позволяя наблюдать свойства программы, показанные в виде спецификации.
Статический анализ программы — это исследование выполняется без фактического выполнения программы. В основном исследуется определенная версия исходного кода. Динамический анализ дает анализировать все пути выполнения программы. Используется в том случае, если исследование выполняется с помощью автоматизированныхинструментов.
В настоящем мире существуют две самые популярные группы методов статической верификации: это методы дедуктивного исследования программ метод проверки модели [11, с. 293–326].
Методы дедуктивного анализа применяется на основании пригодностипрограммы своей спецификации, как правило задаваемый в виде пред и постусловий. На данном уровне прогресс — это инструменты не пригодны для исследования больших программ потому, что требуют ручной аннотации функции и циклов в коде программы [13, с. 452].
Способы проверки модели основываются из кода программы и создают ее математическую модель, обычно в качестве модели используют Крипк [13, с. 452], после этого анализируют эту модель на предмет исполнения установленных условии и ограничений.
Методы статического анализа не зависят от использования компилятора и среды, что дает обнаружить скрытые ошибки, и не понятные поведения программы. С легкостью определяет ошибки в тексте программы, наделенный вставкой и копирования разных частей кода. Статический анализ мало эффективен в обнаружение ошибок, сцепленный с утечкой памяти, и имеет отличительную черту создавать огромное количество ложных срабатываний указывая все подозрительные места в тексте, но современные методы имеют большую точность и полный анализ [14, с. 244].
Верификация методом статического анализа более плодотворна на этапе создания ПО, так как статический анализ пригодный к данному тексту программы и не имеет в виду ее исполнение, это позволяет уменьшить стоимость проекта и увеличить его надежность. Инструменты автоматической верификации на основе статического анализа, используются довольно неограниченно потому, что уместные и нетрудные в выполнении не требуют специальной подготовки программы.
Эти методы, для которых анализ программного обеспечения осуществляются при помощи реального выполнения программы. Если имитационный моделирование реализовывает не сама программа, а программа ее моделирующая, то на вход программы действует последовательность данных, которые имеют возможность создавать недетерминированное поведение, таким способом допускает выявлению уязвимости и ошибки.
Мониторинг — это такой метод, при котором исходит проверка, регистрация и оценка работы ПО [2, с. 285–288]. Протоколируемая информация подчиняется от оценки характеристик системы. Получая данные о работе, при этом используются разные методы инструментированная и это все является мониторинг.
Инструментирование дает возможность следить или установить качественные параметры уровня производительности ПО, и имеет вероятность распознавать ошибки и записывать информацию для наблюдения причины их появлению.
Тестирование ПО адресовано на обнаружение тех ситуации в программном коде, в таких где поведение программы становится недетерминированным, не правильным и не соответствующим спецификации. Как правило, тестирование выполняются в рамках известных, заданных сценариев.
Подготовка тестов выполняется вручную, также можно автоматизировать сам процесс тестирования мониторинг. При отсутствие исходного кода, способы динамического исследования могут разрешить выполнить проверку программы, способом формирования контролируемой среды выполнения программы и дает возможность найти большое количество ошибок и получить точную оценку качества сложной системы. Можно использовать много раз набор текстов и систему мониторинга. Если сравнивать от формальных методов и статического анализа, позволяет найти временные и количественные характеристики программного обеспечения, например, реализация программы в целом и время выполнения ее отдельных участков, и сумма используемых ресурсов. Динамическое исследование кроме стандартных программных ошибок, дает найти те виды вирусов, которые появляются при запуске программы. Динамический анализ дает возможность найти уменьшение объёма свободной оперативной памяти и ошибки, которые появляются в многопоточных приложениях, например, таких как «состояние гонки» и виды ошибок, которые часто существуют в конечной реализации ПО, по-другому их называют плавающие ошибки, но их очень сложно найти на этапе конструировании, из-за того, что исчезают или меняют свойства при попытках обнаружения их. Продуктивность методов динамического анализа непосредственно зависит от качества и количества входных данных. Такие способы существуют в тех областях, где в основном критерием программного обеспечения является его время отклика, употребляемые ресурса надежность. Такие тесты это сервера с базами данных и системы реального времени. Это новая классификация и дает возможность на основе анализа имеющихся методов, создать рекомендации и требования, для реализации нового, синтетического метода верификации программного обеспечения. Синтетический метод осуществляет динамическую верификацию модели ПО, построенной на языке SMT-Lib, по промежуточному представлению кода программы.
Способы экспертизы невозможно автоматизировать, но при этом они имеют большее достоинство благодаря тому, что покрывают большую часть имеющих ошибок программы. Способы формальной верификации имеют отличительную особенность от других сложных процессов создания формальной модели программы, но при этом формальные методы покрывают огромный класс ошибок и легко автоматизируется. В настоящее время статические методы тестирование программного обеспечения лишены высокого полного тестирования, хотя прежде это было их привилегией, большинство программ употребляют динамический код, который нельзя верифицировать статическим методом. Динамические методы верифицируют только определенный набор трасс выполнения ПО и не гарантируют нужную полноту тестирования программы.
В итоге проведенного анализа и классификации имеющих методов, был создан список требований для нового, синтетического метода верификации.
На первых этапах разработки методы динамического анализа уместно употреблять на случаи если, есть какие-либо действующие элементы ПО. Динамические способы дают определить в программе только те ошибки, которые возникаютпри запуске программы. Для использования динамических способов верификации программного обеспечения также необходимо дополнительная подготовка, такие как: разработка тестов, создание тестовой системы, которая дает реализовать их.
Для применения динамических методов верификации ПО требуется дополнительная подготовка — создание тестов, разработка тестовой системы, позволяющие их выполнять или системы мониторинга, позволяющей проверить определенное поведение исследуемого ПО. Вероятно, динамическое генерирование тестов, похожее тестирование нуждается в большем времени. Одновременно является более продуктивным и новейшим методом тестирования, который может обнаружить значительное количество уязвимости в коде программы, нежели при применении статических методов тестирование программного обеспечения.
Метод динамического исследование также имеет недочеты, прежде всего недостатком этого метода является огромное количество ошибочных срабатываний. Величина ошибочных срабатывании при использовании новейших инструментов исследования порядочно велико и составляет, от 20 до 30 % [15-16, с. 514–518], все-таки динамический анализ — это порядочно эффективный метод для проверки программного обеспечения на присутствие уязвимости.
На основании рекомендованной классификации был образован синтетический метод верификации программного обеспечения на базе SMT — решателя, реализовывается разработка и верификация программы на языке SMT-lib, дающее возможность исправить не малое количество классов ошибок, в свою очередь позволяющее увеличить скорость и производительность анализа кода.
Литература:
1. Бурякова Н. А., Чернов А. В. Классификация частично формализованных и формальных моделей и методов верификации программного обеспечения // Инженерный Вестник Дона. 2014. № 4. 129–134 c.
2. Вельдер С. С., Шалыто А. А. Верификация простых автоматных программ на основе метода Модели тестирования // XV Международная научно-методическая конференция «Высокие интеллектуальные технологии и инновации в образовании и науке»: матер. СПб.: СПбГПУ, 2015. 285–288 c.
3. Гленфорд Майерс, Том Баджетт, Кори Сандлер.Искусство тестирования программ, 3-е издание– The Art of Software Testing, 3rd Edition. —М.:«Диалектика», 2012. — 272 с. —ISBN 978–5-8459–1796–6.
4. Глухих М. И., Ицыксон В. М., Цесько В. А. Использование зависимостей для повышения точности статического анализа программ // Моделирование и анализ информационных систем. 2011. № 4. 68–79 c.
5. Гурин Р. Е. Обзор и анализ инструментов, который осуществляют верификацию бинарного кода программы // Новые информационные технологии в автоматизированных системах: материалы 17-го научно-практического семинара. Вып. 17. М.: ИПМ им. М. В. Келдыша, 2014. 514–518. 421 с.
6. Калбертсон Роберт, Браун Крис, Кобб Гэри.Быстрое тестирование. —М.: «Вильямс», 2002. — 374 с. —ISBN 5–8459–0336-X.
7. Канер Кем, Фолк Джек, Нгуен Енг Кек.Тестирование программного обеспечения. Фундаментальные концепции менеджмента бизнес-приложений. — Киев: ДиаСофт, 2001. — 544 с. —ISBN 9667393879.
8. Карпов Ю. Г. MODEL CHECKING. Верификация параллельных и распределенных программных систем. СПб.: БХВ-Петербург, 2015. 560 с.
9. Кулямин В. В. Методы верификации программного обеспечения. 2008. 117 с. // Единое окно доступа к информационным ресурсам: интернет-портал. Режим доступа: http://window.edu.ru/resource/168/56168 (дата обращения 01.09.2015).
10. Лаврищева Е. М., Петрухин В. А. Методы и средства инженерии программного обеспечения: учебник. М.: МФТИ, 2009. 304 с.
11. Лифшиц Ю. Верификация программ и темпоральные логики. Лекция № 4 курса «Современные задачи теоретической информатики». СПб., ИТМО, 2005. 3–8 c.
12. Мандрыкин М. У., Мутилин В. С., Новиков Е. М., Хорошилов А. В. Обзор инструментов статической верификации С программ в применении к драйверам устройств операционной системы Linux // Сборник трудов Института системного программирования РАН. Т. 22. М.: ИСП РАН, 2012. C. 293–294. DOI: 10.15014/ISPRAS-2012–22–17. 345 c.
13. Рудаков И. В., Гурин Р. Е., Ребриков А. В. Верификация программного обеспечения: обзор методов и характеристик // Национальная ассоциация ученых (НАУ). Ежемесячный журнал. 2014. № 3, ч. 2. 22–26 c.
14. Beyer B. Status repоrt on software verification (competition summary SV-COMP 2014) // Tools and Algorithms for the Construction and Analysis of Systems / ed. by E. Abraham, 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.).377 c.
15. Boehmn B., Basilir V. Top 10 list [software development] // IEEE Computer. 2001. Vol. 34, no. 1. P. 135–137. DOI: 10.1109/2.962984. 136 c.
16. Boywer R. S., Elspaser 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, 1985. ACM New York, NY, USA, 1985. P. 234–254. DOI: 10.1145/800027.808445. 244 c.
