Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем
В основе предложенного метода лежит алгоритм отсечения избыточных по отношению к проверяемым
 свойствам ветвей поведения формальной модели. Факт избыточности устанавливается на основании
 доказательства изоморфизма на графе информационных зависимостей модели. Во многих случаях такой&...
Збережено в:
| Опубліковано в: : | Искусственный интеллект |
|---|---|
| Дата: | 2013 |
| Автор: | |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Інститут проблем штучного інтелекту МОН України та НАН України
2013
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/85153 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем / А.В. Колчин // Искусственный интеллект. — 2013. — № 4. — С. 113–126. — Бібліогр.: 19 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1862575065251446784 |
|---|---|
| author | Колчин, А.В. |
| author_facet | Колчин, А.В. |
| citation_txt | Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем / А.В. Колчин // Искусственный интеллект. — 2013. — № 4. — С. 113–126. — Бібліогр.: 19 назв. — рос. |
| collection | DSpace DC |
| container_title | Искусственный интеллект |
| description | В основе предложенного метода лежит алгоритм отсечения избыточных по отношению к проверяемым
свойствам ветвей поведения формальной модели. Факт избыточности устанавливается на основании
доказательства изоморфизма на графе информационных зависимостей модели. Во многих случаях такой
подход существенно сокращает эффект «комбинаторного взрыва» количества состояний.
В основі запропонованого методу лежить алгоритм відсікання надлишкових по відношенню до
властивостей, що перевіряються, гілок поведінки формальної моделі. Факт надмірності встановлюється
на підставі доказу ізоморфізму на графі інформаційних залежностей моделі. В багатьох випадках
такий підхід істотно зменшує ефект «комбінаторного вибуху» кількості станів.
The core of the proposed method is an algorithm for cutting of formal model behavior branches, which are redundant
with respect to verified properties. The fact of redundancy is derived basing on proof of isomorphism on the
model’s informational dependency graph. In many cases, such approach significantly reduces «state space
combinatorial explosion» effect.
|
| first_indexed | 2025-11-26T11:39:04Z |
| format | Article |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-85153 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1561-5359 |
| language | Russian |
| last_indexed | 2025-11-26T11:39:04Z |
| publishDate | 2013 |
| publisher | Інститут проблем штучного інтелекту МОН України та НАН України |
| record_format | dspace |
| spelling | Колчин, А.В. 2015-07-19T19:18:27Z 2015-07-19T19:18:27Z 2013 Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем / А.В. Колчин // Искусственный интеллект. — 2013. — № 4. — С. 113–126. — Бібліогр.: 19 назв. — рос. 1561-5359 https://nasplib.isofts.kiev.ua/handle/123456789/85153 004.832.23+004.942 В основе предложенного метода лежит алгоритм отсечения избыточных по отношению к проверяемым
 свойствам ветвей поведения формальной модели. Факт избыточности устанавливается на основании
 доказательства изоморфизма на графе информационных зависимостей модели. Во многих случаях такой
 подход существенно сокращает эффект «комбинаторного взрыва» количества состояний. В основі запропонованого методу лежить алгоритм відсікання надлишкових по відношенню до
 властивостей, що перевіряються, гілок поведінки формальної моделі. Факт надмірності встановлюється
 на підставі доказу ізоморфізму на графі інформаційних залежностей моделі. В багатьох випадках
 такий підхід істотно зменшує ефект «комбінаторного вибуху» кількості станів. The core of the proposed method is an algorithm for cutting of formal model behavior branches, which are redundant
 with respect to verified properties. The fact of redundancy is derived basing on proof of isomorphism on the
 model’s informational dependency graph. In many cases, such approach significantly reduces «state space
 combinatorial explosion» effect. ru Інститут проблем штучного інтелекту МОН України та НАН України Искусственный интеллект Алгоритмическое и программное обеспечение параллельных вычислительных интеллектуальных систем Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем Метод редукції простору поведінки, що аналізується, при верифікації формальних моделей розподілених програмних систем A method for reduction of analyzed behavior space during verification of formal models of distributed software systems Article published earlier |
| spellingShingle | Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем Колчин, А.В. Алгоритмическое и программное обеспечение параллельных вычислительных интеллектуальных систем |
| title | Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем |
| title_alt | Метод редукції простору поведінки, що аналізується, при верифікації формальних моделей розподілених програмних систем A method for reduction of analyzed behavior space during verification of formal models of distributed software systems |
| title_full | Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем |
| title_fullStr | Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем |
| title_full_unstemmed | Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем |
| title_short | Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем |
| title_sort | метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем |
| topic | Алгоритмическое и программное обеспечение параллельных вычислительных интеллектуальных систем |
| topic_facet | Алгоритмическое и программное обеспечение параллельных вычислительных интеллектуальных систем |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/85153 |
| work_keys_str_mv | AT kolčinav metodredukciianaliziruemogoprostranstvapovedeniâpriverifikaciiformalʹnyhmodeleiraspredelennyhprogrammnyhsistem AT kolčinav metodredukcííprostorupovedínkiŝoanalízuêtʹsâpriverifíkacííformalʹnihmodeleirozpodílenihprogramnihsistem AT kolčinav amethodforreductionofanalyzedbehaviorspaceduringverificationofformalmodelsofdistributedsoftwaresystems |