Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами

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

Full description

Saved in:

Bibliographic Details
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

_version_	1860003759796518912
author	Потиенко, С.В.
author_facet	Потиенко, С.В.
citation_txt	Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами / С.В. Потиенко // Проблеми програмування. — 2008. — № 4. — С. 39-44. — Бібліогр.: 8 назв. — рос.
collection	DSpace DC
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.
first_indexed	2025-12-07T16:37:38Z
format	Article
fulltext	Теоретичні та методологічні основи програмування © С.В. Потиенко, 2008 ISSN 1727-4907. Проблеми програмування. 2008. № 4 39 УДК 519.686.2 С.В. Потиенко МЕТОДЫ ПРЯМОГО И ОБРАТНОГО СИМВОЛЬНОГО МОДЕЛИРОВАНИЯ СИСТЕМ, ЗАДАННЫХ БАЗОВЫМИ ПРОТОКОЛАМИ В работе рассмотрены методы прямого и обратного символьного моделирования, используемые для решения задач верификации систем базовых протоколов. Помимо алгоритмов поиска в пространстве состояний системы, детально проработанных в области проверки на модели (model checking), основная задача символьного моделирования заключается в осуществлении перехода от одного класса состояний к следующему. Такая трансформация производится с помощью предикатных трансформеров. В данной работе построены алгоритмы прямого и обратного предикатных трансформеров для числовых, символьных и списочных структур данных. Трансформеры рассматриваются как функции, которые выводят из заданной формулы новую, определяющую класс состояний системы после перехода, совершенного под действием заданного базового протокола. Вступление Подходы к решению задачи вери- фикации программных систем можно раз- делить на два типа – проверка на модели (model checking) и доказательство теорем (theorem proving). Символьное моделиро- вание – один из методов комбинации про- верки на модели с доказательством теорем. Во время проверки на модели осуществля- ется поиск в пространстве состояний, ге- нерируемых поведением модели. В сим- вольном моделировании роль состояний играют формулы, которые покрывают классы состояний. Во время поиска в та- ком пространстве классов состояний ис- пользуются методы доказательств. Для простоты, классы состояний, заданные формулами, далее будем называть состоя- ниями. Переход от заданного состояния к следующему осуществляется с помощью прямого предикатного трансформера, определяемого как функция вывода фор- мулы – нового состояния модели. Для ре- шения задачи проверки достижимости за- данного состояния, как один из методов применяется обратное символьное моде- лирование, в котором переход от заданно- го состояния к предыдущему осуществля- ется с помощью обратного предикатного трансформера. В данной работе рассматриваются методы символьного моделирования над системами, заданными набором базовых протоколов. Общая методика верификации систем базовых протоколов описана в [1]. Представление требований в форме базо- вых протоколов базируется на теории взаимодействия агентов и сред [2, 3]. Ал- горитмы поиска в пространстве состояний описаны в [4–6]. Здесь раскрываются алго- ритмы работы прямого и обратного преди- катных трансформеров для систем с чи- словыми, символьными и списочными структурами данных. Краткое описание языка базовых протоколов Базовый протокол представляет со- бой выражение вида )( βα >→<∀ ux , где x – список (типизированных) параметров, α и β – формулы базового логического языка, u – процесс протокола (конечное поведение композиции нескольких агентов и среды, обычно задается с помощью MSC диаграмм). Формулаα называется преду- словием, а формула β – постусловием ба- зового протокола. Сам базовый протокол может рассматриваться как формула тем- поральной логики, выражающая тот факт, что, если состояние системы имеет размет- ку, удовлетворяющую условию α , то про- цесс u может быть инициирован, и после его завершения состояние системы будет удовлетворять условию β . В качестве базового языка исполь- зуется язык многосортного исчисления предикатов первого порядка. Формула ба- Теоретичні та методологічні основи програмування 40 зового языка может содержать переменные и константы следующих простых типов данных: числовые (целый и действитель- ный) и символьные (булевский, перечис- лимый и произвольный символьный). Так же допустимы массивы элементов простых типов с целыми или перечислимыми ин- дексами, функциональные типы (функции от аргументов простых типов, возвра- щающие значение простого типа), списки элементов простых типов. В роли пере- менных, меняющих свои значения в про- цессе функционирования системы, высту- пают атрибуты и атрибутные выражения. Атрибутными выражениями являются операторы доступа к элементу массива по индексам (a[i,j]), функции доступа к спи- скам (get_from_head(l), get_from_tail(l), empty(l)), выражения атрибутов функцио- нальных типов (a(x,y,z)). Предусловие базового протокола содержит формулу базового языка, в по- стусловии используются присваивания, операторы обновления списков, а так же формула базового языка. Левыми частями присваиваний могут выступать атрибуты простых типов и атрибутные выражения кроме функций доступа к спискам. Присваивания и операторы обновления списков рассматриваются как равенства, связывающие старые и новые значения атрибутов простых типов и атрибутных выражений. Прямой предикатный трансформер На каждом шаге моделирования из- вестно текущее состояние среды (на пер- вом шаге известно начальное состояние). Применимые в этом состоянии протоколы модифицируют состояние согласно своим постусловиям. Каждый из одновременно применимых протоколов создает новую ветвь в дереве поведения системы. Пред- и постусловие каждого базо- вого протокола представляется в таком ви- де: - предусловие: A(r,l,s,z); - постусловие: B(r,l,s,z) = (r := t0(r,l,s,z)) ∧ ∧ U(l,r,s,z) ∧ C(r,l,s). Здесь: - l – вектор списковых атрибутов; - r,s,z – вектора атрибутов и атрибутных выражений числовых и символьных типов; - A(r,l,s,z) и C(r,l,s) – формулы базового языка; - U(l,r,s,z) – конъюнкция операторов об- новления списков l; - r := t0(r,l,s,z) – конъюнкция присваива- ний новых значений атрибутам r: (r1 := t1(r,l,s,z)) ∧ (r2 := t2(r,l,s,z)) ∧ …; r := t(r,s,z) – присваивания после подста- новки значений операторов доступа к спи- скам (get_from_head(l), get_from_tail(l)); - z – вектор переменных, присутствую- щих в операторах присваивания и обнов- ления списков, но отсутствующих в фор- муле C(r,l,s) постусловия. Таким образом, r – это атрибутные выражения, значения которых меняются присваиваниями, а значения s могут изме- ниться недетерминированным образом, поскольку входят в условие С. Значения выражений из z не меняются. Базовый протокол применим на со- стоянии E, если формула E ∧ A(r,l,s,z) не ложна. Применимый базовый протокол осуществляет переход: E � E' . Здесь E и E' – формулы, опреде- ляющие состояния среды. Они представ- ляются в таком виде: - E = F(r,s,z) ∧ L(r,l,s,z), - E' = F'(r,s,z) ∧ L'(r,l,s,z), где - F(r,s,z), F'(r,s,z) – формулы базового языка; - L(r,l,s,z), L'(r,l,s,z) – списковые равенст- ва вида: (l1 = list(head1(r,s,z), …, tail1(r,s,z))) ∧ ∧ (l2 = list(head2(r,s,z), …, tail2(r,s,z))) ∧ …, где - headi(r,s,z) и taili(r,s,z) – последователь- ности выражений, могут быть пустыми; - … – абстрактная (неизвестная) часть списка; она отсутствует в списках кон- кретной длины. Во время прямого моделирования известно состояние E, с помощью прямого предикатного трансформера необходимо найти состояние E': E' = pt( E ∧ A(r,l,s,z), B(r,l,s,z) ). Теоретичні та методологічні основи програмування 41 Прямой предикатный трансформер определяется с учетом следующего пред- положения: все атрибуты и атрибутные выражения, встречающиеся на верхнем уровне в формуле C(r,l,s) постусловия, и только они могут изменить свои значения после применения базового протокола. Считается, что атрибут находится на верх- нем уровне, если он не расположен внутри какого-либо атрибутного выражения. На- пример, если атрибут встречается как ин- декс массива или параметр атрибута функ- ционального типа, это не считается верх- ним уровнем. Прямой предикатный трансформер применяется к формуле F(r,l,s,z) ∧ L(l,r,s,z) ∧ A(r,l,s,z) и выводит новую формулу E': . ))),,(,),,,((( ))),,(,),,,((( ),,,( .)),,(()),,(( ),,,( ).,,( )),,,(),,,(),,,( ),,,(),,((),( . 222 111 2211 21 K K K K K ∧ ∧=∧ ∧== =′ ∧=∧== = ∧ ∧∧′∧∧ ∧∧∃= ∨∨=′ ii ii i ii i iii iii vutailvuheadlistl vutailvuheadlistl vulL vutrvutr vurT slrC srvuPvulLvurT vluAvuFvuE EEE ξξ ξξ ξ ξξ ξ ξξ ξξ Здесь u, v – вектора связанных пе- ременных, введенных для обозначения старых значений атрибутов r, s. L'(l,u,v,ξi) содержит обновленные списки после при- менения операторов U(l,r,s,ξi). Если атри- бут функционального типа встречается среди атрибутных выражений вектора r или s, а также в векторе z, должны быть рассмотрены все комбинации возможных отождествлений его аргументов. Формула Pi(u,v,r,s) определяет одну из таких воз- можностей. Вектора ξi получаются заме- ной выражений из z с отождествленными аргументами переменными из списков u или v. Например, пусть выражение x(i) встречается среди левых частей присваи- вания, а x(j) встречается в z, где x – атри- бут функционального типа. Тогда рас- смотрим два случая: i = j и i ≠ j. Для случая i = j, выражение x(j) заменяется на пере- менную из списка u, соответствующую выражению x(i). Обратный предикатный трансформер Обратное моделирование позволяет из заданного состояния среды построить трассу в начальное состояние. Для этого используются алгоритмы прямого модели- рования с обратным предикатным транс- формером, который определяется далее. Во время обратного моделирования известно состояние E', с помощью обрат- ного предикатного трансформера необхо- димо найти состояние E: E = pt-1( E', A(r,l,s,z), B(r,l,s,z) ). Определяющим свойством обратно- го трансформера является следующее ус- ловие: .)),,,(),,,,( )),,,(),,,,(,(( 1 EzslrBzslrA zslrBzslrAEptpt ′→∧ ∧′− Рассмотрим два случая. 1. C(r,l,s) = 1. В данном случае постусловие со- держит только операторы присваивания и обновления списков. Рассмотрим оба типа операторов. Операторы присваивания изменяют формулу в состоянии среды как описано в прямом предикатном трансформере. Положим: F(r,s,z) = F'(t(r,s,z),s,z) ∧ A(r,l,s,z) ∧ P(r,s,z) или pt-1( F'(r,s,z) , A(r,l,s,z), B(r,l,s,z) ) = = F'(t(r,s,z),s,z) ∧ A(r,l,s,z) ∧ P(r,s,z). Как упоминалось выше, r, s, z – век- тора атрибутов не списковых типов, т.е. простых типов – числовые (целые и дейст- вительные), перечислимые, символьные, а так же функциональных типов. Массивы могут рассматриваться как функциональ- ные типы с одним целочисленным или пе- речислимым параметром, ограниченным размерностью массива. Если один атрибут функционального типа встречается в по- стусловии более одного раза, должны быть Теоретичні та методологічні основи програмування 42 рассмотрены все комбинации возможных отождествлений его аргументов. Формула P(r,s,z) определяет одну из таких возмож- ностей. Например, пусть выражения x(i) и x(j) встречаются B(r,l,s,z), где x – атрибут функционального типа. Тогда рассмотрим два случая: i = j и i ≠ j. Если формула F'(r,l,s,z) ложна, то данный базовый протокол не мог быть применен и соответствующая ветвь пове- дения не рассматривается. Докажем определяющее свойство такого обратного трансформера: ).,,(... )),,(),,,((),,( )...)),,((),,( ),,,(),),,,((( )...)),,(( ),,,(),,( )),,((),,,(),,(( )),,,(),,,,(),,(( )),,,(),,,,( )),,,(),,,,(),,,((( 111 11 111 2 22 111 1 zsrF suPsluAusrF sutrsuP sluAssutFu sutr sluAsuF sutrsluAsuFu zslrBzslrAzsrFpt zslrBzslrA zslrBzslrAzsrFptpt ′→∨ ∨∧∃∧′= =∨=∧∧ ∧∧′∃= =∨=∧ ∧∧∨ ∨=∧∧∃= =∧= =∧ ∧′− ξξξ ξξ ξξξ ξ ξξ ξξξ Операторы обновления списков U(r,l,s,z) изменяют списковые равенства в состоянии среды: pt(L(r,l,s,z), U(r,l,s,z)) = L'(r,l,s,z), pt-1(L'(r,l,s,z), A(r,l,s,z), U(r,l,s,z)) = L(r,l,s,z). U(r,l,s,z) содержит операторы add_to_tail(l, f(r,s,z)), add_to_head(l, f(r,s,z)), remove_from_tail(l, f(r,s,z)), remove_from_head(l, f(r,s,z)). L(r,l,s,z) содержит равенства вида: l = list(h1(r,s,z), head(r,s,z), …, tail(r,s,z), qn(r,s,z)). Здесь - h1(r,s,z), head(r,s,z) – рекурсивное пред- ставление непустой последовательности; h1(r,s,z) – арифметическое выражение или символьная константа; - tail(r,s,z), qn(r,s,z) – рекурсивное пред- ставление непустой последовательности tail(r,s,z); qn(r,s,z) – арифметическое выра- жение или символьная константа. Если head(r,s,z) или tail(r,s,z) пусты, то l = list(…, tail(r,s,z), qn(r,s,z)) или l = list(h1(r,s,z), head(r,s,z), …) соответст- венно. Полностью абстрактный список со- держит только неизвестную часть: l = = list(…). Восстановление списков и генера- ция списковых равенств L(l,r,s,z) произво- дится по правилам, описанным далее. Для оператора add_to_tail(l,f(r,s,z)): - если L'(l,r,s,z) содержит равенство l = list(head(r,s,z), …, tail(r,s,z), qn(r,s,z)) � применяем remove_from_tail(l) � тогда L(l,r,s,z) содержит равенство l = list(head(t(r,s,z),s,z), …, tail(t(r,s,z),s,z)); в формулу F необходимо добавить: ∃m( (get_from_tail(m) = f(r,s,z)) ∧ ∧ (l = list(head(r,s,z), …, tail(r,s,z), qn(r,s,z)) ) � f(r,s,z) = qn(r,s,z); - если L'(l,r,s,z) содержит равенство l = list(head(r,s,z), …) � неизвестная часть остается неизвестной � тогда L(l,r,s,z) содержит то же равенство l = list(head(t(r,s,z),s,z), …). Для оператора add_to_head(l,f(r,s,z)): - если L'(l,r,s,z) содержит равенство l = list(h1(r,s,z), head(r,s,z), …, tail(r,s,z)) � применяем remove_from_head(l) � тогда L(l,r,s,z) содержит равенство l = list(head(t(r,s,z),s,z), …, tail(t(r,s,z),s,z)); в формулу F необходимо добавить равен- ство f(r,s,z) = h1(r,s,z); - если L'(l,r,s,z) содержит равенство l = list(…, tail(r,s,z)) � неизвестная часть остается неизвестной � тогда L(l,r,s,z) содержит то же равенство l = list(…, tail(t(r,s,z),s,z)). Для оператора remove_from_tail(l): - пусть L'(l,r,s,z) содержит равенство l = list(head(r,s,z), …, tail(r,s,z)) � вводим новую переменную v и применяем add_to_tail(l,v) � тогда L(l,r,s,z) содержит равенство ∃v ( l = list(head(t(r,s,z),s,z), …, …, tail(t(r,s,z),s,z), v) ). Для оператора remove_from_head(l): - пусть L'(l,r,s,z) содержит равенство l = list(head(r,s,z), …, tail(r,s,z)) � Теоретичні та методологічні основи програмування 43 вводим новую переменную v и применяем add_to_head(l,v) � тогда L(l,r,s,z) содержит равенство ∃v ( l = list(v, head(t(r,s,z),s,z), …, …, tail(t(r,s,z),s,z)) ). У списков конкретной длины отсут- ствует неизвестная часть …, правила об- новления применяются те же. Необходимо лишь отдельно рассмотреть случай, когда состояние E' содержит пустой список l = list(), а постусловие базового протокола оператор add_to_tail(l) или add_to_head(l). Тогда этот протокол не мог быть применен и соответствующая ветвь поведения не рассматривается. ).,,(),,,(),,( ),),,,(,(),),,,(( )),,,( ),,,,(),,,,(),,((1 zsrPzslrAzsrM zszsrtlLzszsrtF zslrB zslrAzsrlLzsrFpt ∧∧∧ ∧∧′= = ′∧′− Здесь M(r,s,z) – конъюнкция ра- венств, добавленных во время восстанов- ления списков для операторов add_to_tail и add_to_head. Докажем определяющее свойство обратного трансформера с учетом обнов- ления списков: =∨=∧∧ ∧∧′∧∃= =∧∧ ∧∧= =∧ ′∧′− )...)),,((),,,( ),,(),,,(),,(( )),,,(),,,,(),,( ),),,,(,(),,(( )),,,(),,,,()),,,( ),,,,(),,,,(),,((( 11 111 1 ξξ ξξξ sutrsluA suMsrlLsuFu zslrBzslrAzsrM zszsrtlLzsrFpt zslrBzslrAzslrB zslrAzsrlLzsrFptpt ).,,,(),,( ...)),,(),,,( ),,((),,,(),,( )...)),,(( ),,(),,,(),,( ),,,(),),,,((( 11 111 1 111 111 zsrlLzsrF suPsluA suMusrlLsrF sutr suPsluAsuM srlLssutFu ′∧′→ →∨∧∧ ∧∃∧′∧′= =∨=∧ ∧∧∧∧ ∧′∧′∃= ξξ ξξξ ξ ξξξ ξξξ 2. C(r,l,s) ≠≠≠≠ 1. В этом случае постусловие кроме операторов присваивания и обновления списков содержит формулу базового язы- ка. Обновление списков производится по вышеописанным правилам. Необходимо лишь отдельно рассмотреть случай, когда состояние E' содержит пустой список l = list(), а формула C(r,l,s) содержит опе- раторы доступа get_from_tail(l) или get_from_head(l). Тогда этот протокол не мог быть применен и соответствующая ветвь поведения не рассматривается. Рас- смотрим влияние формулы C(r,l,s) на фор- мулу F. Пусть ( r = t(u,s,z) ∧ C(r,l,s) ) ≠ 0 (условие валидности постусловия). Операторы присваивания и форму- ла C(r,l,s) изменяют формулу в состоянии среды: F'(r,s,z) <=> ∃u ( F(u,s,z) ∧ A(u,l,s,z) ∧ ∧ (r = t(u,s,z)) ∧ C(r,l,s) ). Здесь u – вектор связанных пере- менных, введенных для обозначения ста- рых значений атрибутов r. Отсюда следу- ет: F(r,s,z) = = ∃v ( F'(t(r,v,z),v,z) ) ∧ A(r,l,s,z) ∧ P(r,s,z), или pt-1( F'(r,s,z) , A(r,l,s,z), B(r,l,s,z) ) = = ∃v ( F'(t(r,v,z),v,z) ) ∧ A(r,l,s,z) ∧ P(r,s,z). Определяющее свойство такого об- ратного трансформера, в том числе и с учетом списков, доказывается аналогично вышеприведенному. Примеры Пример 1: - предусловие: 1; - постусловие: (x := x + 1) ∧ (y := z); - формула F': (x > 0) ∧ (y > 5); - полученная формула F: (x + 1 > 0) ∧ (z > 5). Пример 2: - предусловие: 1; - постусловие: (x := x + 1) ∧ (y := z) ∧ add_to_tail(lst, 10); - состояние E': (x > 0) ∧ (y > 5) ∧ lst = list(x,y); - полученное состояние E: (x + 1 > 0) ∧ ∧ (z > 5) ∧ (z = 10) ∧ lst = list(x+1) � (x + 1 > 0) ∧ (z = 10) ∧ lst = list(x+1). Теоретичні та методологічні основи програмування 44 Пример 3: - предусловие: 1; - постусловие: (i := x[i]) ∧ (j := x[j]); - формула F': i = j; - полученная формула F: ( x[i] = x[j] ) ∧ ( i = j ∨ i ≠ j ) � ( i = j ) ∨ ( x[i] = x[j] ∧ i ≠ j ). Пример 4: - предусловие: x < 0; - постусловие: y < 0; - формула F': a < y ∧ y ≤ x; - полученная формула F: ∃u ( a < u ∧ u ≤ x ) ∧ x < 0 � a < x ∧ x < 0. Пример 5: - предусловие: x < 0; - постусловие: y := x + b ∧ y < b – 5; - формула F': a < y ∧ y ≤ x ∧ a > b – 10; - полученная формула F: ∃u ( a < x + u ∧ x + u ≤ x ∧ a > u –10 ) ∧ ∧ x < 0 � ∃u ( u – 10 < a ∧ a < x + u ∧ ∧ u ≤ 0 ∧ x < 0 ) � a < x ∧ x < 0. Пример 6 (неприменимый протокол): - предусловие: x < 0; - постусловие: y := x + b ∧ y < b – 5; - формула F': a < y ∧ y ≤ x ∧ a > b; - полученная формула F: ∃u ( a < x + u ∧ x + u ≤ x ∧ a > u ) ∧ x < 0 � ∃u ( a < x + u ∧ u ≤ 0 ∧ a > u ∧ x < 0 ) � 0. Выводы В данной работе рассмотрены мето- ды прямого и обратного символьного мо- делирования, используемые для решения задач верификации систем базовых прото- колов. Приведено решение задачи осуще- ствления перехода системы от одного класса состояний к следующему. Такая трансформация производится с помощью предикатных трансформеров. Каждый из- вестный класс состояний задается форму- лой базового языка. Построены алгоритмы прямого и обратного предикатных транс- формеров для числовых, символьных и списочных структур данных. Трансформе- ры рассматриваются как функции, которые выводят из заданной формулы новую, оп- ределяющую класс состояний системы по- сле перехода, совершенного под действием заданного базового протокола. 1. Летичевский А.А., Капитонова Ю.В., Вол- ков В.А. и др. Спецификация систем с помощью базовых протоколов // Кибернетика и систем- ный анализ. – 2005. – 4. – С. 3–21. 2. Letichevsky and D. Gilbert. A Model for Interac- tion of Agents and Environments // In D. Bert, C. Choppy, P. Moses, editors. Recent Trends in Al- gebraic Development Techniques. Lecture Notes in Computer Science 1827, Springer. – 1999. – P. 311–328. 3. Летичевский А.А., Капитонова Ю.В., Вол- ков В.А. и др. Инсерционное программирова- ние // Кибернетика и системный анализ. – 2003. – 1. – С. 19–32. 4. Летичевский А.А. Об одном классе базовых протоколов // Проблеми програмування. – 2005. – № 4. – С. 3–19. 5. Летичевський О.О., Левченко І.А. Символьна трасова генерація // Тези доп. Міжнар. конф. «Теоретичні та прикладні аспекти побудови програмних систем TAAPSD'2005». – К.: НаУ- КМА, Національний ун-т ім. Т.Г. Шевченка, Інститут програмних систем НАН України. – 2005. – С. 144–147. 6. Колчин А.В. Направленный поиск в верифика- ции формальных моделей // Тези доп. Міжнар. конф. «Теоретичні та прикладні аспекти побу- дови програмних систем TAAPSD'2007». – Бе- рдянськ. НаУКМА, Національний ун-т ім. Т.Г. Шевченка, Інститут програмних систем НАН України. – 2007. – С. 256–258. 7. Letichevsky A., Kapitonova J., Letichevsky A. Jr., Volkov V., Baranov S., Kotlyarov V., Weigert T. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications // Proc. International Workshop, WITUL’04. Rennes (France). – 2004. – P. 30–38. 8. Kapitonova J., Letichevsky A., Volkov V., and Weigert T. Validation of Embedded Systems // In R. Zurawski, editor. The Embedded Systems Handbook. CRC Press, Miami. – 2005. – 51 p. Получено 04.06.2008 Об авторе: Потиенко Степан Валериевич, ведущий математик. Место работы автора: Институт кибернетики им. В.М. Глушкова НАН Украины. Тел.: (044) 200 8423. e-mail: stepan@iss.org.ua Теоретичні та методологічні основи програмування © С.В. Потиенко, 2008 ISSN 1727-4907. Проблеми програмування. 2008. № 4 45
id	nasplib_isofts_kiev_ua-123456789-2600
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
issn	1727-4907
language	Russian
last_indexed	2025-12-07T16:37:38Z
publishDate	2008
publisher	Інститут програмних систем НАН України
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
spellingShingle	Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами Потиенко, С.В. Теоретичні та методологічні основи програмування
title	Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами
title_alt	Методи прямого і зворотного символьного моделювання систем, заданих базовими протоколами Methods of forward and backward symbolic modeling of systems specified by basic protocols
title_full	Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами
title_fullStr	Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами
title_full_unstemmed	Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами
title_short	Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами
title_sort	методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами
topic	Теоретичні та методологічні основи програмування
topic_facet	Теоретичні та методологічні основи програмування
url	https://nasplib.isofts.kiev.ua/handle/123456789/2600
work_keys_str_mv	AT potienkosv metodyprâmogoiobratnogosimvolʹnogomodelirovaniâsistemzadannyhbazovymiprotokolami AT potienkosv metodiprâmogoízvorotnogosimvolʹnogomodelûvannâsistemzadanihbazovimiprotokolami AT potienkosv methodsofforwardandbackwardsymbolicmodelingofsystemsspecifiedbybasicprotocols

Методы прямого и обратного символьного моделирования систем, заданных базовыми протоколами

Institution

Similar Items