Верификация программ методы верификации

Аннотация. В статье предлагается подход к построению расширяемой среды верификации программных систем, которая, по мнению автора, поможет решить проблемы практической применимости современных строгих методов верификации к практически значимым программам, сложность которых все время растет.

Она же может стать аналогом испытательного стенда для апробации и отладки большого числа новых предлагаемых техник формальных верификации и статического анализа на разнообразном промышленном программном обеспечении. 1. Введение 2. Синтетические методы верификации ПО 3. Подход к построению расширяемой среды верификации ПО 3.1. Анализ требований 3.2. Поддержка различных языков и нотаций 3.3. Архитектурная основа среды верификации 3.4. Организация разработки среды верификации 4. Заключение Литература

1. Введение

Прогресс технологий разработки программного обеспечения (ПО) в последние десятилетия значительно увеличил производительность программистов в терминах количества кода, создаваемого ими в единицу времени. Это проявляется, в частности, в увеличении размеров наиболее сложных программных систем, разрабатываемых сейчас, до десятков миллионов строк кода [1, 2]. Однако качество программ при этом заметным образом не изменилось — среднее количество ошибок на тысячу строк кода, еще не прошедшего тестирование, по-прежнему колеблется в пределах 10-50 [3]. Таким образом, совершенствование методов разработки ПО, давая возможность создавать все более сложные системы, необходимые современной экономике, науке и государственным организациям, парадоксальным образом лишь увеличивает количество дефектов в них и связанные с этим риски.

Занятие 20 (2022-23): Верификация цифровых устройств. История методов верификации.

Борьба с дефектами и ошибками в программном обеспечении ведется при помощи его верификации. В ходе ее выполнения проверяется взаимная согласованность всех артефактов разработки — проектной и пользовательской документации, исходного кода, конфигураций развертывания, — а также их соответствие требованиям к данной системе и нормам применимых к ней стандартов. Методы верификации ПО также активно развиваются, однако их прогресс менее заметен. Поэтому предельная сложность ПО, которое можно сделать надежно и корректно работающим, существенно меньше сложности систем, востребованных современным обществом.

Различные методы проведения верификации ПО можно (больше по историческим, чем содержательным причинам) разделить [4] на формальные методы, использующие строгий анализ математических моделей проверяемых артефактов и требуемых свойств; методы статического анализа, в ходе которых возможные ошибки ищутся без исполнения проверяемого ПО; методы динамического анализа, проводящие проверку реального поведения проверяемой системы в рамках некоторых сценариев ее работы; и экспертизу (review, inspection), выполняемую людьми на основе их знаний и опыта.

Все эти методы имеют разные достоинства и недостатки, различные области применимости, и эффективность их применения сильно отличается в разных контекстах. Но полноценная верификация крупномасштабных сложных систем невозможна без совместного использования всех этих методов, поскольку только их сочетание позволяет преодолеть недостатки каждого. При этом на каждом уровне рассмотрения системы и для каждого вида компонентов хотелось бы выбирать самый эффективный метод, дающий наиболее достоверный вклад в оценку качества системы в целом и требующий минимальных затрат. К сожалению, пока не существует общего подхода, позволяющего сопоставлять и сравнивать различные методы верификации и их сочетания в различных контекстах при применении к реальным программным системам.

Podlodka #268 – Формальные методы и верификация программ

Чтобы справиться со все возрастающей сложностью реальных систем, исследователями за последние 20-30 лет создано огромное количество разнообразных методов и техник верификации [4], особенно в рамках статического анализа и формальных методов. Но для их эффективного использования чаще всего нужно быть специалистом в соответствующей области. Многие из таких работ ограничиваются формулировкой идей и алгоритмов, несколько реже создаются прототипные реализации, цель которых — на двух-трех примерах продемонстрировать, что предложенная техника работает. Эти прототипы невозможно использовать для индустриальной разработки ПО, в рамках которой инструменты должны быть работоспособны и эффективны в очень широком контексте. У исследователей же почти никогда нет ресурсов и времени разрабатывать промышленно применимые инструменты.

В тех очень редких случаях, когда удается все же сделать пригодный к использованию на практике инструмент, он объединяет десяток-два разнообразных техник и способен решать две-три задачи верификации. Однако в процессе промышленной разработки ПО таких задач несколько десятков, а большинству организаций удается успешно внедрить и начать активно использовать лишь два-три таких инструмента.

Другой проблемой является растущая сложность создания и апробации новых техник верификации. Все необходимое для их работы окружение — инструменты анализа исходного кода, описания формальных моделей, библиотеки для работы с внутренним представлением моделей и кода, инструменты, реализующие различные виды анализа кода и моделей, средства получения отчетов — невозможно разработать заново.

Исследователю для проверки работоспособности его идеи приходится на скорую руку собирать это окружение из разнородных компонентов и библиотек, которые можно найти в свободном доступе. В лучшем случае удается создать прототип, который способен справиться с парой нужных примеров. Но таким способом невозможно создать среду, в рамках которой можно было бы проанализировать работоспособность и эффективность новой идеи в широком множестве разнообразных ситуаций, на разных видах приложений и требований к ним. Поэтому большинство новых идей применяются лишь в «тепличных условиях», а эффекты от их применения в широком контексте остаются неясными и непредсказуемыми.

Решением для упомянутых проблем могла бы стать унифицированная расширяемая среда верификации программных систем, предоставляющая общее окружение для решения задач верификации и библиотеки готовых компонентов, реализующих типовые техники. Такая среда могла бы существенно упростить интеграцию модулей, реализующих различные техники верификации, за счет унифицированных интерфейсов ее расширения.

Исследователи могли бы использовать ее для значительного снижения затрат на апробацию новых методов и анализ их работоспособности в разнообразных ситуациях. Промышленные разработчики — для интеграции нужного им набора техник в рамках единого инструмента и эффективного внедрения их в практическое использование.

Подтверждением работоспособности и эффективности интеграции различных методов верификации ПО в разнообразных ситуациях являются многочисленные синтетические методы верификации.

2. Синтетические методы верификации ПО

Синтетические методы верификации используют техники различных видов по приведенной выше классификации, а также комбинируют идеи различных подходов для получения большей эффективности верификации в терминах затрат на ее проведение и достоверности получаемых результатов.

• Расширенный статический анализ (extended static checking) [5, 6] проверяет соответствие кода ПО требованиям, обычно записываемым тоже в коде в виде комментариев к его отдельным элементам (процедурам, типам данных и методам классов). При этом на основе результатов анализа кода автоматически строятся формальные модели его поведения, выполнение требований для которых проверяется чаще всего с помощью дедуктивного анализа и специализированных решателей (solvers).
• Статический анализ на базе автоматической абстракции [7-10]. В рамках такого подхода на основе результатов статического анализа кода автоматически строятся более абстрактные, а потому более простые модели работы проверяемого ПО, которые затем подвергаются проверке на выполнение определенных свойств с помощью инструментов проверки моделей или решателей. Обычно проверяемые свойства фиксированы для данного инструмента или формулируются в конфигурационном файле. При нарушении требования в модели инструменты этого типа пытаются построить соответствующий сценарий работы кода. Если это не получается из-за упрощений, сделанных при построении модели, определяются элементы кода, препятствующие выполнению такого сценария, и в модель вносятся уточнения, более аккуратно описывающие работу именно этих элементов, после уточненная модель снова проверяется на выполнение заданного свойства. В итоге инструмент либо подтверждает выполнение требований, либо находит контрпример, либо завершает работу по истечении некоторого времени или из-за исчерпания ресурсов, не приходя к определенным выводам.

• Построение тестов с помощью разрешения ограничений [20-22]. Часто при разработке тестов на основе критериев полноты тестирования формулируются так называемые цели тестирования (test objectives), представляющие собой специфические ситуации, в которых необходимо проверить поведение тестируемой системы для достижения необходимой уверенности в ее корректной работе. Цель тестирования формулируется как набор ограничений на проходимые во время теста состояния системы и данные выполняемых воздействий. Для построения теста, достигающего такую цель, можно использовать специализированные решатели (solvers). Такой решатель либо автоматически находит необходимые данные и последовательность вызовов операций как решение заданной системы ограничений, либо показывает, что эта система неразрешима, т.е. заданная цель тестирования недостижима и строить нацеленные на нее тесты не имеет смысла.
• Построение тестов как контрпримеров с помощью инструментов проверки моделей [23-26]. Другой способ построения тестов — сформулировать отрицание ограничений, задающих цель тестирования, как свойство, которое можно проверить или опровергнуть с помощью инструмента проверки моделей. Если это свойство подтверждается, значит, цель тестирования недостижима, если же оно опровергается, то инструмент строит контрпример, являющийся в данном случае необходимым тестом.

• Многочисленные проекты NASA по разработке ПО управления для космических спутников, челноков и специализированных исследовательских аппаратов, проводимые с использованием инструментов проверки моделей, генерации тестов на их основе и мониторинга [31-33]. Из используемых в этих проектах инструментах наиболее известны инструменты проверки моделей Spin [34, 35], генератор тестов T-VEC [36, 37] и инструмент символического выполнения Java PathFinder [38, 39], используемый для проверки свойств Java программ, их мониторинга и тестирования.
• Создание и использование в Microsoft инструмента Static Driver Verifier, использующего статический анализ с автоматической абстракций для проверки корректности работы драйверов Windows [40]. Сначала в проекте использовался инструмент проверки моделей SLAM, который затем был значительно доработан и дополнен возможностями анализа произвольного кода на языке C и автоматической абстракции, направляемой контрпримерами [41, 42].
• Внутренний проект Microsoft по проведению формальной спецификации и генерации тестовых наборов для разнообразных клиент-серверных протоколов, используемых в продуктах этой компании [43]. В рамках этого проекта используется, в основном, инструмент SpecExplorer [44], разработанный в Microsoft Research, а объем работ по анализу и формализации документации на протоколы оценивается в несколько десятков человеко-лет.
• Проводившиеся и идущие в настоящее время в ИСП РАН проекты по созданию тестов на основе формальных моделей базовых библиотек операционных систем, телекоммуникационных протоколов семейства IPv6, оптимизирующих блоков компиляторов [45-47], использующие семейство инструментов тестирования на основе моделей UniTESK [48].
• Использование формальных методов верификации и инструментов расширенного статического анализа при создании систем авионики в Airbus и Boeing [10, 49, 50]. В частности, в Airbus использовался инструмент статического анализа на основе формальных моделей ASTREE [10].
• Использование формальных методов, тестирования на основе моделей и средств мониторинга при разработке ПО для смарт-карт [51, 52].

Все эти примеры подтверждают эффективность интеграции различных вери-фикационных методов на практике. Тем не менее, несмотря на достигнутые успехи, каждый из имеющихся синтетических подходов использует лишь часть имеющегося потенциала и не предоставляет единой среды интеграции для всего многообразия различных техник верификации ПО.

Источник: citforum.ru

Методы верификации программного обеспечения

Егоров, В. В. Методы верификации программного обеспечения / В. В. Егоров, Н. И. Томилова, А. Ж. Амиров, К. Н. Касылкасова. — Текст : непосредственный // Молодой ученый. — 2016. — № 21 (125). — С. 138-141. — URL: https://moluch.ru/archive/125/34536/ (дата обращения: 10.07.2023).

В статье идет речьобисследовании и классификации методов верификации программного обеспечения (ПО). Осуществлен обзор имеющихся статических методов верификации, исследованы характеристики методов и осуществлено исследование на обнаружение зависимостей в рамках метода абстрактной интерпретации. В статье показан обзор и классификация динамических методов верификации ПО.

Классификация выполнена по ряду главных критериев, таких как: вид метода, уровень автоматизации, уровень функциональной применимости, точность, типы обнаруживаемых ошибок, эффективность, область соответствия метода, время выполнения и способ достижения результата. Выполнен обзор видов тестирования и средств логического вывода и рассмотрены основные особенности методов верификации. Обнаружены недостатки имеющихся способов верификации программ.

Ключевые слова:верификация, статический анализ, динамический анализ, интерпретация, символьное выполнение, проверка модели

Одна из главных проблем при разработке программного обеспечения является верификация программного обеспечения. Средства верификации программного обеспечения создаются специально для подтверждения требованиям заявленного конечного программного продукта, сама цель верификации программного обеспечения является обнаружение ошибок, некорректных свойств и уязвимость программы [1, с. 129–134]. Актуальной проблемой является формирование новой классификации способов верификациипрограммного обеспечения, и дает возможность рассмотреть существующие в настоящее время методы верификации ПО, обнаружить их преимущество и недостатки. Классификация и анализ существующих способов дает создать список требований и рекомендаций для будущего исследования и разработкисинтетического метода верификации программного обеспечения, по принципу SMT — решателя.

Современные способы верификации можно поделить на эмпирические (те, которые используют экспертизу), формальные (которые используют математический аппарат верификации ПО) и формальные (которые проверяют работу программу с помощью запуска), уровни автоматизации делятся на ручные, автоматические и автоматизированные.

Одна из главных целей верификации программного обеспечения является проверка созданного программного кода техническому заданию и ее требования функциональности [2, с. 285–288].

Проверки документации и кода программного обеспечения с нормами и стандартам проведение оформлениями использует экспертиза, которые установлены в стране, отрасли и организации. Сама экспертиза может быть специализированной и общей.

Понятие верификации программного обеспечения в одной из нотаций [3, с. 272] обозначает символьное выполнение программы или проверку кода на наличие ошибок и уязвимости способов проверки модели.

Широко используется в настоящее время техника символьного выполнения [4–5, с. 68–79, 374], что позволяет проводить моделирование выполнения программы, при этом часть переменных представляются в символьном виде. Символ переменной показывает, что большинство значении входной переменны программы из области ее определения. Каждое символьное выполнение равноценно выполнению ПО, в наборе конкретных текстовых значении переменных, котороесокращает мощность множества изобретаемых тестов. Тоже самое означает альтернативная семантика исполнения программы — семантика условного выполнение для языка программирования, в котором объекты данных представлены в виде символов. Для работы с символьными значениями для этого семантика показывает пути расширения основных конструкции языков программирования.

Главные этапы верификации программного обеспечения — это тестирование программ на пригодность провозглашенным качественным характеристикам. Самые важные характеристики ПО перечислены ниже:

1. Корректность (аналогично системе своего назначение);
2. Безопасность системы;
3. Устойчивость системы в случае недетерминированного поведения окружения (например, неправильные входные данные);
4. Эффективность использования ресурсов времени и памяти;
5. Адаптируемость системы к небольшим преобразованиям окружения;
6. Переносимость и совместимость.

Экспертиза является самым популярным методом тестирование программ [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.

Основные термины (генерируются автоматически): программное обеспечение, статический анализ, динамический анализ, SMT, код программы, ошибка, исходный код, символьное выполнение, синтетический метод верификации, тестирование программ.

Источник: moluch.ru

Верификация и валидация ПО: технологии и инструменты

Сейчас как никогда актуальна проблема обеспечения качества ПО: даже единичный отказ может привести к ликвидации компании или человеческим жертвам. Как обеспечить качество ПО и постоянно поддерживать его на требуемом уровне?

16.05.2019 Моисес Родригес, Марио Пьяттини, Кристофер Эберт

• Ключевые слова / keywords:
• валидация
• validation
• Верификация
• Надежность и отказоустойчивость
• Reliability and fault tolerance
• Программная инженерия
• Средства тестирования программ

Сейчас как никогда актуальна задача обеспечения качества ПО, для решения которой сегодня предлагается множество инструментов верификации и валидации кода. При этом важно не только внедрить сами инструменты, развивать соответствующие компетенции и выстроить стратегию тестирования. Для устранения рисков, связанных с человеческим фактором, нужны развитые возможности автоматического обнаружения критических точек и дефектов.

Программное обеспечение лежит в основе почти любой инфраструктуры, и задача обеспечения его качества сегодня актуальна как никогда. Практически все компании уже используют в своей деятельности Интернет вещей, бизнес-аналитику, искусственный интеллект, облака, социальные сети и т. п. Традиционные ИТ и встроенные системы уступают место повсеместному ПО, а успех цифровой трансформации предприятий зависит от работы программных систем, отвечающих всем отраслевым требованиям к надежности и доступности сервисов.

Сегодня организации вкладывают около 30% бюджета, выделяемого на ИТ, в обеспечение качества и тестирование, что неудивительно — более половины всех систем являются критически важными для бизнеса [1]. При этом компаниям и организациям необходимо максимально гибко реагировать на изменения и внедрять формализованные процессы и методы контролируемого выпуска безопасного ПО. Активно внедряются механизмы автоматического обновления ПО по Сети, методы DevOps и «непрерывная инженерия» (continuous software engineering) [2], что повышает потребность в процессах непрерывной верификации и валидации, требующих намного более тщательного, чем еще совсем недавно, выполнения процедур испытания на общую работоспособность.

Методы Agile и непрерывной разработки ПО, направленные на повышение качества и удовлетворение требований пользователей, должны опираться на эффективные, удобные в применении инструменты, которые могут войти в арсенал как разработчиков ПО, так и пользователей. Кроме того, оценка качества может проводиться третьей стороной — аккредитованной лабораторией или сертификационным центром.

Выбор методов верификации и валидации ПО зависит от модели разработки (V-модель, каскадная, спиральная и т. д.) и стандарта (ISO/IEC 25000 SQUARE, ISO/IEC 12207:2017) (рис. 1).

Рис. 1. Стандарты обеспечения качества процесса разработки ПО и конечного продукта

За качество собственно процесса разработки ПО отвечают стандарт ISO/МЭК 12207, регламентирующий процессы верификации и валидации, а также V-модель, в рамках которой каждой задаче разработки ставится в соответствие процесс тестирования. Например, модульный тест проверяет соответствие исходного кода низкоуровневой архитектуре, интеграционные тесты проверяют совместимость (интеграцию) ранее протестированных компонентов, системные тесты позволяют выяснить, соответствует ли полностью интегрированный продукт спецификациям, а приемочные тесты — отвечает ли продукт ожиданиям пользователя.

В стандартах серии ISO 25000, относящихся к качеству программного продукта, выделены следующие характеристики ПО:

• функциональная пригодность — степень соответствия продукта или системы заявленным функциям, объявленным и подразумеваемым потребностям при эксплуатации ПО в указанных условиях;
• сопровождаемость — удобство и гибкость модификации продукта или системы, ее корректировки или адаптации к изменениям среды или требований;
• удобство использования — простота работы с продуктом или системой для эффективного достижения пользователями указанных целей в заданном контексте применения;
• безопасность — степень, до которой продукт или система защищают данные при условии, что люди либо системы имеют доступ к данным в соответствии со своими привилегиями;
• относительная производительность — соотношение производительности и объема использованных ресурсов при заданных условиях.

На рис. 2 изображены элементы обеспечения качества процессов и продуктов и соответствующие инструменты. Данная схема может помочь в выборе средств верификации и валидации, которые можно задействовать на каждом из этапов V-модели и для каждого параметра качества ПО.

Рис. 2. Инструменты для проверки основных характеристик качества ПО

На этапе написания кода чаще применяются средства статического анализа, позволяющие непосредственно в интегрированной среде разработки контролировать соответствие кода стандартам. В то же время в рамках статического анализа проверяются особенности структуры модулей и архитектуры ПО, поэтому на рис. 2 поле средств статического анализа размещено на одном уровне с написанием кода, но захватывает тесты, касающиеся верификации архитектуры. Средства статического анализа имеют отношение ко всем четырем характеристикам качества.

Технологии и инструменты

Средства XUnit применяются для проверки правильности работы каждого разработанного модуля, при этом необходимо обеспечить максимальное покрытие кода. Фреймворки XUnit получили наиболее широкое распространение среди технологий автоматизации тестирования, позволяя на специальных языках описывать тестовые ситуации и автоматически их выполнять.

Средства комбинаторного тестирования генерируют тестовые данные, что дает возможность проверять корректность функционирования различных интегрированных модулей.

Инструменты фиксации и замены используются для проверки корректности и полноты функционирования системы, в том числе при проведении приемочных тестов. Эти средства регистрируют взаимодействия тестировщиков с приложением, генерируя тестовые сценарии, которые затем можно выполнять автоматически.

Инструментов тестирования так же много, как и языков программирования. В табл. 1 приведены основные средства тестирования для первой десятки наиболее популярных языков программирования (согласно рейтингу Tiobe).

Инструменты контроля сопровож-даемости. Позволяют анализировать исходный код и проверять его на соответствие правилам модульности, читаемости и др. (табл. 2).

Инструменты контроля удобства использования. Применяются для оценки программного продукта в процессе работы с ним реальных пользователей. В то же время такие инструменты позволяют проводить валидацию пользовательского интерфейса без участия самих пользователей (табл. 3).

Средства контроля безопасности. Позволяют обнаруживать уязвимости в системе и определять, защищает ли она данные при сохранении необходимой функциональности. В частности, средства испытания на защиту от проникновения имитируют атаки на программную систему или сеть с помощью сканирования и других действий, направленных на поиск и использование слабых мест. Их также называют инструментами этичного, или белого, хакерства (табл. 4).

Средства проверки производительности. Позволяют выяснить, насколько быстро система работает под нагрузкой (табл. 5). Эти средства не предназначены для поиска дефектов в приложении, а применяются для оценки измеримых характеристик: времени отклика, пропускной способности и т. д.

Средства непрерывной верификации и валидации. Принцип непрерывного обеспечения качества предполагает тесную интеграцию процессов верификации и валидации на всех этапах разработки. Типичный пример — разработка с ориентацией на тестирование: плановые показатели качества задаются еще до разработки ПО.

С учетом преимуществ непрерывной интеграции, одной из основ DevOps, все большее значение придается инструментам, помогающим не только автоматизировать верификацию и валидацию, но и интегрировать эти процессы в цикл разработки. Перечисленные в табл.

6 инструменты позволяют проверять характеристики качества в рамках сред непрерывной интеграции Jenkins, Travis CI, Bamboo, GoCD, Ansible и т. п. Требуется встроить валидацию и верификацию в жизненный цикл ПО, обеспечив автоматическое, прозрачное для разработчиков выполнение соответствующих процессов. Представленные в табл. 6 инструменты проверяют несколько характеристик качества и позволяют получить данные для глобальной оценки и визуализации. В рамках процессов непрерывной верификации и валидации также могут применяться инструменты модульного тестирования, фиксации и замены и статического анализа.

Для управления действиями, выполняемыми при помощи всех перечисленных видов инструментов, и контроля над процессом верификации и валидации в целом, применяются средства управления тестовыми случаями: Test Link, Test Rail, Microfocus Quality Center, VSTS, IBM Rational Quality Manager, XStudio и др.

Перспективы

Современное общество все сильнее зависит от программного обеспечения, которое становится двигателем всех отраслей экономики, в связи с чем растут и требования к качеству ПО. Применение методов и технологий автоматизации соответствующих процессов становится обязательным элементом защиты инфраструктур.

В современном мире становится все больше рисков, связанных с ростом количества угроз кибербезопасности и проблемами, обусловленными неудобством использования приложений. Это означает, что нужно ускорить развитие технологий верификации и валидации, а также удвоить усилия, направленные на повышение надежности систем. В частности, необходимы сценарии мягкой деградации возможностей ПО и его работы в условиях отказа.

Избежать обнаружения злоумышленниками критических уязвимостей и появления новых атак после выпуска продукта помогут непрерывная верификация и валидация, которые должны стать основой стратегии обеспечения качества ПО. Необходима возможность гибко вносить исправления и изменения с использованием беспроводных сетевых соединений. Понадобятся механизмы, препятствующие запуску систем в случае, если на них не установлены самые свежие обновления программного обеспечения. В число таких систем входят автомобили, производственные линии и иное оборудование, требующее особо высокого уровня безопасности. Еще в большей степени это касается медицинской техники — для нее нужна иерархическая система контроля качества.

Выбор систем верификации и валидации определяется многими факторами. В зависимости от применяемой среды разработки, в разных организациях соответствующие процессы имеют свои особенности и строятся на базе различных сочетаний инструментов. При этом важно не только внедрить сами инструменты, развивать соответствующие компетенции и выстроить стратегию тестирования. Для устранения рисков, связанных с человеческим фактором, нужны развитые возможности автоматического обнаружения критических точек и дефектов.

С внедрением технологий искусственного интеллекта появляется потребность в обеспечении прозрачности работы соответствующих систем — необходимо понимание того, по каким правилам нейронная сеть определяет, можно ли предоставить клиенту кредит или как автомобиль-робот отреагирует на стечение нескольких опасных обстоятельств. Классические регрессионные тесты и средства отслеживания в подобных случаях не помогут. В средствах верификации и валидации новых поколений будет все больше интеллектуальных механизмов на основе больших данных, способных к анализу, самообучению и автоматическому улучшению качества ПО.

Аристотель говорил: «Совершенство — это не действие, а привычка». Широкий выбор инструментов — это важно, но главное — создание культуры обеспечения качества ПО и приобретение соответствующих навыков.

1. Capgemini. MicroFocus, and Sogeti. World quality report. 2018. [Online]. URL: https:// www.capgemini.com/service/world-quality-report-2018-19/ (дата обращения: 16.05.2019).

2. B. Fitzgerald, K. Stol. Continuous software engineering: A roadmap and agenda // J. Syst. Softw.— 2017 (Jan). — Vol. 123. — P. 176–189.

Moises Rodriguez, Mario Piattini, Christof Ebert, Software Verification and Validation Technologies and Tools. IEEE Software, March/April 2019, IEEE Computer Society. All rights reserved. Reprinted with permission.

Верификация,валидация,средства тестирования программ,надежность и отказоустойчивость,verification, validation, software testing tools, reliability and fault tolerance

Источник: www.osp.ru