ГОСТ Р МЭК 60880-2010 Атомные электростанции. Системы контроля и управления, важные для безопасности. Программное обеспечение компьютерных систем, выполняющих функции категории А

Приложение Н
(справочное)

     
Инструментальные программы для создания и проверки спецификации, проектирования и реализации

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

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

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

Н.1 Конструктивные инструменты

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

Н.1.1 Текстовый редактор

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

Н.1.2 Графический интерфейс

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

Н.1.3 Автоматический генератор кода

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

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

Автоматически генерируемый код должен быть читаемым. Комментарии должны способствовать распознаванию соответствующих частей спецификации. Структура автоматически генерируемого кода должна способствовать автоматической верификации.

Н.1.4 Генератор доказательства правильности

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

Н.2 Аналитические инструменты

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

Н.2.1 Программа проверки синтаксиса

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

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

b) определение иерархии модулей/подпрограмм;

c) определение нарушений стандартов и соглашений по программированию, включая проверку на наличие безусловных переходов в циклах;

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

e) проверку информационного потока по спецификации;

f) оказание помощи в проектировании плана динамических испытаний;

g) управление тестовыми данными и, возможно, генерацию тестовых данных.

Н.2.2 Программа семантической проверки