ГОСТ Р ИСО/МЭК 15408-3-2013
создании экземпляра реализации формальной системы для спецификации ОО и доказательств
соответствия.
Формальный стиль изложения поддерживает математические доказательства свойств
безопасности на основе функциональных возможностей безопасности, согласованность уточнений и
соответствие представлений. Поддержка формальных средств является адекватной тогда, когда
сделанные вручную, неформальным способом выводы были бы излишне длинными и недостаточно
ясными. Применение формальных средств также способно уменьшить вероятность ошибок, присущих
выводам, сделанным неформальным образом.
Примеры формальных систем:
Язык спецификаций Z весьма выразителен и поддерживает множество различных методов и
стилей формальнойспецификации.Zприменяетсяпреимущественно дляспецификаций,
ориентированных на модели с использованием схем формально специфицированных операций. Для
получения дополнительной информации см. ссылку
http://vl.zus6r.org/.
ALC2 является формальной системой с открытым исходным кодом, состоящей из языка
спецификаций, основанного на языке обработки списков Лисп (LISP), и инструмента доказательства
теорем. Более подробная информация на сайте:
http://www.cs.utexas.edu/users/moore/acl2.
Isabelle - популярная среда доказательства общих теорем, которая позволяет выражать
математические формулы на формальном языке и предоставляет средства для доказательства этих
формулврамкахлогическоговычисления(см.,например.
http://www.cl.cam.ac.uk/Research/HVG/lsabelle/для
получения дополнительной информации).
Метод В является формальной системой, основанной на пропозициональном исчислении
(исчислении высказываний), вычислении предикатов первого порядка с правилами построения
выводов и установленной теоретической базой (см., например.
http://v1.fmnet.info/b/
для получения
дополнительной информации).
246