Оптимизация проверки выполнимости переходов при верификации формальных моделей
При проверке динамических свойств формальных моделей программ, в которых последовательность выполнения операторов выражена неявно, существенную часть операционного времени верификаторы тратят на анализ выполнимости переходов. В работе предложен метод повышения производительности проверки моделей, су...
Збережено в:
| Опубліковано в: : | Проблеми програмування |
|---|---|
| Дата: | 2012 |
| Автор: | |
| Мова: | Російська |
| Опубліковано: |
Інститут програмних систем НАН України
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| _version_ | 1862650752333250560 |
|---|---|
| author | Колчин, А.В. |
| author_facet | Колчин, А.В. |
| citation_txt | Оптимизация проверки выполнимости переходов при верификации формальных моделей / А.В. Колчин // Проблеми програмування. — 2012. — № 2-3. — С. 201-210. — Бібліогр.: 10 назв. — рос. |
| collection | DSpace DC |
| container_title | Проблеми програмування |
| 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.
|
| first_indexed | 2025-12-01T17:52:58Z |
| fulltext | |
| id | nasplib_isofts_kiev_ua-123456789-86604 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1727-4907 |
| language | Russian |
| last_indexed | 2025-12-01T17:52:58Z |
| publishDate | 2012 |
| publisher | Інститут програмних систем НАН України |
| 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 |
| spellingShingle | Оптимизация проверки выполнимости переходов при верификации формальных моделей Колчин, А.В. Формальні методи програмування |
| title | Оптимизация проверки выполнимости переходов при верификации формальных моделей |
| title_full | Оптимизация проверки выполнимости переходов при верификации формальных моделей |
| title_fullStr | Оптимизация проверки выполнимости переходов при верификации формальных моделей |
| title_full_unstemmed | Оптимизация проверки выполнимости переходов при верификации формальных моделей |
| title_short | Оптимизация проверки выполнимости переходов при верификации формальных моделей |
| title_sort | оптимизация проверки выполнимости переходов при верификации формальных моделей |
| topic | Формальні методи програмування |
| topic_facet | Формальні методи програмування |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/86604 |
| work_keys_str_mv | AT kolčinav optimizaciâproverkivypolnimostiperehodovpriverifikaciiformalʹnyhmodelei |