VDM-спецификация программ - Лекция, раздел Философия, Конспект лекций по дисциплине Надежность систем В данной лекции систематически изложены следующие взаимосвязанные аспекты инженерии ПО Язык Vdm (Vienna Development Method) Разработан В Венской Лаборатории ...
Язык VDM (Vienna Development Method) разработан в венской лаборатории компании IBM для описания языков типа ПЛ/1, трансляторов и систем со сложными структурами данных [6.7, 6.8]. Главная его цель - специфицировать правильно программу и описать набор утверждений для ее доказательства, принося в жертву скорость разработки и эффективность, даже если полученная программа громоздка и не всегда удобна в использовании, но является правильной.
Этот язык имеет математическую символику, которая легко воспринимается математически подготовленными студентами последних курсов университетов за 5-6 лекций. В языке содержатся следующие типы данных:
· - натуральные числа с нулем;
· - натуральные числа без нуля;
· - целые числа;
· - булевы;
· - строки символов;
· - знаки и специальные обозначения операций.
Функцияв языке - это определение свойств структур данных и операций над ними аппликативно или императивно. В первом случае функция специфицируется через комбинацию других функций и базовых операций (через выражения), что соответствует синониму функциональный.Во втором случае - значение определяется описанием алгоритма, что соответствует синонимуалгоритмический. Например, спецификация функции вычисления минимального значения из двух значений в VDMимеет вид:
Объекты языка VDM. Все объекты строятся иерархически. Элементами данных, с которыми оперируют функции, могут быть множества, деревья, последовательности, отображения, а также более сложные структуры, образованные с помощью конструкторов.
Множествоможет быть конечное и обозначается . При работе с множеством используются операции , , , и др. Язык имеет правила проверки правильности задания этих операций. Пример, будет корректным только тогда, когда является подмножеством множества, которому принадлежит . Пример дистрибутивного объединения дан ниже:
Списки ( последовательности ) - это цепочки элементов одинакового типа из множества . Операция задает длину списка, а - номера элементов списка.
Например, .
К списковым операциям относится взятие первого (головы) элемента списка - и остатка (хвоста) после удаления первого элемента из списка - .
Например, , .
Могут использоваться также операция конкатенации (соединение двух списков) и операция дистрибутивной конкатенации.
Дерево- это конструкция , позволяющая объединять структуры разной природы (последовательности, множества и отображения). Элементы деревьев могут конструироваться в виде составных объектов, а также применяется деструктор для именования констант, вносимых в ранее определенный составной объект.
Пример. Пусть - переменная типа Время, значение которой - 10 ч. 30 мин, тогда конструкция определяет значение , а .
Отображение- это конструкция , позволяющая создавать абстрактную таблицу из двух столбцов: ключей и значений. Все объекты таблицы принадлежат одному типу данных - множеству. Операция позволяет строить множество ключей, а - множество его значений. Кроме того, есть операции исключения строки, слияния двух таблиц и др.
Приведенные конструкции используются для спецификации программы и, в частности, начального состояния с инвариантными свойствами, в качестве которого используется функция, содержащая описание типов аргументов, результата и операций самой функции. Для проверки правильности спецификации программы средствами языка VDM задаются пред- и постусловия, аксиомы и утверждения.
Предусловие - это предикат с операцией, к которой обращается программа после получения начального состояния для определения правильности выполнения или фиксации ошибочной ситуации.
Утверждение задает описание операций проверки правильности программы в разных ее точках. Операторы программы изменяют состояние переменных в заданной точке, а операции утверждений анализируют ее (например, после операции работы с БД) в целях определения правильности выполнения этой операции. При возникновении непредвиденной ситуации, аксиомы и утверждения должны предусматривать соответствующие действия.
Постусловие - это предикат, который - истинный после выполнения предусловия, завершения текущих операции в заданных точках при выполнении инвариантных свойств программ.
Метод VDM предусматривает пошаговую детализацию спецификации программ. На первом уровне строится грубая спецификация - модель в языке VDM, которая постепенно уточняется, пока не получится окончательный текст описания программы.
Разработка спецификации проводится по следующей схеме:
1. Определение терминов, которыми будет специфицироваться программа.
2. Описание понятий и объектов, для обозначения которых используется денотат, идентифицируемый с помощью некоторого имени (или фразы).
3. Описание инвариантных свойств программы.
4. Определение операций над структурами программы (например, ввести объект, удалить и др.), изменяющие ее состояние и сохранение инвариантных свойств.
При переходе от одного шага детализации к другому модель программы детализируется и постепенно становится ближе к конечному описанию. Функции - это операции, которые уточняются при детализации структуры программы на каждом шаге спецификации и описания поведения модели.
При реальном выполнении спецификация исполняется итерационно. На первом уровне проверяется только свойства модели программы при заданных ограничениях независимо от среды. Затем используется уточненная и расширенная спецификация с набором формальных утверждений. И так до тех пор, пока окончательно не будет завершен процесс пошагового доказательства спецификации.
Для демонстрации возможностей VDM языка рассмотрим задачу поиска ("Поиск") в каталоге ( ) репозитария компонентов имени компонента и сравнения его с заданным в запросе пользователя. В случае совпадения имен проверяются параметры, и при их совпадении из каталога извлекается код компонента и передается пользователю.
Спецификация переменных программы "Поиск"
где - cведения о разработчике компонента ; - переменная, в которую посылается код компонента, выбранного из каталога репозитария при совпадении имен в каталоге и запросе; - переменная, в которой хранится текущий элемент из репозитария, найденный по фасете компонента с номером для ; - имя разработчика компонента; - переменная, которая используется для задания признака - компонент не найден или к нему никто не обращался.
Описание инвариантных свойств программы
Операторы программы проверяют список имен компонентов в каталоге, который содержит элементов типа . Если они совпадают с именем в запросе, результат сохраняется в .
Доказательство инвариантных свойств программ должно проводиться автоматизированным способом с помощью специально созданных инструментальных средств поддержки VDM языка.
Тема... В данной лекции систематически изложены следующие взаимосвязанные аспекты... теоретический и интеллектуальный базис методы принципы средства и методологии и др проектирования...
Если Вам нужно дополнительный материал на эту тему, или Вы не нашли то, что искали, рекомендуем воспользоваться поиском по нашей базе работ:
VDM-спецификация программ
Что будем делать с полученным материалом:
Если этот материал оказался полезным ля Вас, Вы можете сохранить его на свою страничку в социальных сетях:
Анализ и характеристика областей знаний 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].
Для этих целей, как прав
Управление процессом тестирования
Все способы тестирования ПС объединяются базой данных, где помещаются результаты тестирования системы. В ней содержатся все компоненты, тестовые контрольные данные, результаты тестирования и информ
Анализ языков формальной спецификации программ
Языки спецификаций, используемые для формального описания свойств программ, более высокого уровня, чем ЯП. Их можно классифицировать по таким категориям: универсальные языки с общемат
Спецификация программ средствами RAISE
RAISE-метод и RSL-спецификация (RAISE Specification Language) [6.9, 6.10] были разработаны в 80-х годах как результат предварительного исследования формальных методов и их пополнения новыми
Спецификации задач концепторным языком
Для постановки сложных математических задач (суммирование бесконечных рядов, теоретикомножественных операций с бесконечными множествами, гильбертов оператор и др.) и задач искусственного интеллекта
Методы доказательства правильности программ
Формальные методы тесно связаны с математическими техниками спецификаций, верификацией и доказательством правильности программ. Эти методы содержат математическую символику, формальную нотацию и ап
Характеристика формальных методов доказательства
Наиболее известными формальными методами доказательства программ являются метод рекурсивной индукции или утверждений Флойда, Наура, метод структурной индукции Хоара и др. [6.4, 6.5, 6.18, 6.19].
Валидация сценариев требований
Рассматривается подход к проверке требований, которые заданы в модели требований, построенной с использованием сценариев и акторов, как внешней сущности по отношению к разрабатываемой систем
Методы анализа структур программ
Методы анализа структуры программ относятся к доказательству правильности программ [6.20] и состоят в их инспекции независимыми экспертами с участием самих разработчиков. Они проверяют полноту, цел
Верификация и валидация программ
Верификация и валидация - это методы анализа, проверки спецификаций и правильности выполнения программ в соответствии с заданными требованиями и формальным описанием программы [6.19,
Подходы к верификации моделей
Объектная модель и модель распределенного приложения отражают специфику предметной области и принципы взаимодействияобъектов со средой функционирования. Их верификации посвящен ряд работ, в том чис
Метод верификации композиции правильных компонентов
Метод верификации композиции компонентов базируется на спецификации функций и временных (temporal) свойствах готовых проверенных компонентов (типа reuse) [6.23]. Свойства составного компонен
Перспективные направления верификации программ
По данным, опубликованным в [6.15], ежегодно ошибки в ПО США обходятся в 60 млрд. долларов. Для преодоления этих проблем американские специалисты и специалисты из европейских стран по формальным ме
Хотите получать на электронную почту самые свежие новости?
Подпишитесь на Нашу рассылку
Наша политика приватности обеспечивает 100% безопасность и анонимность Ваших E-Mail
Новости и инфо для студентов