Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем

Предложен метод построения точных абстракций «на лету» и его использование в верификации формальных моделей. Метод основан на том, что каждое пройденное состояние модели характеризуется неполным набором атрибутов, при этом достигается существенное сокращение числа состояний, необходимых для анали...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2008
Автор: Колчин, А.В.
Формат: Стаття
Мова:Russian
Опубліковано: Інститут проблем штучного інтелекту МОН України та НАН України 2008
Теми:
Онлайн доступ:http://dspace.nbuv.gov.ua/handle/123456789/7132
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем / А.В. Колчин // Штучний інтелект. — 2008. — № 3. — С. 690-705. — Бібліогр.: 30 назв. — рос.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine
id irk-123456789-7132
record_format dspace
spelling irk-123456789-71322010-03-25T12:00:58Z Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем Колчин, А.В. Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем Предложен метод построения точных абстракций «на лету» и его использование в верификации формальных моделей. Метод основан на том, что каждое пройденное состояние модели характеризуется неполным набором атрибутов, при этом достигается существенное сокращение числа состояний, необходимых для анализа верифицируемой модели. Описаны основные алгоритмы построения абстракций, приведены примеры, иллюстрирующие эффективность применения, а также необходимые расширения для проверки темпоральных свойств. Запропоновано метод побудови точних абстракцій «на льоту» та його використання у верифікації формальних моделей. Метод заснований на тому, що кожний пройдений стан моделі характеризується неповним набором атрибутів, при цьому досягається суттєве скорочення числа станів необхідних для аналізу моделі, що верифікується. Описано основні алгоритми побудови абстракцій, ефективність використання проілюстровано на прикладах. Наведено необхідні розширення для перевірки темпоральних властивостей. A method for “on-the-fly” exact abstraction construction for model checking is proposed. The basis of the method is storing of incomplete set of attributes in visited states. Due to this fact the number of needed for model analysis states is substantially smaller. The main algorithms for abstractions building are described. Effectiveness of the method applying is demonstrated with examples. Enhancements needed for temporal properties verification are described. 2008 Article Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем / А.В. Колчин // Штучний інтелект. — 2008. — № 3. — С. 690-705. — Бібліогр.: 30 назв. — рос. 1561-5359 http://dspace.nbuv.gov.ua/handle/123456789/7132 519.686.2 ru Інститут проблем штучного інтелекту МОН України та НАН України
institution Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection DSpace DC
language Russian
topic Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем
Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем
spellingShingle Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем
Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем
Колчин, А.В.
Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем
description Предложен метод построения точных абстракций «на лету» и его использование в верификации формальных моделей. Метод основан на том, что каждое пройденное состояние модели характеризуется неполным набором атрибутов, при этом достигается существенное сокращение числа состояний, необходимых для анализа верифицируемой модели. Описаны основные алгоритмы построения абстракций, приведены примеры, иллюстрирующие эффективность применения, а также необходимые расширения для проверки темпоральных свойств.
format Article
author Колчин, А.В.
author_facet Колчин, А.В.
author_sort Колчин, А.В.
title Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем
title_short Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем
title_full Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем
title_fullStr Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем
title_full_unstemmed Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем
title_sort автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем
publisher Інститут проблем штучного інтелекту МОН України та НАН України
publishDate 2008
topic_facet Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем
url http://dspace.nbuv.gov.ua/handle/123456789/7132
citation_txt Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем / А.В. Колчин // Штучний інтелект. — 2008. — № 3. — С. 690-705. — Бібліогр.: 30 назв. — рос.
work_keys_str_mv AT kolčinav avtomatičeskijmetodoperativnogopostroeniâabstrakcijpriverifikaciiformalʹnyhmodelejasinhronnyhsistem
first_indexed 2023-10-18T16:36:47Z
last_indexed 2023-10-18T16:36:47Z
_version_ 1796139439128313856