ГОСТ Р МЭК 62279—2016
шаговое уточнение системы (стратегия сверху вниз) в рамках композиции взаимодействующих процессов, общее
поведение которых формирует также поведение всей системы. В равной степени можно выполнять и стратегию
снизу вверх, комбинируя процессы и получая в результате необходимые свойства формируемой системы, исполь
зуя правила вывода композиционного типа.
D.28.4
Л
огика высшего порядка (HOL)
Цель. Формальный язык, предназначенный в качестве основы для спецификации и верификации аппарат
ных средств.
Описание. HOL представляет собой разработанную в компьютерной лаборатории Кембриджского универ
ситета конкретную логическую нотацию и систему, которая ее автоматически поддерживает.
Л
огическая нотация
взята в основном из простой теории типов Черча, а машинная реализация основана на теории LCF (логике вы
числимых функции).
D.28.5 LOTOS
Цель. LOTOS является средством для описания и анализа поведения систем, реализующих параллельные
коммуникационные процессы.
Описание. LOTOS (язык для спецификации процессов, упорядоченных во времени) основан на CCS с до
полнительными возможностями из близких алгебраических теорий CSP и CIRCAL (теория цепей). LOTOS преодо
левает недостатки CCS в управлении структурами данных и представлении значений выражений, объединяя его с
аспектами языка абстрактных типов данных ACT ONE. Процесс описания аспектов в LOTOS может быть однако
использован для других формальных методов при описании абстрактных типов данных.
D.28.6 OBJ
Цель. Обеспечение точной спецификации системы в процессе диалога с пользователем и подтверждение
соответствия системы до ее реализации.
Описание. OBJ представляет собой алгебраический язык спецификаций. Пользователи определяют требо
вания в терминах алгебраических выражений. Системные аспекты (поведение или конструктивы) специфициру
ются в терминах операций, действующих над абстрактными типами данных (ADT). ADT подобен языку ADA3), где
поведение оператора наблюдаемо, однако подробности реализации скрыты.
Спецификация OBJ и последующая пошаговая реализация подвергаются тем же формальным методам про
верки. что и другие формальные методы. Более того, поскольку конструктивные аспекты спецификации OBJ авто
матически исполнимы, существует непосредственная возможность подтверждения соответствия системы на осно ве
самой спецификации. Исполнение — это по существу оценка функций системы путем подстановки выражений
(перезаписыванием), которая продолжается до тех пор. пока не будут получены конкретные выходные значения.
Эта исполнимость позволяет конечным пользователям рассматриваемой системы получать «облик» планируемой
системы на этапе ее спецификации без необходимости знакомства с методами, лежащими в основе формальных
спецификаций.
Как и все другие методы ADT. метод OBJ применим только к последовательным системам или к последо
вательным аспектам параллельных систем. Метод OBJ применяют для спецификации как малых, так и крупных
промышленных применений.
D.28.7 Временная логика
Цель. Непосредственное выражение требований к безопасности и эксплуатации, а также формальное пред
ставление сохранения этих качеств на последующих этапах разработки.
Описание. Стандартная предикатная логика первого порядка не содержит концепций времени. Временная
логика расширяет логику первого порядка добавлением модальных операторов (например «с этого момента» и
«случайно»). Эти операторы могут использоваться для уточнения суждений о системе. Например, свойства безо
пасности могут потребовать использовать модальный оператор «с этого момента», но может потребоваться, чтобы и
другие необходимые состояния системы были достигнуты «случайно» из некоторого другого начального состо яния.
Временные формулы интерпретируются последовательностями состояний (поведениями). Представление
состояния зависит от выбранного уровня описания. Оно может относиться ко всей системе, системным элементам
или компьютерной программе. Квантифицированные временные интервалы и ограничения во временной логике
явно не обрабатываются. Абсолютное время обрабатывается путем образования дополнительных временных со
стояний. что является частью описания состояния.
D.28.8 Метод разработки Vienna (VDM)
Цель. Систематическая спецификация и реализация последовательных программ реального времени.
Описание. VDM — это математический метод спецификации и уточнения реализаций, который позволяет
доказать их корректность относительно спецификации.
В этом основанном на модели методе спецификации состояние системы моделируется в терминах теорети
ко-множественных структур, в которых описаны инварианты (предикаты), а операции над этим состоянием модели
руются путем определения их пред- и пост-условий в терминах системных состояний. Операции могут проверяться
на сохранение системных инвариантов.
31Ада — структурированный, статически типизированный, императивный, с широким спектром применения,
объектно-ориентированный язык программирования высокого уровня, расширенный от Паскаля и других языков.
79