Формальные специфики программ
Содержание
Введение 3
1 Формальные спецификации, доказательства и верификации программ 4
1.1 Анализ языков формальной спецификации программ 4
1.2 VDM-спецификация программ 6
1.3 Спецификация программ средствами RAISE 8
1.4 Спецификации задач концепторным языком 8
1.5 Методы доказательства правильности программ 11
1.6 Характеристика формальных методов доказательства 11
1.7 Валидация сценариев требований 13
1.8 Методы анализа структур программ 15
1.9 Верификация и валидация программ 16
2 История и основные идеи KVEST 17
2.1 История разработки и основные идеи KVEST 17
2.2 Шаги методологии 20
2.2.1 Определение состава программного контракта 20
2.2.2 Разработка спецификаций Цели 21
2.2.3 Генерация тестовых наборов 21
2.2.4 Выполнение тестов и анализ результатов 21
2.2.5 Метод тестирования 22
2.3 Технология генерации тестов 23
2.4 Интеграция обратной и прямой инженерии ПО 25
Заключение 26
Список использованной литературы 29
Введение
Формальные спецификации и методы доказательства их правильности являются современными направлениями в области проверки правильности программ. Для доказательства того, что спецификация программы задает правильное решение некоторой задачи, для которой она разработана, привлекается математический аппарат.
В формальных методах проводитсяанализ текста и описание поведения программы в стиле, близком математической нотации, путем рассуждений и доказательств, принятых в математике.
Спецификация является формальным описанием функций и данных программы, с которыми эти функции оперируют. Различают следующие виды данных:
1 Формальные спецификации, доказательства и верификации программ
1.1 Анализ языков формальной спецификации программ
Языки спецификаций, который используются для формального описания свойств программможно классифицировать по следующим категориям:
- универсальные языки с общематематической основой (например, RAISE, Z, API, VDM и др.);
- языки спецификации проблемных областей (например, ЯП, языки спецификаций ПрО или доменов - DSL и др.);
- специализированные языки спецификации (например, языки таблиц, логики, равенств и подстановок и др.);
- языки, ориентированные на спецификацию параллельных процессов (например, CIP-L, Ada-68 Concurrent Pascal и др.) (рис.1.1).
1.2 VDM-спецификация программ
Язык VDM (ViennaDevelopmentMethod) разработан в венской лаборатории компании IBM для описания языков типа ПЛ/1, трансляторов и систем со сложными структурами данных. Цель языка спецификации VDMзаключается в правильном специфицировании программы и описании набора утверждений для ее доказательства, принося в жертву скорость разработки и эффективность, даже если полученная программа громоздка и не всегда удобна в использовании, но является правильной.
Функция в языке VDMаппликативно или императивно определяет свойства структур данных и операций над ними. В первом случае функция специфицируется через комбинацию других функций и базовых операций (через выражения). Во втором случае, значение функции определяется описанием алгоритма.
1.3 Спецификация программ средствами RAISE
RAISE-метод и RSL-спецификация (RAISE SpecificationLanguage) были разработаны в 80-х годах как результат предварительного исследования формальных методов и их пополнения новыми возможностями. Метод содержит нотации, техники и инструменты для конструирования программ и доказательстве их правильности. Он имеет программную поддержку в виде набора инструментов и методик, которые постоянно развиваются и используются при доказательстве правильности программ, описанных в RSL и ЯП (С++ и Паскаль). Язык RSL содержит абстрактные параметрические типы данных (алгебраические спецификации) и конкретные типы данных (модельноориентированные), подтипы, операции для задания последовательных и параллельных программ. Он предоставляет аппликативный и императивный стиль спецификации абстрактных программ, а также формальное конструирование программ в других ЯП и доказательство их правильности. Синтаксис этого языка близок к синтаксису языков С++ и Паскаль.
1.4 Спецификации задач концепторным языком
Для постановки сложных математических задач (суммирование бесконечных рядов, теоретико-множественных операций с бесконечными множествами, гильбертов оператор и др.) и задач искусственного интеллекта (игры, распознавание образов и др.) предложен общематематический процедурный язык, так называемый концепторный язык. В этом языке процесс описания сложной задачи проводится путем обоснования решения задачи с математической точки зрения, затем формального описания постановок задач и, наконец, делается переход к алгоритмическому описанию.
1.5 Методы доказательства правильности программ
Формальные методы тесно связаны с математическими техниками спецификаций, верификацией и доказательством правильности программ. Эти методы содержат математическую символику, формальную нотацию и аппарат вывода. Правила доказательства являются громоздкими и поэтому на практике редко используются рядовыми программистами. Однако с теоретической точки зрения они развивают логику применения математического метода индукции при проверке правильности программ. На основеспецификации программ проводится частичное и полное доказательство правильности программ.
1.6 Характеристика формальных методов доказательства
Наиболее известными формальными методами доказательства программ являются метод рекурсивной индукции или утверждений Флойда, Наура, метод структурной индукции Хоара и др. Метод Флойда основан на определении условий для входных и выходных данных и в выборе контрольных точек в доказываемой программе так, чтобы путь прохождения по программе пересекал хотя бы одну контрольную точку. Для этих точек формулируются утверждения о состоянии и значениях переменных в них (для циклов эти утверждения должны быть истинными при каждом прохождении циклаинварианта).
1.7 Валидация сценариев требований
Рассматривается подход к проверке требований, которые заданы в модели требований, построенной с использованием сценариев и акторов, как внешней сущности по отношению к разрабатываемой системе
Сценарий после трансформации - это последовательность взаимодействий между одним или несколькими акторами и системой, в которой актор выполняет цели сценария при взаимодействии с ней. В модели требований сценарий задает несколько альтернативных событий, заданных на языке диаграмм UML. Они разделяются на функциональные (системные) и внутренние, определяющие поведение системы. На основе описания сценарных требования проводится их валидация.
Валидация требований - это процесс выявления ошибок в представлении сценарных требований, он итерационный и состоит из следующих шагов:
1.8 Методы анализа структур программ
Методы анализа структуры программ относятся к доказательству правильности программ и состоят в их инспекции независимыми экспертами с участием самих разработчиков. Они проверяют полноту, целостность, однозначность и непротиворечивость определений в программе. Сущность инспекции заключается в том, что эксперты пытаются взглянуть на программу "со стороны", подвергнуть ее всестороннему критическому анализу, рассмотреть словесные объяснения разработчиков о способах ее разработки. Цель инспекции - обнаружение ошибок в логике и в исходной программе в статике.
1.9 Верификация и валидация программ
Верификация и валидация - это методы анализа, проверки спецификаций и правильности выполнения программ в соответствии с заданными требованиями и формальным описанием программы [6.19, 6.20].
Верификация помогает сделать заключение о корректности созданной программной системы после завершения ее разработки.Валидация позволяет установить выполнимость заданных требований путем их просмотра, инспекции и оценки результатов проектирования на этапах ЖЦ для подтверждения того, что проводится корректная реализация требований, соблюдение заданных условий и ограничений к системе. Верификация и валидация обеспечивают проверку полноты, непротиворечивости и однозначности спецификации и правильности выполнения функций системы в соответствии с требованиями.
Верификации и валидации подвергаются:
2 История и основные идеи KVEST
2.1 История разработки и основные идеи KVEST
В 1994 году NortelNetworks (предыдущие названия: Bell-Northern Research, NorthernTelecom и Nortel) предложил ИСП РАН разработать методологию и комплект инструментов автоматизации тестирования интерфейсов прикладных программ (ApplicationProgramInterface - API). Первым практическим применением методологии стало ядро операционной системы реального времени. Был строго описан программный контракт ядра ОС и созданы тестовые наборы для проверки выполнения реализацией программного контракта.
Будем различать методологию и технологию, совокупность технических решений и инструментов, поддерживающих KVEST методологию. Методология KVEST нацелена на фиксацию программных контрактов и различные способы использования спецификаций программных контрактов.