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

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

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

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

• Презентация о том, что нужно делать assurance case в структурированном (более-менее формальном) виде

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)

Ссылки:

• эта же нотация (CAE) воспроизведена в виде стереотипов UML в книжка, а про QUASAR http://www.sei.cmu.edu/reports/06hb001.pdf книжке по MFESA при рассмотрении architectural quality case с использованием метода QUASAR
• предварительное моделирование трех стандартов разработки софта в CAE, для того, чтобы структурировать построение доказательства им соответствия (сначала делается шаблон дерева “заявлений соответствия” стандарту, чтобы потом подставить туда аргументы и факты для конкретного проекта)
• попытка использовать нотацию CAE для представления результатов работы алгоритмов SAT доказательства правильности программ (пример использования SAT в атомной промышленности). Просто удивительно, что они не пошли по пути “assurance case — это программа” (вероятно потому, что CAE слишком простая нотация).
• обзор целе-ориентированных методов обоснования безопасности для атомных станций (с участием Adelard, чтобы был понятен акцент на CAE)