Методы анализа структуры программ относятся к доказательству правильности программ [6.20] и состоят в их инспекции независимыми экспертами с участием самих разработчиков. Они проверяют полноту, целостность, однозначность и непротиворечивость определений в программе. Сущность инспекции заключается в том, что эксперты пытаются взглянуть на программу «со стороны», подвергнуть ее всестороннему критическому анализу, рассмотреть словесные объяснения разработчиков о способах ее разработки. Цель инспекции — обнаружение ошибок в логике и в исходной программе в статике.
Сквозной контроль может сопровождаться ручной имитацией выполнения программы на выбранных тестах для получения результатов и сравнения их с ожидаемыми. Эти приемы позволяют обнаружить ошибки при многократном просмотре исходного кода, так они не формализованы, их проверка зависит от степени квалификации экспертов группы.
Метод простого структурного анализа ориентирован на анализ графовой структуры программы, в которой каждая вершина — оператор, а дуга — передача управления между операторами. На основе графа определяется достижимость вершин программы и существование выходов всех потоков управления для ее завершения.
Методы анализа данных
Для проведения анализа потоков данных граф расширяется специальными указателями переменных, их значениями и ссылками на каждый оператор программы.
При тестировании потоков данных сначала определяются значения предикатов в операторах реализации логических условий, по которым проходили пути выполнения программы. Затем проводится проверка вычислений на арифметических операциях. Для прослеживания путей программы устанавливаются точки, в которых имеются ссылки на переменные до присвоения им значений. Переменной присваивается значение без ее описания либо выполняется повторное описание переменной, к которой нет обращения.
Метод символьной проверки применяется при анализе логики программы и выявлении операторов, по которым не проходит путь вычислений, а также при обнаружении противоречий в описаниилогики программы. Этот метод называют методом анализа потоков управления в символьном виде. Результат проверки — значения переменных, полученных из выражений формул над входными потоками данных.
Метод задается следующими шагами:
1. построение тестового набора данных для заданного пути в виде последовательности операторов символьного выполнения. В случае невозможности построения такого набора делается заключение о нереализуемости (противоречивости) данного пути;
2. определение пути прохождения, при котором выполняются заданные ограничения на входные данные и символьные значения переменных.
Приведем шаги символьной проверки.
Шаг 1. Пусть — программа, выполняемая символически на наборах данных , где и — множество входных данных.
Пронумеруем операторы программы и обозначим состояние выполнения программы в виде тройки
где — номер текущего оператора программы , ( ) — условие выбора пути в программе (вначале ) в виде логического выражения над данными ; — множество пар , в которых — переменная программы, а — ее значение; — множество промежуточных и выходных данных.
Защита программ и данных: лекция 8 «Методы защиты программ от анализа»
Семантика символьного выполнения задается базовыми конструкциями ЯП и правилами оперирования символьными значениями, как алгебраическими вычислениями. К базовым конструкциям относятся операторы присваивания, перехода и условные операторы.
В операторе присваивания , , в выражение подставляются символьные значения переменных и , в результате чего получается выражение , которое становится значением переменной . Вхождение в полученное выражение переменных из означает, что их значения, а также значение не определены.
Оператор перехода — это ссылка к помеченной меткой оператора программы.
Согласно условного оператора «если то иначе » вычисляется выражение . Если оно определено и равно , то формируются логические формулы:
( 6.1)
( 6.2)
Если , то только одна из этих формул может быть выполнимой, а именно если
· формула (6.1) выполнима, то управление передается на оператор ;
· формула (6.2) выполнима, то управление передается на оператор ;
· (6.1), (6.2) не выполнимы (т.е. из не следует ни , ни ), тогда один набор данных, который удовлетворяет и соответствует части «то» условного оператора и имеется набор данных, соответствующий оператору после «иначе» этого условного оператора.
Таким образом, создаются два пути символьного выполнения в соответствии с формулами: и . Получаем, что , тогда когда
· для заданного пути формируется исходя из семантики условного оператора, преобразующего к виду (6.1) или (6.2);
· решаются системы уравнений (6.1) и (6.2) и если решения нет, то это означает невыполнимость пути.
Шаг 2. Определение пути при заданных ограничениях на входные данные проводится так:
· полагаем , где — входная спецификация, когда ее нет, то ;
· производим символьное выполнение операторов, если встречается ветвление, то запоминается состояние в данной точке или выбирается одна из ветвей; выполняется условный оператор, при котором формируется состояние программы с условием ;
· в конце пути прохождения по программе определяется функция и набор данных, которым удовлетворяет , покрывающий данный путь;
· для промежуточных выходной спецификации проводится доказательство выполнимости логических формул и , где — значение текущего условия в данной точке программы.
Доказательства этих формул можно провести верификацией данного участка пути. Выражение формулы декомпозируется на множество неравенств с целью определения несовместимости, мешающей прохождению по данному пути.
При проведении статического анализа программы используются различные инструменты, позволяющие определить ошибки в программе (например, неинициализированные или не использованные переменные). Кроме того, имеются способы автоматизации символьного выполнения программ и контроля в среде языковоориентированной разработки [6.23].
Не сдавайте скачаную работу преподавателю!
Методы и средства инженерии программного обеспечения — тест 6
nbsp
nbsp
Номер 2
Объединение — это:
nbsp
nbsp
nbsp
Номер 3
Количество компонентов произведения d находится следующим образом:
nbsp
nbsp
nbsp
Упражнение 4: Номер 1
Декларативные средства КЯ — это:
nbsp
nbsp
nbsp
Номер 2
Императивные средства КЯ — это:
nbsp
nbsp
nbsp
Номер 3
Концептор — это:
nbsp
nbsp
nbsp
Упражнение 5: Номер 1
Метод Флойда основан:
nbsp
nbsp
nbsp
Номер 2
Метод Маккарти основан:
nbsp
nbsp
nbsp
Номер 3
Метод Дейкстры основан:
nbsp
nbsp
nbsp
Упражнение 6: Номер 1
Валидация требований — это:
nbsp
nbsp
nbsp
Номер 2
Валидация требований включает следующие шаги:
nbsp
nbsp
nbsp
nbsp
Номер 3
Валидация требований не включает следующие шаги:
nbsp
nbsp
nbsp
nbsp
Упражнение 7: Номер 1
Методы анализа структуры программ проверяют:
nbsp
nbsp
nbsp
nbsp
Номер 2
Метод простого структурного анализа ориентирован на:
nbsp
nbsp
nbsp
Номер 3
Метод символьной проверки применяется при:
nbsp
nbsp
nbsp
Упражнение 8: Номер 1
Основные систематические методы обеспечения правильности программ — это:
nbsp
nbsp
nbsp
nbsp
Номер 2
Для доказательства правильности спецификации сообщения создается набор утверждений, доказывающий, что:
nbsp
nbsp
nbsp
Номер 3
Контекст — это:
nbsp
nbsp
nbsp
Упражнение 9: Номер 1
К событиям процесса относятся:
nbsp
nbsp
nbsp
nbsp
nbsp
Номер 2
К событиям процесса не относятся:
nbsp
nbsp
nbsp
Номер 3
Схема спецификации процесса — это:
nbsp
nbsp
nbsp
Упражнение 10: Номер 1
Каждый компонент C в ОКМ-модели задается в виде C = (E, I, V, P), где:
nbsp
nbsp
nbsp
Номер 2
Каждый компонент C в ОКМ-модели задается в виде C = (E, I, V, P), где:
nbsp
nbsp
nbsp
Номер 3
Каждый компонент C в ОКМ-модели задается в виде C = (E, I, V, P), где:
nbsp
nbsp
nbsp
Упражнение 11: Номер 1
При использовании модели проверки временных свойств и обнаружения ошибок взаимодействия должны выполняться следующие условия:
nbsp
nbsp
nbsp
nbsp
nbsp
Номер 2
Свойство компонента C включается в абстракцию P только тогда, когда:
nbsp
nbsp
nbsp
Номер 3
Модель ОКМ — это:
nbsp
nbsp
nbsp
Упражнение 12: Номер 1
Международный проект по разработке «целостного автоматизированного набора инструментов для проверки корректности ПС» включает следующие основные задачи:
nbsp
nbsp
nbsp
nbsp
Номер 2
Международный проект по разработке «целостного автоматизированного набора инструментов для проверки корректности ПС» предполагает, что:
nbsp
nbsp
nbsp
Номер 3
Функции репозитария не включают в себя:
nbsp
nbsp
nbsp
nbsp
Источник: eljob.ru
Методы анализа структур программ
Методы анализа структуры программ относятся к доказательству правильности программ [6.20] и состоят в их инспекции независимыми экспертами с участием самих разработчиков. Они проверяют полноту, целостность, однозначность и непротиворечивость определений в программе. Сущность инспекции заключается в том, что эксперты пытаются взглянуть на программу «со стороны», подвергнуть ее всестороннему критическому анализу, рассмотреть словесные объяснения разработчиков о способах ее разработки. Цель инспекции — обнаружение ошибок в логике и в исходной программе в статике.
Сквозной контроль может сопровождаться ручной имитацией выполнения программы на выбранных тестах для получения результатов и сравнения их с ожидаемыми. Эти приемы позволяют обнаружить ошибки при многократном просмотре исходного кода, так они не формализованы, их проверка зависит от степени квалификации экспертов группы.
Метод простого структурного анализа ориентирован на анализ графовой структуры программы, в которой каждая вершина — оператор, а дуга — передача управления между операторами. На основе графа определяется достижимость вершин программы и существование выходов всех потоков управления для ее завершения.
Для проведения анализа потоков данных граф расширяется специальными указателями переменных, их значениями и ссылками на каждый оператор программы.
При тестировании потоков данных сначала определяются значения предикатов в операторах реализации логических условий, по которым проходили пути выполнения программы. Затем проводится проверка вычислений на арифметических операциях. Для прослеживания путей программы устанавливаются точки, в которых имеются ссылки на переменные до присвоения им значений. Переменной присваивается значение без ее описания либо выполняется повторное описание переменной, к которой нет обращения.
Метод символьной проверки применяется при анализе логики программы и выявлении операторов, по которым не проходит путь вычислений, а также при обнаружении противоречий в описаниилогики программы. Этот метод называют методом анализа потоков управления в символьном виде. Результат проверки — значения переменных, полученных из выражений формул над входными потоками данных.
Метод задается следующими шагами:
1. построение тестового набора данных для заданного пути в виде последовательности операторов символьного выполнения. В случае невозможности построения такого набора делается заключение о нереализуемости (противоречивости) данного пути;
2. определение пути прохождения, при котором выполняются заданные ограничения на входные данные и символьные значения переменных.
Приведем шаги символьной проверки.
Шаг 1. Пусть 
— программа, выполняемая символически на наборах данных 
, где 
и 
— множество входных данных.
Пронумеруем операторы программы и обозначим состояние выполнения программы в виде тройки
где 
— номер текущего оператора программы 
, 
(
) — условие выбора пути в программе (вначале 
) в виде логического выражения над данными 
; 
— множество пар 
, в которых 
— переменная программы, а 
— ее значение; 
— множество промежуточных и выходных данных.
Семантика символьного выполнения задается базовыми конструкциями ЯП и правилами оперирования символьными значениями, как алгебраическими вычислениями. К базовым конструкциям относятся операторы присваивания, перехода и условные операторы.
В операторе присваивания 
, 
, 
в выражение 
подставляются символьные значения переменных 
и 
, в результате чего получается выражение 
, которое становится значением переменной 
. Вхождение в полученное выражение переменных из означает, что их значения, а также значение 
не определены.
Оператор перехода — это ссылка к помеченной меткой оператора программы.
Согласно условного оператора «если 
то 
иначе 
» вычисляется выражение . Если оно определено и равно 
, то формируются логические формулы:
 |
(6.1) |
 |
(6.2) |
Если , то только одна из этих формул может быть выполнимой, а именно если
· формула (6.1) выполнима, то управление передается на оператор ;
· формула (6.2) выполнима, то управление передается на оператор ;
· (6.1), (6.2) не выполнимы (т.е. из 
не следует ни , ни 
), тогда один набор данных, который удовлетворяет и соответствует части «то» условного оператора и имеется набор данных, соответствующий оператору после «иначе» этого условного оператора.
Таким образом, создаются два пути символьного выполнения в соответствии с формулами: 
и 
. Получаем, что 
, тогда когда
· для заданного пути формируется исходя из семантики условного оператора, преобразующего к виду (6.1) или (6.2);
· решаются системы уравнений (6.1) и (6.2) и если решения нет, то это означает невыполнимость пути.
Шаг 2. Определение пути при заданных ограничениях на входные данные проводится так:
· полагаем 
, где 
— входная спецификация, когда ее нет, то ;
· производим символьное выполнение операторов, если встречается ветвление, то запоминается состояние в данной точке или выбирается одна из ветвей; выполняется условный оператор, при котором формируется состояние программы с условием ;
· в конце пути прохождения по программе определяется функция и набор данных, которым удовлетворяет , покрывающий данный путь;
· для промежуточных 
выходной спецификации 
проводится доказательство выполнимости логических формул 
и 
, где — значение текущего условия в данной точке программы.
Доказательства этих формул можно провести верификацией данного участка пути. Выражение формулы декомпозируется на множество неравенств с целью определения несовместимости, мешающей прохождению по данному пути.
При проведении статического анализа программы используются различные инструменты, позволяющие определить ошибки в программе (например, неинициализированные или не использованные переменные). Кроме того, имеются способы автоматизации символьного выполнения программ и контроля в среде языковоориентированной разработки [6.23].
Источник: studopedia.org