---

Обычно спецификация Z представляет собой сочетание формального текста на языке Z и неформального пояснительного текста на естественном языке. Формальный текст сам по себе может оказаться слишком сжатым для простого восприятия и часто его смысл необходимо пояснять, тогда как неформальный, естественный язык может оказаться неоднозначным и неточным.

В отличие от VDM язык Z представляет собой скорее нотацию, чем завершенный метод. Однако был разработан близкий метод (метод В), который может быть использован в сочетании с языком 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. Toetenel, eds), Springer Verlag, 398 - 405, 1991.

Specification of the UNIX Filestore. С Morgan and B. Sufrin. IEEE Transactions on Software Engineering, SE-10, 2, March 1984.

C.2.5 Программирование с защитой

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица А.4).

Цель: создание программ, выявляющих во время их исполнения аномальные потоки управления, данных или значения данных и реагирующих на них заранее определенным и приемлемым способом.

Описание: в процессе разработки программ допускается использовать разные методы для проверки аномалий в потоках управления или данных. Эти методы могут применяться систематически в процессе программирования системы для снижения вероятности ошибочной обработки данных.

Существуют два пересекающихся множества методов защиты. Внутренние методы защиты от ошибок проектируются в программных средствах для преодоления недостатков в процессе создания этих программных средств. Эти недостатки могут быть обусловлены ошибками при проектировании или кодировании, либо ошибочными требованиями. Ниже перечислены некоторые из рекомендаций по защите:

- проверка диапазона значений переменных;

- проверка значений переменных на их достоверность (если возможно);

- проверка типа, размерности и диапазона значений параметров процедур на входе процедур.

Представленные три рекомендации помогают гарантировать допустимость значений, обрабатываемых в программах, как с точки зрения терминов программных функций, так и физических значений переменных.

Параметры «только для чтения» и параметры «для чтения-записи» должны быть разделены, и доступ к ним должен проверяться. Программные функции должны рассматривать все параметры в качестве параметров «только для чтения». Символьные константы не должны быть доступны для записи. Это помогает обнаруживать случайные перезаписи или ошибочное использование переменных.

Устойчивые к ошибкам программные средства проектируются в «предположении», что ошибки существуют в самой программной среде, либо используются выходящие за номиналы значения условий или используются предполагаемые условия, но программные средства ведут себя заранее определенным способом. В этом случае применяют следующие проверки:

- проверку на достоверность физических значений входных и промежуточных переменных;

- проверку влияния выходных переменных, предпочтительно путем прямого наблюдения соответствующих изменений состояния системы;

- проверку самими программными средствами своей конфигурации, включая наличие и доступность предполагаемых аппаратных средств, а также завершенность самих программ, что особенно важно для поддержки полноты безопасности в процессе их эксплуатации.

Некоторые из методов защиты программ, например проверки последовательности потока управления, также справляются и с внешними ошибками.

Литература:

Dependability of Critical Computer Systems 1. F. J. Redmill, Elsevier Applied Science, 1988, ISBN 1-85166-203-0.

Dependability of Critical Computer Systems 2. F. J. Redmill, Elsevier Applied Science, 1989, ISBN 1-85166-381-9.

Software Engineering Aspects of Real-time Programming Concepts. E. Schoitsch, Computer Physics Communications 41, North Holland, Amsterdam, 1986.

C.2.6 Стандарты по проектированию и кодированию

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица А.4).

С.2.6.1 Общие положения

Цель: упрощение верификации, с тем чтобы поддержать групповой объективный подход и установить стандартный метод проектирования.

Описание: в самом начале между участниками проекта должны быть согласованы необходимые правила, охватывающие рассмотренные ниже методы проектирования и разработки (например, JSP, MASCOT, сети Петри, и т.д.), а также соответствующие стандарты кодирования (см. С.2.6.2).

Данные правила создаются для облегчения разработки, верификации, оценки и эксплуатации. При этом должны учитываться доступные инструментальные средства, в частности, для аналитиков и развитие средств проектирования [4].

Литература:

Dependability of Critical Computer Systems 1. F. J. Redmill, Elsevier Applied Science, 1988. ISBN 1-85166-203-0.

Verein Deutscher Ingenieure. Software-Zuverlassigkeit - Grundlagen, Konstruktive Mass-nahmen, Nach-weisverfahren. VDI-Verlag, 1993, ISBN 3-18-401185-2.

С.2.6.2 Стандарты кодирования

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.1).

Цель: упростить верификацию разработанного кода.

Описание: до выполнения кодирования должны быть согласованы подробные правила, которых следует придерживаться. К таким правилам обычно относят:

- иметь подробные сведения о модульности, например о виде интерфейса, размерах программных модулей;

- использовать инкапсуляцию, наследование (ограниченное по глубине) и полиморфизм в случае объектно-ориентированных языков;

- исключать или использовать ограниченно некоторые языковые конструкции, например «goto», «equivalence», динамические объекты, динамические данные, структуры динамических данных, рекурсию, указатели и т. п.;

- ограничивать прерывания, допустимые при выполнении критичного для безопасности кода;

- распечатывать программный код (формировать листинг);

- исключать безусловные переходы (например «goto») в программах на языках высокого уровня.

Данные правила созданы для облегчения процессов тестирования программных модулей, верификации, оценки и обслуживания. При этом должны учитываться доступные инструментальные средства, в частности, для аналитиков.

Примечание - Более подробная информация по этим правилам приведена в С.2.6.3 - С.2.6.7

С.2.6.3 Отказ от динамических переменных или динамических объектов

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.1).

Цель: исключить:

- нежелательные или необнаруживаемые наложения в памяти;

- узкие места ресурсов в процессе (связанном с безопасностью) выполнения программы.

Описание: в случае применения этого метода динамические переменные и динамические объекты получают определяемые во время выполнения программы определенные и абсолютные адреса в памяти. Объем (размер) распределяемой памяти и ее адреса зависят от состояния системы в момент распределения памяти и не могут быть проверены компилятором или другим автономным инструментом.

Так как число динамических переменных и объектов и существующее свободное пространство памяти для размещения новых динамических переменных или объектов зависит от состояния системы в момент их размещения, то при размещении или при использовании переменных или объектов возможны сбои. Например, если объем свободной памяти, распределяемый системой, недостаточен, то содержимое памяти другой переменной может быть неумышленно стерто. Если динамические переменные или объекты не используются, то появление этих ошибок исключено.

С.2.6.4 Проверка создания динамических переменных или динамических объектов при выполнении программы

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.1).

Цель: убедиться в том, что память, в которой должны быть размещены динамические переменные и объекты, свободна до ее загрузки, а размещение в ней динамических переменных и объектов во время выполнения программы не повлияет на уже существующие в ней переменные, данные или коды.

Описание: в случае применения этих средств к динамическим переменным относят те переменные, которые имеют свои конкретные и абсолютные адреса в памяти, устанавливаемые во время выполнения программы (в этом смысле динамические переменные являются также атрибутами экземпляров объектов).

Аппаратными либо программными средствами память проверяется на то, что она свободна до размещения в ней динамических переменных или объектов (например, для того, чтобы исключить переполнение стека). Если размещение не разрешается (например, если памяти по конкретному адресу недостаточно), должны быть предприняты соответствующие действия. После использования динамических переменных или объектов (например, после выхода из подпрограммы) вся используемая ими память должна быть освобождена.

Примечание - Альтернативным методом является демонстрация статического распределения памяти.

С.2.6.5 Ограниченное использование прерываний

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.1).

Цель: сохранение верифицируемости и тестируемости программного обеспечения.

Описание: использование прерываний должно быть ограничено. Прерывания могут использоваться, если они упрощают систему. Использование программных средств для обработки прерываний должно быть запрещено в критических ситуациях для выполняемых функций (например, критичность по времени, критичность изменений данных). Если прерывания используются, то непрерываемые фрагменты должны иметь специфицированное максимальное время вычисления с тем, чтобы можно было вычислить максимальное время, в течение которого прерывание запрещено. Использование прерываний и их маскирование должны подробно документироваться.

С.2.6.6 Ограниченное использование указателей

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.1).

Цель: исключение проблем, связанных с доступом к данным без предварительной проверки типа и диапазона указателя. Обеспечение модульного тестирования и верификации программных средств. Ограничение последствия отказов.

Описание: в прикладных программных средствах указатель арифметических операций может быть использован на уровне исходного кода только в случае, если тип и диапазон значений указателя данных (для гарантии того, что ссылка указателя находится внутри корректного адресного пространства) будут проверены перед доступом. Связи между задачами в прикладных программах не должны осуществляться с помощью непосредственных ссылок между задачами. Обмен данными должен осуществляться через операционную систему.

С.2.6.7 Ограниченное использование рекурсий

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.1).

Цель: исключение неверифицируемого и нетестируемого использования вызовов подпрограмм.

Описание: если используется рекурсия, то должен быть определен четкий критерий, который делает глубину рекурсии предсказуемой.

С.2.7 Структурное программирование

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица А.4).

Цель: проектирование и реализация программы с использованием практического анализа программы без ее выполнения. Программа может содержать только абсолютный минимум статистически нетестируемого поведения.

Описание: для минимизации структурной сложности программы следует применять следующие принципы:

- разделять программу на подходящие небольшие минимально связанные программные модули, все взаимодействия между которыми точно специфицированы;

- составлять поток управления программными модулями с использованием таких структурированных конструкций, как последовательности, итерации и выбор;

- обеспечивать небольшое число возможных путей через программные модули и возможно более простые отношения между входными и выходными параметрами;

- исключать сложные ветвления и, в частности, безусловные переходы (goto) при использовании языков высокого уровня;

- по возможности, связывать ограничения цикла и ветвление с входными параметрами;

- исключать использование сложных вычислений в ветвлении и цикле.

Свойства языков программирования, которые способствуют указанному выше методу, следует использовать, предпочитая их другим свойствам, которые (как утверждают) более эффективны, за исключением случаев, когда эффективность приобретает абсолютный приоритет (например, некоторые критичные к безопасности системы).

Литература:

Notes on stuctured programming. E. W. Dijkstra, Stuctured Programming, Academic Press, London, 1972, ISBN 0-12-200550-3.

A Discipline of Programming. E. W. Dijkstra. Englewood Cliffs NJ, Prentice-Hall, 1976.

A Software Tool for Top-down Programming. D. С Ince. Software - Practice and Experience, Vol. 13, No. 8, August 1983.

Verification - The Practical Problems. J. T. Webb and D. J. Mannering, SARSS 87, Nov. 1987, Altrincham, England, Elsevier Applied Science, 1987, ISBN 1-85166-167-0.

An Experience in Design and Validation of Software for a Reactor Protection System. S. Bologna, E. de Agostino et al, IFAC Workshop, SAFECOMP, 1979, Stuttgart, 16-18 May 1979, Pergamon Press, 1979.

C.2.8 Ограничение доступа/инкапсуляция информации

Примечание - Ссылка на данный метод/средство приведена в МЭК 61508-3 (таблица В.9).

Цель: предотвращение непреднамеренного доступа к данным или процедурам и обеспечение тем самым качественной структуры программных средств.

Описание: общедоступные для всех программных компонентов данные могут быть случайно или некорректно модифицированы любым из этих компонентов. Любые изменения этих структур данных могут потребовать подробной проверки программного кода и серьезных исправлений.

Ограничение доступа представляет собой общий метод к минимизации указанных выше проблем. Ключевые структуры данных «скрыты», и с ними можно работать только через конкретный набор процедур доступа, это позволяет модифицировать внутренние структуры данных или добавлять новые процедуры и при этом не оказывать влияния на функциональное поведение остальных программных средств. Например, имя директории может иметь процедуры доступа «вставить», «удалить» и «найти». Процедуры доступа и структуры внутренних данных могут быть изменены (например, при использовании различных методов просмотра или запоминании имен на жестком диске), не оказывая влияния на логическое поведение остальных программных средств, использующих эти процедуры.