ГОСТ Р МЭК 61508-7—2012
С.2.4.9 Z
Цель. Z — это нотация языка спецификаций для последовательных систем и метод проектирования, позво
ляющий разработчику выполнять работу, начиная со спецификации на языке Z до исполнительных алгоритмов,
обеспечивая при этом доказательство их корректности по отношению к спецификации.
Язык Z в принципе используется на этапе спецификации, однако данный язык был разработан для исполь
зования от этапа составления спецификации до проектирования и реализации систем. Более всего он подходит
для разработки последовательных систем, ориентированных на данные.
Описание. Как и в VDM. в реализованном в языке Z методе спецификации состояние системы моделируется
в терминах теоретико-множественных структур, в которых описаны инварианты (используя предикаты), а операции
над этими состояниями моделируются путем определения их пред- и постусловий в терминах системных состоя
ний. Операции допускается проверять на сохранение системных инвариантов для демонстрации их согласован
ности. Формальная часть спецификации подразделяется на схемы, которые обеспечивают возможность структури
рования спецификаций путем их усовершенствования.
Обычно спецификация Z представляет собой сочетание формального текста на языке Z и неформального
пояснительного текста на естественном языке. Формальный текст сам по себе гложет оказаться слишком сжатым
для простого восприятия и часто его смысл необходимо пояснять, тогда как неформальный, естественный язык
может оказаться неоднозначным и неточным.
В отличие or VDM язык Z представляет собой скорее нотацию, чем завершенный метод. Однако был раз
работан близкий метод (метсд В), который может быть использован в сочетании с языком Z. Метод В основан на
принципе пошагового уточнения.
Литература:
Formal Specification using Z. 2nd Edition. D. Lightfoot. Palgrave Macmillan. 2000. ISBN 9780333763278.
The В-Method. S. Schneider. Palgrave Macmillan. 2001, ISBN 9780333792841.
C.2.5 Программирование с защитой
П р и м е ч а н и е — Ссыпка на данный метод/средство приведена в МЭК 61508-3 (таблица А.4).
Цель. Создание программ, выявляющих во время их исполнения аномальные потоки управления, данных
или значения данных и реагирующих на них заранее определенным и приемлемым способом.
Описание. В процессе разработки программ допускается использовать разные методы для проверки анома
лий в потоках управления или данных. Эти методы могут применяться систематически в процессе программирова
ния системы для снижения вероятности ошибочной обработки данных.
Существуют два пересекающихся множества методов защиты. Внутренние методы защиты от ошибок про
ектируются в программном обеспечении для преодоления недостатков в процессе создания этих программных
средств. Эти недостатки могут быть обусловлены сшибками при проектировании или кодировании либо ошибоч
ными требованиями. Ниже перечислены некоторые из рекомендаций по защите:
- проверка диапазона значений переменных;
- проверка значений переменных на их достоверность (если возможно);
- проверка типа, размерности и диапазона значений параметров процедур на входе процедур.
Представленные три рекомендации помогают гарантировать допустимость значений, обрабатываемых
в программах, как с точки зрения терминов программных функций, так и физических значений переменных.
Параметры «только для чтения» и параметры «для чтения-записи» должны быть разделены, и доступ к ним
должен проверяться. Программные функции должны рассматривать все параметры в качестве параметров «толь
кодля чтения». Символьные константы недолжны бытьдоступны для записи. Это помогает обнаруживать случай
ные перезаписи или ошибочное использование переменных.
Устойчивое к ошибкам программное обеспечение проектируется в «предположении», что ошибки существу
ют в его собственном окружении либо используются выходящие за номиналы значения или предполагаемые усло
вия. но программное обеспечение ведет себя заранее определенным способом. В этом случае применяют следу
ющие проверки:
- проверку на достоверность физических значений входных и промежуточных переменных:
- проверку влияния выходных переменных, предпочтительно путем прямого наблюдения соответствующих
изменений состояния системы:
- проверку самим программным обеспечением своей конфигурации, включая наличие и доступность пред
полагаемых аппаратных средств, а также завершенность самого программного обеспечения, что особенно важно
для поддержки полноты в процессе его эксплуатации.
Некоторые из методов защиты программ, например, проверки последовательности потока управления, так
же справляются и с внешними отказами.
Литература:
Software Engineering for Real-time Systems. J.E. Cooling. Pearson Education. 2003, ISBN 0201596202.
9780201596205.
DependabilityofCritical ComputerSystems: Guidelines Produced bythe European Workshop on Industrial Computer
Systems. Technical Committee 7 (EWICS TC7, Systems Reliability. Safety, and Security). Elsevier Applied Science. 1989.
ISBN 1851663819. 9781851663811.
39