The 26 reference contexts in paper A. Rebrikov V., I. Rudakov V., R. Gurin E., А. Ребриков В., И. Рудаков В., Р. Гурин Е. (2016) “Методы верификации программного обеспечения // Methods of Software Verification” / spz:neicon:technomag:y:2015:i:0:p:235-251

  1. Start
    1930
    Prefix
    Методы верификации программного обеспечения предназначены для подтверждения фактов соответствия конечного программного продукта заявленным требованиям, целью верификации программного обеспечения является обнаружение ошибок, уязвимостей, некорректно реализованных свойств и требований
    Exact
    [1]
    Suffix
    . Проблема создания новой классификации методов верификации ПО является актуальной, так как позволяет рассмотреть существующие на данные момент методы верификации ПО и их программную реализацию, выявить их преимущества и недостатки.
    (check this in PDF content)

  2. Start
    2409
    Prefix
    Классификация и исследование существующих методовпозволяет составить список требований и рекомендаций для дальнейшей разработки и исследования синтетического метода верификации ПО, на основе SMT – решателя. Существующие методы верификации
    Exact
    [2]
    Suffix
    ПО можно разделить на эмпирические (использующие экспертизу), формальные (использующие математический аппарат для верификации программного обеспечения) и динамические (проверяющие работу программной реализации с помощью непосредственного запуска), а с точки зрения уровня автоматизации на ручные, автоматизированные и автоматические. 1.
    (check this in PDF content)

  3. Start
    3016
    Prefix
    Верификация программного обеспечения Одним из предназначений верификации ПО является проверка соответствия реализованного программного кода техническому заданию и требования к функциональности
    Exact
    [2]
    Suffix
    . Экспертиза используется для проверки документации и кода программного обеспечения на соответствие с нормами и стандартам оформлениями, которые приняты в стране, отрасли и организации. Экспертиза может быть общей и специализированной.
    (check this in PDF content)

  4. Start
    3301
    Prefix
    Экспертиза используется для проверки документации и кода программного обеспечения на соответствие с нормами и стандартам оформлениями, которые приняты в стране, отрасли и организации. Экспертиза может быть общей и специализированной. Термин верификации ПО в одной из нотаций
    Exact
    [3]
    Suffix
    означаетсимвольное выполнение программы или проверку кода на наличие ошибок и уязвимостей методами проверки модели. Методы формальной верификации позволяют провести верификацию программного обеспечения основываясь на математической модели программы без обращения к ее физической реализации.
    (check this in PDF content)

  5. Start
    3642
    Prefix
    Методы формальной верификации позволяют провести верификацию программного обеспечения основываясь на математической модели программы без обращения к ее физической реализации. Техника символьного выполнения
    Exact
    [4-5]
    Suffix
    широко используется в настоящее время для тестирования и анализа программ [5,6] и позволяет проводить моделирование выполнения программы, при котором часть входных переменных представляется в символьном виде.
    (check this in PDF content)

  6. Start
    3721
    Prefix
    Методы формальной верификации позволяют провести верификацию программного обеспечения основываясь на математической модели программы без обращения к ее физической реализации. Техника символьного выполнения [4-5]широко используется в настоящее время для тестирования и анализа программ
    Exact
    [5,6]
    Suffix
    и позволяет проводить моделирование выполнения программы, при котором часть входных переменных представляется в символьном виде. Символ переменной обозначает множество значений входной переменной программы из области ее определения.
    (check this in PDF content)

  7. Start
    7107
    Prefix
    Артефактом ПО – называется исследуемый участок кода программы;  Время выполнения – определяет время, которое требуется для верификации программы;  Способ достижения результата – определяет методы, и алгоритмы, с помощью которых инструменты анализа осуществляют верификацию ПО. Основными видами и характеристиками являются
    Exact
    [2]
    Suffix
    , устойчивость системы в случае недетерминированного поведения окружения, эффективность использования ресурсов времени и памяти, именно по этим параметрам, как правило, проводится верификация ПО.
    (check this in PDF content)

  8. Start
    7408
    Prefix
    Основными видами и характеристиками являются [2], устойчивость системы в случае недетерминированного поведения окружения, эффективность использования ресурсов времени и памяти, именно по этим параметрам, как правило, проводится верификация ПО. Одним из наиболее распространённых методом верификации ПО, является экспертиза
    Exact
    [2]
    Suffix
    . Под которой понимается исследование программного обеспечения, проводимое лицом (экспертом), сведущем в данной предметной области, эксперт может является, как и создателем программного продукта, так и лицом или группой лиц, привлеченным со стороны, для беспристрастной оценки характеристик программного продукта.
    (check this in PDF content)

  9. Start
    7858
    Prefix
    обеспечения, проводимое лицом (экспертом), сведущем в данной предметной области, эксперт может является, как и создателем программного продукта, так и лицом или группой лиц, привлеченным со стороны, для беспристрастной оценки характеристик программного продукта. Экспертиза может быть общей или специализированной, причем общую экспертизу можно разделить на следующие виды
    Exact
    [2]
    Suffix
    .  Техническая экспертиза. Определение пригодности программного продукта для использования его по назначению, соответствие его спецификации и стандартам;  Сквозной контроль. Анализ и оценка программы путем проверки артефакта, при помощи группы экспертов, участники команды последовательно представляют все характеристики программы, а эксперты анализируют ее и вносят замечания отмечая
    (check this in PDF content)

  10. Start
    8559
    Prefix
    Анализ, при котором поиск ошибок и уязвимостей осуществляется в соответствии с точным планом;  Аудит. Анализ программы, который выполняется людьми, не входящими в команду проекта. В свою очередь, специализированную экспертизу можно разделить на следующие виды
    Exact
    [2]
    Suffix
    :  Организационная экспертиза. Контроль руководством состояния проекта;  Экспертиза удобства использования. Контроль заказчиком и пользователем удобства использования разрабатываемого программного обеспечения;  Экспертиза защищенности.
    (check this in PDF content)

  11. Start
    9740
    Prefix
    Точность экспертизы напрямую зависит от квалификации и опыта специалистов, проводящих ее. Исследования показывают, что от 50 до 90% ошибок и уязвимостей выявляется с помощью метода экспертизы
    Exact
    [7]
    Suffix
    . Метод позволяет выявить практически любые виды ошибок и наиболее эффективен, в том случае если экспертизу проводят наиболее опытные и квалифицированные специалисты. Неоспоримым преимуществом, является применимость этого метода на любом этапе разработки проекта.
    (check this in PDF content)

  12. Start
    10580
    Prefix
    Формальные методыверификации подразумевают под собой, верификацию математической модели программы, а не ее исходный код. Требования к программной модели формулируются в виде спецификации. Проверяется выполнимость требований спецификации на модели программы.
    Exact
    [1]
    Suffix
    Формальные методы можно разделить в соответствии со следующими признаками [1]:  Дедуктивный анализ;  Проверка моделей;  Проверка согласованности;  Абстрактная интерпретация. По сравнения с экспертизой, явным преимуществом формальных методов является возможность автоматизации процесса верификации и построения моделей программ.
    (check this in PDF content)

  13. Start
    10657
    Prefix
    Требования к программной модели формулируются в виде спецификации. Проверяется выполнимость требований спецификации на модели программы. [1] Формальные методы можно разделить в соответствии со следующими признаками
    Exact
    [1]
    Suffix
    :  Дедуктивный анализ;  Проверка моделей;  Проверка согласованности;  Абстрактная интерпретация. По сравнения с экспертизой, явным преимуществом формальных методов является возможность автоматизации процесса верификации и построения моделей программ.
    (check this in PDF content)

  14. Start
    11227
    Prefix
    Формальные методы обладают высокой функциональной пригодностью, а также высокой точностью в том случае, если построена адекватная формальная модель. При помощи формальных методов можно выявить следующие классы ошибок
    Exact
    [8]
    Suffix
    :  Неопределенное поведения программы;  Неинициализированные переменные; обращение к NULL указателям;  Нарушение правил и алгоритмов пользования библиотекой;  Сценарии приводящие к недокументированному поведению программы;  Переполнение буфера.
    (check this in PDF content)

  15. Start
    12123
    Prefix
    ограниченный круг решаемых задач верификации ПО, а также то что не всегда можно построить наиболее полную и адекватную математическую модель, но при этом способны эффективно работать в промышленных проектах. Данный метод применим только к тем проверяемы участкам, которые можно учесть в формальной модели. Для построения математических моделей, обычно используется структура Крипке
    Exact
    [9]
    Suffix
    , адля спецификации программного обеспечения используют темпоральную логику [10], автоматическое доказательство теорем, использование мультимножеств и графов, модельные подходы (конечные автоматы, сети Петри, временные автоматы, логическое описание).
    (check this in PDF content)

  16. Start
    12209
    Prefix
    Данный метод применим только к тем проверяемы участкам, которые можно учесть в формальной модели. Для построения математических моделей, обычно используется структура Крипке [9], адля спецификации программного обеспечения используют темпоральную логику
    Exact
    [10]
    Suffix
    , автоматическое доказательство теорем, использование мультимножеств и графов, модельные подходы (конечные автоматы, сети Петри, временные автоматы, логическое описание). Главным достоинством метода проверки моделей, является возможность автоматизации процесса верификации и построения модели.
    (check this in PDF content)

  17. Start
    13424
    Prefix
    Этот термин обычно используется в случае, когда анализ производится с помощью автоматизированных инструментов. На данный момент наибольшее распространение получили две группы методов статической верификации: методы дедуктивного анализа программ и методы проверки моделей
    Exact
    [11]
    Suffix
    . Методы дедуктивного анализа используются для доказательства соответствия программы своей спецификации, обычно задаваемой в виде пред и постусловий. На текущем уровне развития эти инструменты не применимы для анализа больших программ, так как требуют ручной аннотации функций и циклов в тексте программы [13].
    (check this in PDF content)

  18. Start
    13759
    Prefix
    Методы дедуктивного анализа используются для доказательства соответствия программы своей спецификации, обычно задаваемой в виде пред и постусловий. На текущем уровне развития эти инструменты не применимы для анализа больших программ, так как требуют ручной аннотации функций и циклов в тексте программы
    Exact
    [13]
    Suffix
    . Методы проверки моделей (model checking) исходя из кода программы формируют её математическую модель, обычно в качестве модели используется модель Крипке [13], далее проводят анализ этой модели на предмет выполнения установленных условий и ограничений.
    (check this in PDF content)

  19. Start
    13918
    Prefix
    На текущем уровне развития эти инструменты не применимы для анализа больших программ, так как требуют ручной аннотации функций и циклов в тексте программы [13]. Методы проверки моделей (model checking) исходя из кода программы формируют её математическую модель, обычно в качестве модели используется модель Крипке
    Exact
    [13]
    Suffix
    , далее проводят анализ этой модели на предмет выполнения установленных условий и ограничений. При верификации методом проверки модели, анализируется не сама программа, а ее математическая модель, точность и полнота анализа зависит от того, на сколько адекватной является построенная математическая модель программы.
    (check this in PDF content)

  20. Start
    14404
    Prefix
    При верификации методом проверки модели, анализируется не сама программа, а ее математическая модель, точность и полнота анализа зависит от того, на сколько адекватной является построенная математическая модель программы. При статической верификации происходит разбор текста программы, в ее внутреннее представление, в результате которого строится граф потока управления
    Exact
    [11]
    Suffix
    . Генерация внутреннего представления программы происходит в процессе синтаксического анализа и позволяет сохранить ее исходную синтаксическую структур. Вершины графа соответствуют операторам, в тексте программы, а ребра ассоциируются с передачей потока управления.
    (check this in PDF content)

  21. Start
    15817
    Prefix
    Но при этом статический анализ слабо эффективен в диагностике ошибок, связанных с утечкой памяти, и имеет особенность генерировать большое количество ложных срабатываний помечая все подозрительные места в тексте программы. Тем не менее современные методы обладают высокой точностью и полнотой анализа
    Exact
    [14]
    Suffix
    . Данный метод позволяет определять такие ошибки как:  Неопределенное поведения программы – неинициализированные переменные;  Обращение к NULL указателям;  Нарушение правил и алгоритмов пользования библиотекой;  Сценарии, приводящие к недокументированному поведению программы;  Переполнение буфера;  Сценарии мешающие кросс – платформенности;  Ошибки, возникающие в повторяющемся коде
    (check this in PDF content)

  22. Start
    17225
    Prefix
    При использовании инструментов, которые не удовлетворяют этим характеристикам, анализ программы может быть не полным, при анализе может возникнуть большое количество “ложных срабатываний”. Одним из способов повысить точность и полноту анализа является использование механизма зависимостей
    Exact
    [12]
    Suffix
    . Зависимость представляет собой строго определенную связь между значениями двух и более переменных, которая может быть описана предикатом вида . Механизм зависимостей применим в случае, если текущее состояние программы объединяет два или более состояния, которые были получены на различных путях выполнения.
    (check this in PDF content)

  23. Start
    17664
    Prefix
    Механизм зависимостей применим в случае, если текущее состояние программы объединяет два или более состояния, которые были получены на различных путях выполнения. Зависимости способны связывать различные типы программных объектов
    Exact
    [12]
    Suffix
    . Зависимости можно разделить по характеру связи между программными объектами.  Арифметические зависимости  Зависимость эквивалентности  Логические зависимости  Зависимости сравнения Зависимости могут быть двух видов, присваивания и слияния.
    (check this in PDF content)

  24. Start
    18595
    Prefix
    Данный метод оперирует состоянием программы.Состояние программы представляет собой множество элементов абстрактного семантического домена, то есть множеством значений, которое может принимать переменная.
    Exact
    [13, 14]
    Suffix
    . При анализе программы происходит выявление зависимостей присваивания и слияния. Например, если и , то по окончании времени жизни строится зависимость [9- 10].
    (check this in PDF content)

  25. Start
    21608
    Prefix
    Динамический анализ можно разделить на несколько видов:  Тестирование  Мониторинг  Имитационное тестирование  Профилирование Мониторинг представляет собой метод, при котором идет наблюдение, регистрация и оценка работы программного обеспечения
    Exact
    [2]
    Suffix
    . Протоколируемая информация зависит от оцениваемых характеристик системы. Мониторинг может получать данные о работе, используя различные методы инструментированния. Инструментирование – это возможность отслеживания или установления количественных параметров уровня производительности программного продукта, а также возможность диагностировать ошибки и записывать информа
    (check this in PDF content)

  26. Start
    22488
    Prefix
     Инструментирование времени выполнения или инъекция времени выполнения (runtime instrumentation, runtime injection).  Симуляторный мониторинг (simulation-based, hypervisor-based) – осуществляет протоколирование работы проверяемого ПО симулятором, на котором выполняется
    Exact
    [1]
    Suffix
    . По способу получения характеристик ПО техники мониторинга могут быть разделены на следующие группы:  Основанные на событиях (используют для создания знаний полную запись событий и их сопутствующих атрибутов)  Статические (оценка системы на основе снимков ее состояния, которые получены через определенные промежутки времени) Наиболее эффективным и всеобъемлющим методом ди
    (check this in PDF content)