Обоснование заявленных свойств — различия между версиями
Admin (обсуждение | вклад) |
Admin (обсуждение | вклад) м |
||
| (не показаны 4 промежуточные версии этого же участника) | |||
| Строка 1: | Строка 1: | ||
| − | '''Обоснование заявленных свойств''' (assurance case). | + | '''Обоснование заявленных свойств''' (assurance case) - создаваемый обоснованный проверяемый артефакт, подтверждающий, что удовлетворяется претензия верхнего уровня (или совокупность претензий), включая поддерживающие претензию систематическую аргументацию и ее явные предположения ([[ISO 15026]]). |
Поскольку обоснования "по традиции" близко к концу жизненного цикла (невзирая на призывы и заклинания вести обоснование с самого начала работы, а не оставлять на последний момент), то все сводится к "доказательству" того, что заявленные свойства системы наличествуют. И доказательство идет по принципу "как в суде" — с общим наименованием подхода как assurance case (с вариантами dependability case, safety case, security case, requirement case, architectural quality case). | Поскольку обоснования "по традиции" близко к концу жизненного цикла (невзирая на призывы и заклинания вести обоснование с самого начала работы, а не оставлять на последний момент), то все сводится к "доказательству" того, что заявленные свойства системы наличествуют. И доказательство идет по принципу "как в суде" — с общим наименованием подхода как 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 в структурированном (более-менее формальном) виде] | * [http://www.asq509.org/ht/action/GetDocumentAction/id/476 Презентация о том, что нужно делать assurance case в структурированном (более-менее формальном) виде] | ||
| − | |||
== GSN == | == GSN == | ||
| − | Нотация GSN (Goal Structuring Notation) | + | Нотация GSN (Goal Structuring Notation) вводит следующие понятия: |
* '''заявление о соответствии''' (Goal), | * '''заявление о соответствии''' (Goal), | ||
* '''тип аргумента''' (Strategy), | * '''тип аргумента''' (Strategy), | ||
| Строка 17: | Строка 16: | ||
GSN сейчас бурно развивается в самых разных направлениях: | GSN сейчас бурно развивается в самых разных направлениях: | ||
| − | * [http:// | + | * [http://ocvs.cfv.jp/tr-data/PS2009-010.pdf автоматизация как построения, так и проверки обоснований]. Тут проводится непосредственное отождествление "обоснования"-assurance case и "доказательства"-proof, затем предлагается задействовать средства диалоговой помощи в обеспечении доказательств. Сначала говорится, что доказательство -- это функциональная программа, а потом функциональной программой объявляется весь assurance case в нотации "похожей на GSN". Заодно делается заявление, что поскольку assurance case пишется на языке программирования, то модель системы тоже может быть сделана в этом языке, что более тесно свяжет систему и доказательство ее соответствия требованиям. |
| − | * [http:// | + | * [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)]. | * 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 == | == CAE == | ||
| Строка 30: | Строка 28: | ||
* [http://www.vtt.fi/inf/pdf/workingpapers/2009/W115.pdf попытка использовать нотацию CAE для представления результатов работы алгоритмов SAT доказательства правильности программ] (пример использования SAT в атомной промышленности). Просто удивительно, что они не пошли по пути "assurance case — это программа" (вероятно потому, что 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) | * [http://www.vtt.fi/inf/pdf/workingpapers/2008/W94.pdf обзор целе-ориентированных методов обоснования безопасности для атомных станций] (с участием Adelard, чтобы был понятен акцент на CAE) | ||
| − | |||
[[Категория:Практики]] | [[Категория:Практики]] | ||
| + | [[Категория:Рабочие продукты]] | ||
Текущая версия на 16:31, 14 ноября 2016
Обоснование заявленных свойств (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)