ГОСТ Р МЭК 61508-7—2007
- временные выражения, предусмотренные для представления как текущего момента, так и момента вызо
ва метода внутри тела метода:
- выражение, описывающее синхронизирующий сигнал, которое может быть добавлено к методу для специ
фикации верхних (или нижних) пределов времени исполнения для корректности реализаций;
- переменные непрерывного времени, которые должны быть введены. С условными операторами и опера
торами действия допускается специфицировать отношения (например дифференциальные уравнения) между
этими временными функциями, что оказалось очень полезно при спецификации требований к системам, действу
ющим в среде с непрерывным временем. Уточняющие шаги приводят кдискретным программным решениям для
программ реального времени.
Литература:
Conformity Clause for VDM-SL, G. I. 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.
Major VDM+ - Language characteristics: http:/>\vww.ifad.dk/productsArdmlangchar.html
Systematic Software Development using VDM. С. B. Jones. Prentice-Hall. 2nd Edition. 1990.
Software Development - A Rigorous Approach. С. B. Jones. Prentice-Hall. 1980.
Formal Specification and Software Development. D. Bjomer and С. B. Jones. Prentice-Hall. 1982.
The Specification of Complex Systems. B. Cohen. W. T. Harwood and M. I. Jackson. Addison Wesley. 1986.
C.2.4.92
Цель: 2 — это нотация языка спецификаций для последовательных систем и метод проектирования, позво
ляющий разработчику выполнять работу, начиная со спецификации на языке 2 до исполнительных алгоритмов,
обеспечивая при этом доказательство их корректности по отношению к спецификации.
Язык 2 в принципе используется на этапе спецификации, однако данный язык был разработан для исполь
зования от этапа составления спецификации до проектирования и реализации систем. Более всего он подходит
для разработки последовательных систем, ориентированных на данные.
Описание: как и в VDM. в методе спецификации, реализованном в языке 2. состояние системы моделиру
ется в терминах теоретико-множественных структур, в которых описаны инварианты (предикаты), а операции над
этим состоянием моделируются путем определения их пред- и пост-условий в терминах системных состояний.
Операции допускается проверять на сохранение системных инвариантов для демонстрации их согласованности.
Формальная часть спецификации подразделяется на схемы, которые обеспечивают возможность структурирова
ния спецификаций путем их усовершенствования.
Обычно спецификация 2 представляет собой сочетание формального текста на языке 2 и неформального
пояснительного текста на естественном языке. Формальный текст сам по себе может оказаться слишком сжатым
для простого восприятия и часто его смысл необходимо пояснять, тогда как неформальный, естественный язык
может оказаться неоднозначным и неточным.
В отличие от VDM язык 2 представляет собой скорее нотацию, чем завершенный метод. Однако был разра
ботан близкий метод (метод В), который может быть использован в сочетании с языком Z. Метод В основан на
принципе пошагового уточнения.
Литература:
The Z Notation — A Reference Manual. J. M. Spivey. Prentice-Hall, 1992. Specification Case Studies. Edited by I.
Hayes. Prentice-Hall. 1987.
The В Method. J. R. Abrial et al. VDM 91 Formal Software Development Methods. (S. Prehen и W. J. Toelenel.
eds). Springer Verlag, 398 — 405. 1991.
Specification of the UNIX Filestore. C Morgan and B. Sufrin. IEEE Transactions on Software Engineering. SE-10.
2. March 1984.
C.2.5 Программирование с защитой
П р и м е ч а н и е — Ссылка на данный метод|’средство приведена в МЭК 61508-3 (таблица А.4).
Цель: создание программ, выявляющих во время их исполнения аномальные потоки управления, данных
или значения данных и реагирующих на них заранее определенным и приемлемым способом.
Описание: в процессе разработки программ допускается использовать разные методы для проверки ано
малий в потоках управления или данных. Эти методы могут применяться систематически в процессе программи
рования системы для снижения вероятности ошибочном обработки данных.
Существуют два пересекающихся множества методов защиты. Внутренние методы защиты отошибок проек
тируются в программных средствах для преодоления недостатков впроцессе создания этих программных средств.
Эти недостатки могут быть обусловлены ошибками при проектировании или кодировании, либо ошибочными
требованиями. Ниже перечислены некоторые из рекомендаций по защите:
- проверка диапазона значений переменных;
- проверка значений переменных на их достоверность (если возможно):
- проверка типа, размерности и диапазона значений параметров процедур на входе процедур.
Представленные три рекомендации помогают гарантировать допустимость значений, обрабатываемых в
программах, как с точки зрения терминов программных функций, так и физических значений переменных.
38