Методы анализа структур программ - Лекция, раздел Философия, Конспект лекций по дисциплине Надежность систем В данной лекции систематически изложены следующие взаимосвязанные аспекты инженерии ПО Методы Анализа Структуры Программ Относятся К Доказательству Правильности Про...
Методы анализа структуры программ относятся к доказательству правильности программ [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].
Тема... В данной лекции систематически изложены следующие взаимосвязанные аспекты... теоретический и интеллектуальный базис методы принципы средства и методологии и др проектирования...
Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ:
Методы анализа структур программ
Что будем делать с полученным материалом:
Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:
Анализ и характеристика областей знаний SWEBOK
Ядро знаний SWEBOK является основополагающим научно-техническим документом, который отображает мнение многих зарубежных и отечественных специалистов в области программной инженерии [1.3-1.12
Требования к ПО (Software Requirements)
Требования - это свойства, которыми должно обладать ПО для адекватного определения функций, условий и ограничений выполнения ПО, а также объемов данных, технического обеспечения и среды функциониро
Проектирование ПО (Software design)
Проектирование ПО - это процесс определения архитектуры, компонентов, интерфейсов, других характеристик системы и конечного состава программного продукта. Область знаний "Прое
Конструирование ПО (Software Construction)
Конструирование ПО - создание работающего ПО с привлечением методов верификации, кодирования и тестирования компонентов. К инструментам конструирования ПО отнесены языки программирования и конструи
Тестирование ПО (Software Testing)
Тестирование ПО - это процесс проверки готовой программы в статике (просмотры, инспекции, отладки исходного кода) и в динамике путем прогона конечного набора тестовых данных, проверяющих разные пут
Сопровождение ПО (Software maintenance)
Сопровождение ПО - совокупность действий по обеспечению работы ПО, а также по внесению изменений в случае обнаружения ошибок в процессе эксплуатации, по адаптации ПО к новой среде функционирования,
Управление конфигурацией ПО
Управление конфигурацией (Software Configuration Management - SCM) состоит в идентификации компонентов системы, определении функциональных и физических характеристик аппаратного и программно
Управление инженерией ПО
Управление инженерией ПО (Software Engineering Management) - руководство работами команды разработчиков ПО в процессе выполнения плана проекта, определение критериев эффективности работы ком
Процесс инженерии ПО (Software Engineering Process)
В некотором смысле это метауровень, который связан с определением, реализацией, оценкой, измерением, управлением изменениями и совершенствованием самого процесса. Однако такой процесс не явл
Методы и инструменты инженерии ПО
Методы обеспечивают проектирование, реализацию и выполнение ПО. Они накладывают некоторые ограничения на инженерию ПО в связи с особенностями применения их нотаций и процедур, а также обеспечивают
Качество ПО (Software Quality)
Качество ПО - набор свойств продукта (сервис или службы), которые характеризуют его способность удовлетворить установленные или предполагаемые потребности заказчика. Понятие качества имеет разные и
Жизненный цикл ПС, связь с ядром знаний SWEBOK
Программная инженерия, как инженерная дисциплина, охватывает все аспекты создания ПС от начальной стадии разработки системных требований до реализации программного продукта и его использован
Каскадная модель ЖЦ
Одной из первых стала применяться каскадная модель, в которой каждая работа выполняется один раз и в том порядке, как это представлено в модели (рис. 2.4).
Инкрементная модель ЖЦ
Первая создаваемая промежуточная версия системы (выпуск 1) реализует часть требований, в последующую версию (выпуск 2) добавляют дополнительные требования и так до тех пор, пока не будут окончатель
Спиральная модель
увеличить изображение Рис. 2.6.Спиральная модель ЖЦ р
Эволюционная модель ЖЦ
В случае эволюционной модели система разрабатывается в виде последовательности блоков структур (конструкций). В отличие от инкрементной модели ЖЦ подразумевается, что требования устанавливаются час
Стандартизация модели ЖЦ
Типичный ЖЦ системы начинается с формулировки идеи или потребности, проходит все процессы разработки, производства, эксплуатации и сопровождения системы. Стандартный ЖЦ состоит из процессов, каждый
Характеристика областей знаний SWEBOK
В ядре знаний SWEBOK определено 10 областей знаний. Среди них выделим базовые области, методы и средства которых соответствуют процессам разработки ПС:
1. Разработка требований;
2
Процессы ЖЦ верификация и валидация программ
Верификация и валидация, как методы, обеспечивают соответственно проверку и анализ правильности выполнения заданных функций и соответствия ПО требованиям заказчика, а та
Тестирование программ
Тестированиеможно рассматривать, как процесс семантической отладки (проверки) программы, заключающийся в исполнении последовательности различных наборов контрольных тестов, для кот
Статические методы тестирования
Статические методы используются при проведении инспекций и рассмотрении спецификаций компонентов без их выполнения.Техника статического анализа заключается в методическом просмотре (или обзоре) и а
Динамические методы тестирования
Динамические методы тестирования используются в процессе выполнения программ. Они базируются на графе, связывающем причины ошибок с ожидаемыми реакциями на эти ошибки. В процессе тестирования накап
Функциональное тестирование
Цель функционального тестирования - обнаружение несоответствий между реальным поведением реализованных функций и ожидаемым поведением в соответствии со спецификацией и исходными требованиями
Инфраструктура процесса тестирования ПС
Под инфраструктурой процесса тестирования понимается:
· выделение объектов тестирования;
· проведение классификации ошибок для рассматриваемого класса тестируемых программ;
Методы поиска ошибок в программах
Международный стандарт ANSI/IEEE-729-83 разделяет все ошибки в разработке программ на следующие типы.
Ошибка (error) - состояние программы, при котором выдаются неправильные результаты, пр
Служба тестирования ПС
За функциональные и исполнительные тесты несут ответственность разработчики заказчик, он больше влияет на составление тестов испытаний и инсталляции системы [7.6].
Для этих целей, как прав
Управление процессом тестирования
Все способы тестирования ПС объединяются базой данных, где помещаются результаты тестирования системы. В ней содержатся все компоненты, тестовые контрольные данные, результаты тестирования и информ
Анализ языков формальной спецификации программ
Языки спецификаций, используемые для формального описания свойств программ, более высокого уровня, чем ЯП. Их можно классифицировать по таким категориям: универсальные языки с общемат
VDM-спецификация программ
Язык VDM (Vienna Development Method) разработан в венской лаборатории компании IBM для описания языков типа ПЛ/1, трансляторов и систем со сложными структурами данных [6.7, 6.8]. Главная его
Спецификация программ средствами RAISE
RAISE-метод и RSL-спецификация (RAISE Specification Language) [6.9, 6.10] были разработаны в 80-х годах как результат предварительного исследования формальных методов и их пополнения новыми
Спецификации задач концепторным языком
Для постановки сложных математических задач (суммирование бесконечных рядов, теоретикомножественных операций с бесконечными множествами, гильбертов оператор и др.) и задач искусственного интеллекта
Методы доказательства правильности программ
Формальные методы тесно связаны с математическими техниками спецификаций, верификацией и доказательством правильности программ. Эти методы содержат математическую символику, формальную нотацию и ап
Характеристика формальных методов доказательства
Наиболее известными формальными методами доказательства программ являются метод рекурсивной индукции или утверждений Флойда, Наура, метод структурной индукции Хоара и др. [6.4, 6.5, 6.18, 6.19].
Валидация сценариев требований
Рассматривается подход к проверке требований, которые заданы в модели требований, построенной с использованием сценариев и акторов, как внешней сущности по отношению к разрабатываемой систем
Верификация и валидация программ
Верификация и валидация - это методы анализа, проверки спецификаций и правильности выполнения программ в соответствии с заданными требованиями и формальным описанием программы [6.19,
Подходы к верификации моделей
Объектная модель и модель распределенного приложения отражают специфику предметной области и принципы взаимодействияобъектов со средой функционирования. Их верификации посвящен ряд работ, в том чис
Метод верификации композиции правильных компонентов
Метод верификации композиции компонентов базируется на спецификации функций и временных (temporal) свойствах готовых проверенных компонентов (типа reuse) [6.23]. Свойства составного компонен
Перспективные направления верификации программ
По данным, опубликованным в [6.15], ежегодно ошибки в ПО США обходятся в 60 млрд. долларов. Для преодоления этих проблем американские специалисты и специалисты из европейских стран по формальным ме
Хотите получать на электронную почту самые свежие новости?
Подпишитесь на Нашу рассылку
Наша политика приватности обеспечивает 100% безопасность и анонимность Ваших E-Mail
- программа, выполняемая символически на наборах данных 
, где 
и 
- множество входных данных.
и обозначим состояние выполнения программы в виде тройки
- номер текущего оператора программы 
, 
( 
) - условие выбора пути в программе (вначале 
) в виде логического выражения над данными 
; 
- множество пар 
, в которых 
- переменная программы, а 
- ее значение; 
- множество промежуточных и выходных данных.
, 
, 
в выражение 
подставляются символьные значения переменных 
и 
, в результате чего получается выражение 
, которое становится значением переменной 
. Вхождение в полученное выражение 
не определены.
то 
иначе 
" вычисляется выражение 
, то формируются логические формулы:
, то только одна из этих формул может быть выполнимой, а именно если
не следует ни 
), тогда один набор данных, который удовлетворяет 
и 
. Получаем, что 
, тогда когда
, где 
- входная спецификация, когда ее нет, то 
выходной спецификации 
проводится доказательство выполнимости логических формул 
и 
, где 
Новости и инфо для студентов