А.5 Дополнительный материал по формальным методам

Формальные методы дают математическое представление о ФБО и их работе, что требуется в компонентах ADV_FSP.6 "Полная полуформальная функциональная спецификация с дополнительной формальной спецификацией", ADV_SPM.1 "Формальная модель политики безопасности ОО" и ADV_TDS.6 "Полный полуформальный модульный проект с формальным высокоуровневым представлением". Есть два аспекта формальных методов: язык спецификации, который используется для формального выражения, и средства доказательства теорем, которые математически доказывают полноту и правильность формальной спецификации.

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

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

- Семантика, синтаксис и правила логического вывода формальной системы определяются или их определение дается в ссылках.

- Каждая формальная система сопровождается пояснительным текстом, который содержит определенную семантику, так, что:

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

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

3) формальная система способна выразить правила и характеристики соответствующих ПФБ, функциональные возможности по безопасности и интерфейсы (с указанием подробных результатов, исключений и сообщений об ошибках) ФБО, их подсистем или модулей, которые должны быть определены для семейства доверия, для которого используется система обозначений;

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

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

- Каждая формальная система устанавливает правила доказательства, которые

5) поддерживают логическое доказательство хорошо известных математических понятий,

6) помогают предотвратить возникновение противоречий.

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

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

Примеры формальных систем:

Язык спецификаций Z весьма выразителен, и поддерживает множество различных методов и стилей формальной спецификации. Z применяется преимущественно для модели ориентированной спецификации, используя схемы для формального определения операций. Смотрите http://vl.zuser.org/ для получения дополнительной информации.

ALC2 является открытым исходным кодом формальной системы, состоящей из LISP-ориентированного языка спецификаций и средств доказательства теорем. Смотрите http://www.cs.utexas.edu/users/moore/acl2 для получения дополнительной информации.

Isabelle является широко распространеннойобщей средойдоказательства теорем, которая позволяет выразить математическую формулу на формальном языке и предоставляет инструментальные средства для доказательства этих формул в рамках логического вычисления (См., например http://www.cl.cam.ac.uk/Research/HVG/Isabelle/ для получения дополнительной информации).

Метод В является формальной системой, основанной на вычислении высказываний, вычислении предикатов первого порядка с правилами вывода и теории множеств (см., например http://vl.fmnet.info/b/ для получения дополнительной информации).

Приложение B
(справочное)
Композиция (ACO)

Это приложение служит для объяснения принципов, поддерживающих оценку композиции, и критериев класса ACO. В данном приложении нет определения критериев класса ASE; это определение приводится в разделе 10.

Дата добавления: 2014-01-15