Обоснование заявленных свойств

Обоснование заявленных свойств (assurance case) - создаваемый обоснованный проверяемый артефакт, подтверждающий, что удовлетворяется претензия верхнего уровня (или совокупность претензий), включая поддерживающие претензию систематическую аргументацию и ее явные предположения (ISO 15026).

Поскольку обоснования "по традиции" близко к концу жизненного цикла (невзирая на призывы и заклинания вести обоснование с самого начала работы, а не оставлять на последний момент), то все сводится к "доказательству" того, что заявленные свойства системы наличествуют. И доказательство идет по принципу "как в суде" — с общим наименованием подхода как assurance case (с вариантами dependability case, safety case, security case, requirement case, architectural quality case).

Требование обоснований заложено в ISO 15026, идущий в пару к ISO 15288.

GSN

Нотация GSN (Goal Structuring Notation) вводит следующие понятия:

  • заявление о соответствии (Goal),
  • тип аргумента (Strategy),
  • очевидный факт (Solution).

Понятно, что выбор терминологии связан с акцентом на интенсиональность, а не на собственно "обоснование". Обширная литература может быть найдена тут, но это только самые основные работы. Обратите внимание, что на авторов существенное влияние оказали работы по языкам паттернов (pattern languages).

GSN сейчас бурно развивается в самых разных направлениях:

  • автоматизация как построения, так и проверки обоснований. Тут проводится непосредственное отождествление "обоснования"-assurance case и "доказательства"-proof, затем предлагается задействовать средства диалоговой помощи в обеспечении доказательств. Сначала говорится, что доказательство -- это функциональная программа, а потом функциональной программой объявляется весь assurance case в нотации "похожей на GSN". Заодно делается заявление, что поскольку assurance case пишется на языке программирования, то модель системы тоже может быть сделана в этом языке, что более тесно свяжет систему и доказательство ее соответствия требованиям.
  • текстовые (не графические) языки для тех же целей "наилучшего выражения аргументации" (аж пять штук — от обычной прозы через аутлайн к LISP-подобной).
  • security assurance case (как ни странно, этому направлению всего несколько лет), подробнейшие обзоры (1) и (2).

CAE

Claims-Arguments-Evidence (CAE) — сверхупрощенный (безо всякой "интенсиональности", тупо "презентация логики доказательства") вариант того же самого, нотация также известна под именем ASCAD (Adelard Safety Claims Arguments Data)

Ссылки: