Оптимизация проверки выполнимости переходов при верификации формальных моделей
При проверке динамических свойств формальных моделей программ, в которых последовательность выполнения операторов выражена неявно, существенную часть операционного времени верификаторы тратят на анализ выполнимости переходов. В работе предложен метод повышения производительности проверки моделей, су...
Збережено в:
| Опубліковано в: : | Проблеми програмування |
|---|---|
| Дата: | 2012 |
| Автор: | |
| Мова: | Russian |
| Опубліковано: |
Інститут програмних систем НАН України
2012
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/86604 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Оптимизация проверки выполнимости переходов при верификации формальных моделей / А.В. Колчин // Проблеми програмування. — 2012. — № 2-3. — С. 201-210. — Бібліогр.: 10 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-86604 |
|---|---|
| record_format |
dspace |
| spelling |
Колчин, А.В. 2015-09-23T16:17:04Z 2015-09-23T16:17:04Z 2012 Оптимизация проверки выполнимости переходов при верификации формальных моделей / А.В. Колчин // Проблеми програмування. — 2012. — № 2-3. — С. 201-210. — Бібліогр.: 10 назв. — рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/86604 519.686.2 При проверке динамических свойств формальных моделей программ, в которых последовательность выполнения операторов выражена неявно, существенную часть операционного времени верификаторы тратят на анализ выполнимости переходов. В работе предложен метод повышения производительности проверки моделей, суть которого заключается в локализации причины невыполнимости перехода в некотором состоянии и ее использовании для анализа выполнимости в последующих состояниях. Transitions feasibility analysis becomes a significant part of operation time of verification tools for formal models of programs, which control flow is expressed implicitly. This paper describes a new method of model checking performance improvement. The main idea is a localization of a transition’s unsatisfiability reason in some state and it’s usage for the satisfiability analysis in subsequent states. ru Інститут програмних систем НАН України Проблеми програмування Формальні методи програмування Оптимизация проверки выполнимости переходов при верификации формальных моделей 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 |
2012 |
| language |
Russian |
| container_title |
Проблеми програмування |
| publisher |
Інститут програмних систем НАН України |
| description |
При проверке динамических свойств формальных моделей программ, в которых последовательность выполнения операторов выражена неявно, существенную часть операционного времени верификаторы тратят на анализ выполнимости переходов. В работе предложен метод повышения производительности проверки моделей, суть которого заключается в локализации причины невыполнимости перехода в некотором состоянии и ее использовании для анализа выполнимости в последующих состояниях.
Transitions feasibility analysis becomes a significant part of operation time of verification tools for formal models of programs, which control flow is expressed implicitly. This paper describes a new method of model checking performance improvement. The main idea is a localization of a transition’s unsatisfiability reason in some state and it’s usage for the satisfiability analysis in subsequent states.
|
| issn |
1727-4907 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/86604 |
| citation_txt |
Оптимизация проверки выполнимости переходов при верификации формальных моделей / А.В. Колчин // Проблеми програмування. — 2012. — № 2-3. — С. 201-210. — Бібліогр.: 10 назв. — рос. |
| work_keys_str_mv |
AT kolčinav optimizaciâproverkivypolnimostiperehodovpriverifikaciiformalʹnyhmodelei |
| first_indexed |
2025-12-01T17:52:58Z |
| last_indexed |
2025-12-01T17:52:58Z |
| _version_ |
1850860740009787392 |