ГОСТРМЭК 62279—2016
Выполнение спецификаций осуществляется путем реализации состояния системы в терминах структур дан
ных в заданном языке и уточнения операций в терминах программы на этом заданном языке. Этапы реализации и
уточнения позволяют логически вывести свойства, устанавливающие корректность этих этапов. Выполняются или
нет эти свойства, определяет проектировщик.
В принципе VDM используется на этапе создания спецификации, но может также использоваться на этапах
проектирования и реализации исходного кода. VDM может быть также применен к последовательно структуриро
ванным программам или к последовательным процессам в параллельных системах.
D.28.9 Z
Цель. Z — это нотация языка спецификаций для последовательных систем и метод проектирования, позво
ляющий проектировщику выполнять работу, начиная со спецификации на языке Z до исполнительных алгоритмов,
обеспечивая при этом доказательство их корректности по отношению к спецификации.
Язык Z в принципе используется на этапе спецификации, однако данный язык был разработан для использо
вания от этапа составления спецификации до проектирования и реализации систем. Более всего он подходит для
разработки последовательных систем, ориентированных на данные.
Описание. Как и в VDM. в реализованном в языке Z методе спецификации состояние системы моделируется
в терминах теоретико-множественных структур, в которых описаны инварианты (используя предикаты), а операции
над этими состояниями моделируются путем определения их пред- и пост-условий в терминах системных состо
яний. Операции допускается проверять на сохранение системных инвариантов для демонстрации их согласован
ности. Формальная часть спецификации разделяется на схемы, которые обеспечивают возможность структуриро
вания спецификаций путем их уточнения.
Обычно спецификация Z представляет собой сочетание формального текста на языке Z и неформального
пояснительного текста на естественном языке. Формальный текст сам по себе может оказаться слишком сжатым
для простого восприятия и часто его смысл необходимо пояснять, тогда как неформальный, естественный язык
может оказаться неоднозначным и неточным.
В отличие от VDM язык Z представляет собой скорее нотацию, чем завершенный метод. Однако был раз
работан близкий метод (метод В), который может быть использован в сочетании с языком Z. Метод В основан на
принципе пошагового уточнения.
D.28.10 Метод В
Цель. Как и VDM. цепь метода В состоит в том, чтобы формально промоделировать систему или программ
ное обеспечение и доказать, что поведение системы или программного обеспечения соответствует свойствам,
которые были выявлены во время моделирования.
Описание. Моделирование в методе В использует математические элементы из теории множеств. С одной
стороны, инварианты (т. е. предикаты) определяют статические свойства модели. С другой стороны, операции
устанавливают постусловия, определяя, таким образом, ее динамическое поведение. Существует возможность
спецификации сложной системы или программного обеспечения, декомпозируя модель в «машины», связанные
ссылками с различной семантикой.
Различают две основные категории моделирования с В формализмом:
- первый (исторически, первый)стремится разрабатывать программное обеспечение. В этом случав цельсо
стоит в том. чтобы создать программу, которая отвечает ее спецификации. Модель состоит из абстрактных машин
(не обязательно детерминированных) и последовательное уточнение этих машин, приводит кдетерминированным
реализациям, записанным в псевдокоде, названном «ВО». Этот псевдокод затем может быть автоматически транс
лирован в целевой язык программирования;
- последний стремится моделировать системы и в этом случае мы говорим о «Событии В». Цель состоит
в том. чтобы однозначно и связно определить систему, которая выполняет явно определенные свойства. Модель
учитывает саму систему и ее окружение. Динамика системы моделируется с помощью «событий», а метод уточне
ния используется для уточнения взаимодействий между системой и ее окружением.
Автоматически генерируется набор доказанных обязательных свойств (логических утверждений, которые
должны быть формально доказаны из гипотез, которые были получены из формальной модели В). Эти доказанные
обязательные свойства гарантируют:
- существование данных, которые реализуют статические и динамические свойства модели;
- что операции (динамическое поведение модели) соответствуют инварианту:
- что уточнение данных и операции (и псевдокод ВО. если необходимо) не противоречит спецификации, за
писанной в абстрактных машинах;
- что каждая операция вызывается в контексте ее предусловия:
- что в случав моделирования программного обеспечения программа действительно завершается (в част
ности, каждый цикл завершается).
Также генерируются другие доказанные обязательные свойства, например проверка целочисленного пере
полнения или потери разрядов.
D.28.11 Проверка модели
Цель. Для заданной модели системы автоматически проверить, удовлетворяет ли эта модель заданной спе
цификации.
80