Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем
Предложен метод построения точных абстракций «на лету» и его использование в верификации формальных моделей. Метод основан на том, что каждое пройденное состояние модели характеризуется неполным набором атрибутов, при этом достигается существенное сокращение числа состояний, необходимых для анали...
Збережено в:
| Дата: | 2008 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Russian |
| Опубліковано: |
Інститут проблем штучного інтелекту МОН України та НАН України
2008
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.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 |
nasplib_isofts_kiev_ua-123456789-7132 |
|---|---|
| record_format |
dspace |
| spelling |
Колчин, А.В. 2010-03-24T17:29:46Z 2010-03-24T17:29:46Z 2008 Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем / А.В. Колчин // Штучний інтелект. — 2008. — № 3. — С. 690-705. — Бібліогр.: 30 назв. — рос. 1561-5359 https://nasplib.isofts.kiev.ua/handle/123456789/7132 519.686.2 Предложен метод построения точных абстракций «на лету» и его использование в верификации формальных моделей. Метод основан на том, что каждое пройденное состояние модели характеризуется неполным набором атрибутов, при этом достигается существенное сокращение числа состояний, необходимых для анализа верифицируемой модели. Описаны основные алгоритмы построения абстракций, приведены примеры, иллюстрирующие эффективность применения, а также необходимые расширения для проверки темпоральных свойств. Запропоновано метод побудови точних абстракцій «на льоту» та його використання у верифікації формальних моделей. Метод заснований на тому, що кожний пройдений стан моделі характеризується неповним набором атрибутів, при цьому досягається суттєве скорочення числа станів необхідних для аналізу моделі, що верифікується. Описано основні алгоритми побудови абстракцій, ефективність використання проілюстровано на прикладах. Наведено необхідні розширення для перевірки темпоральних властивостей. 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. ru Інститут проблем штучного інтелекту МОН України та НАН України Архитектура, алгоритмическое и программное обеспечение интеллектуальных многопроцессорных систем Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем Автоматичний метод оперативної побудови абстракцій при верифікації формальних моделей асинхронних систем An Automatic Method for On-The-Fly Abstractions Building During Model Verification of Asynchronous 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 |
2008 |
| language |
Russian |
| publisher |
Інститут проблем штучного інтелекту МОН України та НАН України |
| format |
Article |
| title_alt |
Автоматичний метод оперативної побудови абстракцій при верифікації формальних моделей асинхронних систем An Automatic Method for On-The-Fly Abstractions Building During Model Verification of Asynchronous Systems |
| description |
Предложен метод построения точных абстракций «на лету» и его использование в верификации
формальных моделей. Метод основан на том, что каждое пройденное состояние модели
характеризуется неполным набором атрибутов, при этом достигается существенное сокращение числа
состояний, необходимых для анализа верифицируемой модели. Описаны основные алгоритмы
построения абстракций, приведены примеры, иллюстрирующие эффективность применения, а также
необходимые расширения для проверки темпоральных свойств.
Запропоновано метод побудови точних абстракцій «на льоту» та його використання у верифікації
формальних моделей. Метод заснований на тому, що кожний пройдений стан моделі характеризується
неповним набором атрибутів, при цьому досягається суттєве скорочення числа станів необхідних для
аналізу моделі, що верифікується. Описано основні алгоритми побудови абстракцій, ефективність
використання проілюстровано на прикладах. Наведено необхідні розширення для перевірки темпоральних
властивостей.
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.
|
| issn |
1561-5359 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/7132 |
| citation_txt |
Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем / А.В. Колчин // Штучний інтелект. — 2008. — № 3. — С. 690-705. — Бібліогр.: 30 назв. — рос. |
| work_keys_str_mv |
AT kolčinav avtomatičeskiimetodoperativnogopostroeniâabstrakciipriverifikaciiformalʹnyhmodeleiasinhronnyhsistem AT kolčinav avtomatičniimetodoperativnoípobudoviabstrakcíipriverifíkacííformalʹnihmodeleiasinhronnihsistem AT kolčinav anautomaticmethodforontheflyabstractionsbuildingduringmodelverificationofasynchronoussystems |
| first_indexed |
2025-12-07T16:28:37Z |
| last_indexed |
2025-12-07T16:28:37Z |
| _version_ |
1850867625829072896 |