ГОСТ Р МЭК 61508-7—2012
системы на этапе ее спецификации без необходимости знакомства с методами, лежащими в основе формальных
спецификаций.
Как и все другие методы ADT, метод OBJ применим только к последовательным системам или к последо
вательным аспектам параллельных систем. Метод OBJ применяют для спецификации как малых, так и крупных
промышленных применений.
Литература:
Software Engineering with OBJ: Algebraic Specification in Action. J. Goguen. G. Malcotm. Springer. 2000, ISBN
0792377575. 9780792377573.
C.2.4.7 Временная логика
Цель. Непосредственное выражение требований к безопасности и эксплуатации, а также формальное пред
ставление сохранения этих качеств на последующих этапах разработки.
Описание. Стандартная предикатная логика первого порядка не содержит концепций времени. Временная
логика расширяет логику первого порядка добавлением модальных операторов (например «с этого момента» и
«случайно»). Эти операторы могут использоваться для уточнения суждений о системе. Например, свойства безо
пасности могут потребовать использовать модальный оператор «с этого момента», но может потребоваться, чтобы и
другие необходимые состояния системы были достигнуты «случайно» из некоторого другого начального состо яния.
Временные формулы интерпретируются последовательностями состояний (поведениями). Представление
состояния зависит от выбранного уровня описания. Оно может относиться ко всей системе, системным элементам
или компьютерной программе.
Квантифицированные временные интервалы и ограничения во временной логике явно не обрабатываются.
Абсолютное время обрабатывается путем образования дополнительных временных состояний, что является ча
стью описания состояния.
Литература:
Mathematical Logic for Computer Science. M. Ben-Ari. Springer. 2001, ISBN 1852333197. 9781852333195.
C.2.4.8 VDM. VDM++ — метод разработки Vienna
Цель. Систематическая спецификация и реализация последовательных (VDM) и параллельных (VDM++)
программ реального времени.
Описание. VDM — это математический метод спецификации и уточнения реализаций, который позволяет
доказать их корректность относительно спецификации.
В этом основанном на модели методе спецификации состояние системы моделируется в терминах теорети
ко-множественных структур, в которых описаны инварианты (предикаты), а операции над этим состоянием модели
руются путем определения их пред- и постусловий в терминах системных состояний. Операции могут проверяться
на сохранение системных инвариантов.
Выполнение спецификаций осуществляется путем реализации состояния системы в терминах структур дан
ных в заданном языке и уточнения операций в терминах программы на заданном языке. Этапы реализации и уточ
нения позволяют логически вывести свойства, устанавливающие корректность этих этапов. Выполняются или нет
эти свойства, определяет разработчик.
В принципе VDM используется на этапе создания спецификации, но гложет также использоваться на этапах
проектирования и реализации исходного кода. VDM может быть также применен к последовательно структуриро
ванным программам или к последовательным процессам в параллельных системах.
Объектно ориентированное и параллельное для реального времени расширения VDM. VDM++ представля
ют собой язык формализованных спецификаций, основанный на языке VDM-SL, созданном в ИСО. и на обьектно-
ориентированном языке Smalltalk.
VDM++ имеет широкий диапазон конструкций, что позволяет пользователю формально специфицировать
параллельные системы реального времени в обьектно-ориентированной среде. В VDM++ полная формальная
спецификация содержит совокупность спецификаций классов и отдельных характеристик рабочего пространства.
К средствам описания реального времени на языке VDM++ относятся:
- временные выражения, предусмотренныедля представления как текущего момента, так и момента вызова
метода внутри тела метода:
- выражение, описывающее синхронизирующий сигнал, которое может быть добавлено к методу
для спецификации верхних (или нижних) пределов времени исполнения для корректности реализаций:
- переменные непрерывного времени, которые должны быть введены. С условными операторами и опе
раторами действия допускается специфицировать отношения (например дифференциальные уравнения) между
этими временными функциями, что оказалось очень полезно при спецификации требований к системам, дей
ствующим в среде с непрерывным временем. Уточняющие шаги приводят к дискретным программным решениям
для программ реального времени.
Литература:
ISO/IEC 13817-1:1996. Information technology— Programming languages, theirenvironmentsand system software
interfaces — Vienna Development Method — Specification Language — Part 1: Base language.
Systematic Software Development using VDM. С. B. Jones. Prentice-Hall. 2nd Edition. 1990.
Conformity Clause for VDM-SL. G.l. Parkin and B.A. Wichmann. Lecture Notes in Computer Science 670. FME’93
Industrial-Strength Formal Methods. First International Symposium of Formal Methods in Europe. Editors: J. С P. Woodcock
and P.G. Larsen. Springer Verlag. 501—520.
38