ГОСТ Р МЭК 60880—2010
Приложение Н
(справочное)
Инструментальные программы
для создания и проверки спецификации,
проектирования и реализации
Инструментальные программы образуют в настоящее время существенную часть среды разработки про
граммного обеспечения, выполняющего функции безопасности. Неавтоматизированные методы связаны с боль
шим риском совершения ошибок и требуют привлечения высококвалифицированного персонала. Поэтому эти
методы нуждаются в инструментальной поддержке с использованием математических методов, раскрывающих
структурные и внутренние функциональные взаимосвязи программного обеспечения и проверяющих внутрен
нюю совместимость, совместимость с некоторой априорной моделью, желательные/нежелательные свойства
ит.п.
Конечное подтверждение соответствия программы своей спецификации гложет осуществляться с помощью
анализатора соответствия. Если проверенный генератор кода обеспечивает полное соответствие исполняемой
программы описанию ев проекта, то статистический и динамический анализы обеспечивают разнообразие про
верки правильности этого описания.
Инструментальные программы для формализированных методов спецификации и проектирования могут
быть классифицированы в качестве конструктивных или аналитических инструментов.
Н.1 Конструктивные инструменты
Конструктивные инструменты используются для поддержки разработки спецификации, проектирования,
кодирования. Они могут включать в себя:
Н.1.1 Текстовый редактор
Поскольку формализованные методы, основанные на теории множеств, на исчислении предикатов и ис
числении высказываний требуют специальных математических символов, то важно иметь соответствующий тек
стовый редактор, способный отображать эти символы на экране с высоким разрешением и четко их распечаты
вать.
Н.1.2 Графический интерфейс
Там. где формализованные методы используют графику, требуются соответствующие графические возмож
ности.
Н.1.3 Автоматический генератор кода
После утверждения формализованной спецификации целостность процесса проектирования гложет быть
существенно улучшена путем применения прошедшего валидацию автоматического генератора кода. Такой гене
ратор кода преобразует спецификацию в исполняемый код. снижая таким образом вероятность внесения оши бок.
Кроме того, посредством выбора генератора кода может быть реализована безопасная сокращенная версия языка.
Для стандартных функций рекомендуется использовать сертифицированные модули программного обес
печения.
Автоматически генерируемый код должен быть читаемым. Комментарии должны способствовать распозна
ванию соответствующих частей спецификации. Структура автоматически генерируемого кода должна способство
вать автоматической верификации.
Н.1.4 Генератор доказательства правильности
Формализованные методы, основанные на логических умозаключениях, требуют использования генерато
ра доказательства правильности, который автоматически регистрирует доказательства правильности, возникаю
щие на этапах проектирования.
Н.2 Аналитические инструменты
Аналитические инструменты позволяют проводить проверку спецификации, проектирования и реализации.
Аналитические инструменты могут включать в себя следующие программы:
Н.2.1 Программа проверки синтаксиса
Программа проверки синтаксиса представляет информацию о структуре программы, по использованию
данных программы, зависимости выходных переменных от входных переменных и управляющей логике про
граммы, что позволяет проводить:
a) определение дефектов структуры, таких как множественный запуск, множественное завершение, недо
стижимый код. избыточный код. отсутствие использования результатов функции;
b
) определение иерархии модулей/подпрограмм;
c) определение нарушений стандартов и соглашений по программированию, включая проверку на наличие
безусловных переходов в циклах;
76