Просмотр исходного текста страницы Обоснование заявленных свойств

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

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

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

* [http://www.asq509.org/ht/action/GetDocumentAction/id/476 Презентация о том, что нужно делать assurance case в структурированном (более-менее формальном) виде]

== GSN ==
Нотация GSN (Goal Structuring Notation) вводит следующие понятия:
* '''заявление о соответствии''' (Goal),
* '''тип аргумента''' (Strategy),
* '''очевидный факт''' (Solution).

Понятно, что выбор терминологии связан с акцентом на интенсиональность, а не на собственно "обоснование". Обширная литература может быть найдена [http://www.origin-consulting.com/gsnclub/pubs.php тут], но это только самые основные работы. Обратите внимание, что на авторов существенное влияние оказали работы по языкам [[Паттерны|паттернов]] (pattern languages).

GSN сейчас бурно развивается в самых разных направлениях:
* [http://ocvs.cfv.jp/tr-data/PS2009-010.pdf автоматизация как построения, так и проверки обоснований]. Тут проводится непосредственное отождествление "обоснования"-assurance case и "доказательства"-proof, затем предлагается задействовать средства диалоговой помощи в обеспечении доказательств. Сначала говорится, что доказательство -- это функциональная программа, а потом функциональной программой объявляется весь assurance case в нотации "похожей на GSN". Заодно делается заявление, что поскольку assurance case пишется на языке программирования, то модель системы тоже может быть сделана в этом языке, что более тесно свяжет систему и доказательство ее соответствия требованиям. 
* [http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.408.7951&rep=rep1&type=pdf текстовые (не графические) языки] для тех же целей "наилучшего выражения аргументации" (аж пять штук — от обычной прозы через аутлайн к LISP-подобной).
* security assurance case (как ни странно, этому направлению всего несколько лет), подробнейшие обзоры [https://buildsecurityin.us-cert.gov/bsi/articles/knowledge/assurance/643-BSI.html (1)] и [https://buildsecurityin.us-cert.gov/bsi/articles/knowledge/assurance/973-BSI.html (2)].

== CAE ==
Claims-Arguments-Evidence (CAE) — сверхупрощенный (безо всякой "интенсиональности", тупо "презентация логики доказательства") вариант того же самого, нотация также известна под именем [http://www.adelard.com/web/hnav/ASCE/choosing-asce/cae.html ASCAD] (Adelard Safety Claims Arguments Data)

Ссылки:
* эта же нотация (CAE) воспроизведена в виде стереотипов UML в [http://www.freebookspot.in/Books-Method%20Framework%20for%20Engineering%20System%20Architectures.htm книжка, а про QUASAR http://www.sei.cmu.edu/reports/06hb001.pdf книжке по MFESA] при рассмотрении architectural quality case с использованием метода QUASAR
* [http://www.acq.osd.mil/sse/docs/2010-01-19-Structured-Assurance-Cases-Ankrum-Kromholz.pdf предварительное моделирование трех стандартов разработки софта в CAE], для того, чтобы структурировать построение доказательства им соответствия (сначала делается шаблон дерева "заявлений соответствия" стандарту, чтобы потом подставить туда аргументы и факты для конкретного проекта)
* [http://www.vtt.fi/inf/pdf/workingpapers/2009/W115.pdf попытка использовать нотацию CAE для представления результатов работы алгоритмов SAT доказательства правильности программ] (пример использования SAT в атомной промышленности). Просто удивительно, что они не пошли по пути "assurance case — это программа" (вероятно потому, что CAE слишком простая нотация).
* [http://www.vtt.fi/inf/pdf/workingpapers/2008/W94.pdf обзор целе-ориентированных методов обоснования безопасности для атомных станций] (с участием Adelard, чтобы был понятен акцент на CAE)

[[Категория:Практики]]
[[Категория:Рабочие продукты]]