Характеристика формальных методов доказательства - Лекция, раздел Философия, Конспект лекций по дисциплине Надежность систем В данной лекции систематически изложены следующие взаимосвязанные аспекты инженерии ПО Наиболее Известными Формальными Методами Доказательства Программ Являются Мет...
Наиболее известными формальными методами доказательства программ являются метод рекурсивной индукции или утверждений Флойда, Наура, метод структурной индукции Хоара и др. [6.4, 6.5, 6.18, 6.19].
Метод Флойда основан на определении условий для входных и выходных данных и в выборе контрольных точек в доказываемой программе так, чтобы путь прохождения по программе пересекал хотя бы одну контрольную точку. Для этих точек формулируются утверждения о состоянии и значениях переменных в них (для циклов эти утверждения должны быть истинными при каждом прохождении циклаинварианта).
Каждая точка рассматривается для индуктивного утверждения того, что формула остается истинной при возвращении в эту точку программы и зависит не только от входных и выходных данных, но и от значений промежуточных переменных. На основе индуктивных утверждений и условий на аргументы создаются утверждения с условиями проверки правильности программы в отдельных ее точках. Для каждого пути программы между двумя точками устанавливается проверка на соответствие условий правильности и определяется истинность этих условий при успешном завершении программы на данных, удовлетворяющих входным условиям.
Формирование таких утверждений - довольно сложная задача, особенно для программ с высокой степенью параллельности и взаимодействия с пользователем. Кроме того, трудно проверить достаточность и правильность самих утверждений.
Доказательство корректности применялось для уже написанных программ и тех, которые разрабатываются методом последовательной декомпозиции задачи на подзадачи, для каждой из них формулируются утверждения с учетом условий ввода и вывода и точек программы, расположенными между входными и выходными утверждениями. Суть доказательства истинности выполнения условий и утверждений относительно заданной программы и составляет основу доказательства ее правильности.
Данный метод доказательства уменьшает число ошибок и время тестирования программы, обеспечивает отработку спецификаций программы на полноту, однозначность и непротиворечивость.
Метод Хоара- это усовершенствованный метод Флойда, основанный на аксиоматическом описании семантики языка программирования исходных программ. Каждая аксиома описывает изменение значений переменных с помощью операторов этого языка. Формализация операторов перехода и вызовов процедур обеспечивается с помощью правил вывода, содержащих индуктивные высказывания для каждой точки и функции исходной программы.
Система правил вывода дополняется механизмом переименования глобальных переменных, условиями на аргументы и результаты, а также на правильность задания данных программы. Оператор перехода трактуется как выход из циклов и аварийных ситуаций.
Описание с помощью системы правил утверждений - громоздкое и отличается неполнотой, поскольку все правила предусмотреть невозможно. Данный метод проверялся экспериментально на множестве программ без применения средств автоматизации из-за их отсутствия.
Метод Маккартисостоит в структурной проверке функций, работающих над структурными типами данных, структур данных и диаграмм перехода во время символьного выполнения программ. Эта техника включает в себя моделирование выполнения кода с использованием символов для изменяемых данных. Тестовая программа имеет входное состояние, данные и условия ее выполнения.
Выполняемая программа рассматривается как серия изменений состояний. Самое последнее состояние программы считается выходным состоянием и если оно получено, то программа считается правильной. Данный метод обеспечивает высокое качество исходного кода.
Метод Дейкстрыпредлагает два подхода к доказательству правильности программ. Первый подход основан на модели вычислений, оперирующей с историями результатов вычислений программы, анализом путей прохождения и правил обработки большого объема информации. Второй подход базируется на формальном исследовании текста программы с помощью предикатов первого порядка. В процессе выполнения программа получает некоторое состояние, которое запоминается для дальнейших сравнений.
Основу метода составляет математическая индукция, абстрактное описание программы и ее вычисление. Математическая индукция применяется при прохождении циклов и рекурсивных процедур, а также необходимых и достаточных условий утверждений. Абстракция позволяет сформулировать некоторые количественные ограничения. При вычислении на основе инвариантных отношений проверяются на правильность границы вычислений и получаемые результаты.
Процесс формального доказательства правильности программ методом математической индукции зарекомендовал себя как система правил статической проверки правильности программ за столом для обнаружения в них формальных ошибок. С помощью этого метода можно доказать истинность некоторого предположения в зависимости от параметра для всех , и тем самым доказать случай . Исходя из истинности для любого значения , доказывается , что достаточно для доказательства истинности для всех .
Путь доказательства следующий. Пусть даны описание некоторой правильной программы (ее логики) и утверждение относительно этой программы, которая при выполнении достигает некоторой определенной точки. Проходя через эту точку раз, можно получить справедливость утверждения , если индуктивно доказать, что:
1. справедливо при первом проходе через заданную точку,
2. если справедливо при проходах через заданную точку, то справедливо и прохождение через заданную точку раз.
Исходя из предположения, что программа в конце концов успешно завершится, утверждение о ее правильности будет справедливым.
Тема... В данной лекции систематически изложены следующие взаимосвязанные аспекты... теоретический и интеллектуальный базис методы принципы средства и методологии и др проектирования...
Анализ и характеристика областей знаний 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.20] и состоят в их инспекции независимыми экспертами с участием самих разработчиков. Они проверяют полноту, цел
Верификация и валидация программ
Верификация и валидация - это методы анализа, проверки спецификаций и правильности выполнения программ в соответствии с заданными требованиями и формальным описанием программы [6.19,
Подходы к верификации моделей
Объектная модель и модель распределенного приложения отражают специфику предметной области и принципы взаимодействияобъектов со средой функционирования. Их верификации посвящен ряд работ, в том чис
Метод верификации композиции правильных компонентов
Метод верификации композиции компонентов базируется на спецификации функций и временных (temporal) свойствах готовых проверенных компонентов (типа reuse) [6.23]. Свойства составного компонен
Перспективные направления верификации программ
По данным, опубликованным в [6.15], ежегодно ошибки в ПО США обходятся в 60 млрд. долларов. Для преодоления этих проблем американские специалисты и специалисты из европейских стран по формальным ме
Хотите получать на электронную почту самые свежие новости?
Подпишитесь на Нашу рассылку
Наша политика приватности обеспечивает 100% безопасность и анонимность Ваших E-Mail
в зависимости от параметра 
для всех 
, и тем самым доказать случай 
. Исходя из истинности 
, что достаточно для доказательства истинности 
относительно этой программы, которая при выполнении достигает некоторой определенной точки. Проходя через эту точку 
, если индуктивно доказать, что:
справедливо при первом проходе через заданную точку,
прохождение через заданную точку 
раз.
Новости и инфо для студентов