ГОСТ Р МЭК 61508-7—2007
Спецификация OBJ и последующая пошаговая реализация подвергаются тем же формальным методам
проверки, что и другие формальные методы. Более того, поскольку конструктивные аспекты спецификации OBJ
автоматически исполнимы, существует непосредственная возможность подтверждения соответствия системы на
основе самой спецификации. Исполнение — это по существу оценка функций системы путем подстановки выра
жений (перезаписыванием), которая продолжается до тех пор. пока не будут получены конкретные выходные
значения. Эта исполнимость позволяет конечным пользователям рассматриваемой системы получать «облик»
планируемой системы на этапе ее спецификации без необходимости знакомства с методами, лежащими в осно ве
формальных спецификаций.
Как и все другие методы ADT. метод OBJ применим только к последовательным системам или к последова
тельным аспектам параллельных систем. Метод OBJ применяют для спецификации как малых, так и крупных
промышленных приложений.
Литература:
An Introduction to OBJ: A language for Writing and Testing Specifications. J. A. Goguen and J. Tardo, Specification
of Reliable Software. IEEE Press 1979, reprinted in Software Specification Techniques. N. Gehani, A. McGrettrick (eds).
Addison-Wesley. 1985.
Algebraic Specification for Practical Software Production. C. Rattray. Cogan Press. 1987.
An Algebraic Approach to the Standardisation and Certification of Graphics Software. R. Gnatz. Computer Graphics
Forum 2 (2/3), 1983.
C.2.4.7 Временная логика
Цель: непосредственное выражение требований к безопасности и эксплуатации, а также формальное пред
ставление сохранения этих качеств на последующих этапах разработки.
Описание: стандартная предикатная логика первого порядка не содержит концепций времени. Временная
логика расширяет логику первого порядка добавлением модальных операторов (например, «с этого моментаи и
«случайно»). Эти операторы могут использоваться для уточнения суждений о системе. Например, свойства безо
пасности могут потребовать использовать модальный оператор «с этого момента», но может потребоваться,
чтобы и другие необходимые состояния системы были достигнуты «случайно» из некоторого другого начального
состояния. Временные формулы интерпретируются последовательностями состояний (поведениями). Представ
ление состояния зависит от выбранного уровня описания. Оно может относиться ко всей системе, системным
компонентам или компьютерной программе.
Квантифицированные временные интервалы и ограничения во временной логике не обрабатываются явно.
Абсолютное время обрабатывается путем образования дополнительных временных состояний, что является
частью описания состояния.
Литература:
Temporal Logic of Programs. F. Kroger. EATCS Monographs on Computer Science. Vol. 8. Springer Verlag. 1987.
Design for Safety using Temporal Logic. J. Gorski. SAFECOMP 86. Sarlat. France. Pergamon Press. October 1986.
The Temporal Logic of Programs. A. Pnueti. 18th Annual Symposium on Foundations of Computer Science.
IEEE. 1977.
Verifying Concurrent Processes Using Temporal Logic. Hailpem. T. Brent. Springer Verlag, 1981.
C.2.4.8 VDM. VDM++ — метод разработки Vienna
Цель: систематическая спецификация и реализация последовательных (VDM) и параллельных (VDM++)
программ реального времени.
Описание: VDM — это математический метод спецификации и уточнения реализаций, который позволяет
доказать их корректность относительно спецификации.
В этом основанном на модели методе спецификации состояние системы моделируется в терминах теоре
тико-множественных структур, в которых описаны инварианты (предикаты), а операции над этим состоянием
моделируются путем определения их пред- и пост-условий в терминах системных состояний (29). Операции
могут проверяться на сохранение системных инвариантов.
Выполнение спецификаций осуществляется путем реализации состояния системы в терминах структур
данных в заданном языке и уточнения операций в терминах программы на заданном языке. Этапы реализации и
уточнения позволяют логически вывести свойства, устанавливающие корректность этих этапов. Выполняются или
нет эти свойства, определяет разработчик.
В принципе VDM используется на этапе создания спецификации, но может также использоваться на этапах
проектирования и реализации исходного кода. VDM может быть также применен к последовательно структуриро
ванным программам или к последовательным процессам в параллельных системах.
Обьектно-ориентированное и параллельное для реального времени расширения VDM. VDM++ представ
ляют собой язык формализованных спецификаций, основанный на языке VDM-SL. созданном в ИСО. и на обьек-
тно-ориентированном языке Smalltalk.
VDM++ имеет широкий диапазон конструкций, что позволяет пользователю формально специфицировать
параллельные системы реального времени в обьектно-ориентированной среде. В VDM++ полная формальная
спецификация содержит совокупность спецификаций классов и отдельных характеристик рабочего пространства.
К средствам описания реального времени на языке VDM++ относятся:
37