Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем

В основе предложенного метода лежит алгоритм отсечения избыточных по отношению к проверяемым свойствам ветвей поведения формальной модели. Факт избыточности устанавливается на основании доказательства изоморфизма на графе информационных зависимостей модели. Во многих случаях такой подход существе...

Full description

Saved in:
Bibliographic Details
Published in:Искусственный интеллект
Date:2013
Main Author: Колчин, А.В.
Format: Article
Language:Russian
Published: Інститут проблем штучного інтелекту МОН України та НАН України 2013
Subjects:
Online Access:https://nasplib.isofts.kiev.ua/handle/123456789/85153
Tags: Add Tag
No Tags, Be the first to tag this record!
Journal Title:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Cite this:Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем / А.В. Колчин // Искусственный интеллект. — 2013. — № 4. — С. 113–126. — Бібліогр.: 19 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id nasplib_isofts_kiev_ua-123456789-85153
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
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
title Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем
spellingShingle Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем
Колчин, А.В.
Алгоритмическое и программное обеспечение параллельных вычислительных интеллектуальных систем
title_short Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем
title_full Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем
title_fullStr Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем
title_full_unstemmed Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем
title_sort метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем
author Колчин, А.В.
author_facet Колчин, А.В.
topic Алгоритмическое и программное обеспечение параллельных вычислительных интеллектуальных систем
topic_facet Алгоритмическое и программное обеспечение параллельных вычислительных интеллектуальных систем
publishDate 2013
language Russian
container_title Искусственный интеллект
publisher Інститут проблем штучного інтелекту МОН України та НАН України
format Article
title_alt Метод редукції простору поведінки, що аналізується, при верифікації формальних моделей розподілених програмних систем
A method for reduction of analyzed behavior space during verification of formal models of distributed software systems
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.
issn 1561-5359
url https://nasplib.isofts.kiev.ua/handle/123456789/85153
fulltext
citation_txt Метод редукции анализируемого пространства поведения при верификации формальных моделей распределенных программных систем / А.В. Колчин // Искусственный интеллект. — 2013. — № 4. — С. 113–126. — Бібліогр.: 19 назв. — рос.
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
first_indexed 2025-11-26T11:39:04Z
last_indexed 2025-11-26T11:39:04Z
_version_ 1850621970126733312