Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами
В работе рассмотрены методы прямого и обратного символьного моделирования, используемые для решения задач верификации систем базовых протоколов. Помимо алгоритмов поиска в пространстве состояний системы, детально проработанных в области проверки на модели (model checking), основная задача символьног...
Saved in:
| Date: | 2008 |
|---|---|
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Інститут програмних систем НАН України
2008
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/2600 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами / С.В. Потиенко // Проблеми програмування. — 2008. — № 4. — С. 39-44. — Бібліогр.: 8 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| id |
nasplib_isofts_kiev_ua-123456789-2600 |
|---|---|
| record_format |
dspace |
| spelling |
Потиенко, С.В. 2008-12-15T13:20:57Z 2008-12-15T13:20:57Z 2008 Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами / С.В. Потиенко // Проблеми програмування. — 2008. — № 4. — С. 39-44. — Бібліогр.: 8 назв. — рос. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/2600 519.686.2 В работе рассмотрены методы прямого и обратного символьного моделирования, используемые для решения задач верификации систем базовых протоколов. Помимо алгоритмов поиска в пространстве состояний системы, детально проработанных в области проверки на модели (model checking), основная задача символьного моделирования заключается в осуществлении перехода от одного класса состояний к следующему. Такая трансформация производится с помощью предикатных трансформеров. В данной работе построены алгоритмы прямого и обратного предикатных трансформеров для числовых, символьных и списочных структур данных. Трансформеры рассматриваются как функции, которые выводят из заданной формулы новую, определяющую класс состояний системы после перехода, совершенного под действием заданного базового протокола. -------------------- У роботі розглянуті методи прямого та зворотного символьного моделювання, які використовуються для рішення задач верифікації систем базових протоколів. Окрім алгоритмів пошуку в просторі станів системи, детально опрацьованих у області перевірки на моделі (model checking), основна задача символьного моделювання полягає у здійсненні переходу від одного класу станів до наступного. Така трансформація виконується за допомогою предикатних трансформерів. У даній роботі побудовані алгоритми прямого та зворотного предикатних трансформерів для чисельних, символьних та списочних структур даних. Трансформери розглядаються як функції, що виводять із заданої формули нову, яка визначає клас станів системи після переходу, здійсненого під дією заданого базового протоколу.------------------ The paper considers methods of forward and backward symbolic modeling which are used for solution of verification tasks for basic protocols systems. Besides of algorithms for state space search detailed in model checking works, the main task of symbolic modeling is implementation of transition from one state class to the next. Such a transformation is realized by predicate transformers. In the current work, algorithms of forward and backward predicate transformers have been built for numeric, symbolic, and lists data structures. Transformers are considered as functions which derive from given formula a new one that defines state class of the system after transition made by given basic protocol. ru Інститут програмних систем НАН України Теоретичні та методологічні основи програмування Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами Методи прямого і зворотного символьного моделювання систем, заданих базовими протоколами Methods of forward and backward symbolic modeling of systems specified by basic protocols 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 |
Методи прямого і зворотного символьного моделювання систем, заданих базовими протоколами Methods of forward and backward symbolic modeling of systems specified by basic protocols |
| description |
В работе рассмотрены методы прямого и обратного символьного моделирования, используемые для решения задач верификации систем базовых протоколов. Помимо алгоритмов поиска в пространстве состояний системы, детально проработанных в области проверки на модели (model checking), основная задача символьного моделирования заключается в осуществлении перехода от одного класса состояний к следующему. Такая трансформация производится с помощью предикатных трансформеров. В данной работе построены алгоритмы прямого и обратного предикатных трансформеров для числовых, символьных и списочных структур данных. Трансформеры рассматриваются как функции, которые выводят из заданной формулы новую, определяющую класс состояний системы после перехода, совершенного под действием заданного базового протокола. --------------------
У роботі розглянуті методи прямого та зворотного символьного моделювання, які використовуються для рішення задач верифікації систем базових протоколів. Окрім алгоритмів пошуку в просторі станів системи, детально опрацьованих у області перевірки на моделі (model checking), основна задача символьного моделювання полягає у здійсненні переходу від одного класу станів до наступного. Така трансформація виконується за допомогою предикатних трансформерів. У даній роботі побудовані алгоритми прямого та зворотного предикатних трансформерів для чисельних, символьних та списочних структур даних. Трансформери розглядаються як функції, що виводять із заданої формули нову, яка визначає клас станів системи після переходу, здійсненого під дією заданого базового протоколу.------------------
The paper considers methods of forward and backward symbolic modeling which are used for solution of verification tasks for basic protocols systems. Besides of algorithms for state space search detailed in model checking works, the main task of symbolic modeling is implementation of transition from one state class to the next. Such a transformation is realized by predicate transformers. In the current work, algorithms of forward and backward predicate transformers have been built for numeric, symbolic, and lists data structures. Transformers are considered as functions which derive from given formula a new one that defines state class of the system after transition made by given basic protocol.
|
| issn |
1727-4907 |
| url |
https://nasplib.isofts.kiev.ua/handle/123456789/2600 |
| citation_txt |
Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами / С.В. Потиенко // Проблеми програмування. — 2008. — № 4. — С. 39-44. — Бібліогр.: 8 назв. — рос. |
| work_keys_str_mv |
AT potienkosv metodyprâmogoiobratnogosimvolʹnogomodelirovaniâsistemzadannyhbazovymiprotokolami AT potienkosv metodiprâmogoízvorotnogosimvolʹnogomodelûvannâsistemzadanihbazovimiprotokolami AT potienkosv methodsofforwardandbackwardsymbolicmodelingofsystemsspecifiedbybasicprotocols |
| first_indexed |
2025-12-07T16:37:38Z |
| last_indexed |
2025-12-07T16:37:38Z |
| _version_ |
1850868192308625408 |