Обоснование заявленных свойств — различия между версиями

Версия 20:49, 29 ноября 2015

Обоснование заявленных свойств (assurance case).

Поскольку обоснования "по традиции" близко к концу жизненного цикла (невзирая на призывы и заклинания вести обоснование с самого начала работы, а не оставлять на последний момент), то все сводится к "доказательству" того, что заявленные свойства системы наличествуют. И доказательство идет по принципу "как в суде" — с общим наименованием подхода как 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)