ГОСТ Р ИСО/МЭК 15408-3—2002
фикации. Неоднозначность в этих спецификациях уменьшается с повышением уровня формализации
стиля изложения.
Неформальнуюспецификациюизлагают кактекст на естественном языке. Под естественным язы
ком здесь подразумевается применение выразительных средств общения любого разговорного языка
(например, английского, немецкого, русского, французского). Неформальная спецификация не
под чинена никаким нотационным или специальным ограничениям, отличным от общепринятых
соглаше ний для этого языка (таких, как грамматика исинтаксис). Хотя не применяются никакие
нотационные ограничения, в неформальной спецификации все же требуется привести определения
значений терми нов. использование которых в контексте отличается от общепринятого.
Полуформальнуюспецификацию излагают на языке с ограниченным синтаксисом и обычно сопро
вождают вспомогательным пояснительным (неформальным) текстом. Язык с ограниченным синтакси
сом может быть естественным языком с ограниченной структурой предложения и ключевыми словами
со специальными значениями или же он может быть языком схем (таких, как схемы потоковданных,
переходов, взаимосвязей сущностей, структур данных и процессов или структур программ). В обоих
случаях обязателен набор соглашений, позволяющих определить ограничения, накладываемые на
син таксис.
Формальнуюспецификацию излагают с использованием нотации, основанной на известных мате
матических понятиях, и обычно сопровождают вспомогательным пояснительным (неформальным)
текстом. Эти математические понятия используют, чтобы определить синтаксис и семантику нотации
и правила доказательства, поддерживающие логическую аргументацию. Следует, чтобы синтаксичес
кие и семантические правила, регламентирующие формальную нотацию, определяли, как однозначно
распознавать конструкции и определять их значение. Требуется свидетельство невозможности вывода
противоречий, а все правила, регламентирующие нотацию, необходимо определить или сослался на
них.
Существенное доверие может бытьдостиг»!уто через обеспечение прослеживания ФЬО до каждо
го из его представлений и соответствия модели Г1БО функциональной спецификации. Семейство
ADV RCR содержит требования к отображению соотвегствия между различными
представлениями ФБО. а семейство ADV_SPM —между моделью ИБО и функциональной
спецификацией. Соответ ствие может принять форму либо неформальной или полуформальной
демонстрации, либо формаль ногодоказательства.
Когда требуется неформальная демонстрация соответствия, это означает, что требуется только
соответствие по сути. Методы демонстрации включают, например, использование двумерной таблицы
с входами, обозначающими соответствие, или использование подходящей дзя этого нотации схем
проекта. Могутбыть также использованы указатели и ссылки на другие документы.
Нагуформалышя демонстрациясоответствия требует структурного подхода при анализе соответ
ствия. Следует, чтобы при этом подходе уменьшалась неоднозначность, которая может существовать
при неформальном соответствии, ограничивая интерпретацию применяемых терминов. Могут быть
также использованы указатели и ссылки на другие документы.
Форма
1
ьноедоказательствосоответствия требует, чтобы были использованы известные матема
тические понятия дзя определения синтаксиса и семантики формдзьной нотации и правил доказатель
ства, которые поддерживают логическую аргументацию. Необходимо, чтобы свойства безопасности
могли быть выражены на языке формальной спецификации и было показано, что эти свойства удов
летворяются формдзьной спецификацией. Могут бить также использованы указатели и ссылки на
другие документы.
Элементы ADV_RCR.MC содержат требование, чтобы разработчик представил свидетельство
для каждой смежной пары предстаазений ФБО, что все относящиеся к безопасности функцнондзьные
возможности более абстрактного представления ФБО уточнены в менее абстрактном представлении
ФБО. Каждый из элементовADV_FSP.*.2E. ADV HLD/.2E, ADV_LLD.*.2E и ADV_IMP.*.2E содер
жит требование, чтобы оценщик сделдз заключение о том, что ФБО, предстаазяемые этим семей
ством требований, —точное и полное отображение функциональныхтребований безопасности ОО.
Чтобы сделать заключение, что представление ФБО является точным и полным отображением функ
циональных требований безопасности ОО. предполагается, что оценщик использует свидетельство,
предоставленное разработчиком в ADV RCR.MC, как основание дзя этого заключения. Устанавливая
соответствие между функииондзьнымн требованиями безопасности ОО и каждым из цепочки после
довательных представлений ФБО. этот пошаговый процесс предоставит, в конечном счете, более
1
• -
2
-
1451
49