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

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

Ausführliche Beschreibung

Gespeichert in:
Bibliographische Detailangaben
Veröffentlicht in:Проблеми програмування
Datum:2012
1. Verfasser: Колчин, А.В.
Sprache:Russisch
Veröffentlicht: Інститут програмних систем НАН України 2012
Schlagworte:
Online Zugang:https://nasplib.isofts.kiev.ua/handle/123456789/86604
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:Digital Library of Periodicals of National Academy of Sciences of Ukraine
Zitieren:Оптимизация проверки выполнимости переходов при верификации формальных моделей / А.В. Колчин // Проблеми програмування. — 2012. — № 2-3. — С. 201-210. — Бібліогр.: 10 назв. — рос.

Institution

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