Инсерционное моделирование

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

Ausführliche Beschreibung

Gespeichert in:

Bibliographische Detailangaben
Datum:	2012
1. Verfasser:	Летичевский, А.Ад.
Format:	Artikel
Sprache:	Russian
Veröffentlicht:	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України 2012
Schriftenreihe:	Управляющие системы и машины
Schlagworte:	Теоретические основы инсерционного моделирования
Online Zugang:	http://dspace.nbuv.gov.ua/handle/123456789/83102
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. — № 6. — С. 3-14. — Бібліогр.: 32 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	irk-123456789-83102
record_format	dspace
spelling	irk-123456789-831022015-06-15T03:02:00Z Инсерционное моделирование Летичевский, А.Ад. Теоретические основы инсерционного моделирования Представлен обзор современного состояния инсерционного моделирования – направления, которое развивается на протяжении последнего десятилетия как подход к построению общей теории взаимодействия агентов и сред в сложных распределенных многоагентных системах. The review of the current state of insertion modeling, – the direction which developed over the last decade as an approach to the construction of a general theory of the interaction of agents and environments in complex distributed multi-agent systems is presented. Подано огляд сучасного стану інсерційного моделювання – напрямку, який розвивається на протязі останнього десятиліття як підхід до побудови загальної теорії взаємодії агентів та середовищ у складних розподілених багатоагентних системах. 2012 Article Инсерционное моделирование / А.Ад. Летичевский // Управляющие системы и машины. — 2012. — № 6. — С. 3-14. — Бібліогр.: 32 назв. — рос. 0130-5395 http://dspace.nbuv.gov.ua/handle/123456789/83102 519.686.2 ru Управляющие системы и машины Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
collection	DSpace DC
language	Russian
topic	Теоретические основы инсерционного моделирования Теоретические основы инсерционного моделирования
spellingShingle	Теоретические основы инсерционного моделирования Теоретические основы инсерционного моделирования Летичевский, А.Ад. Инсерционное моделирование Управляющие системы и машины
description	Представлен обзор современного состояния инсерционного моделирования – направления, которое развивается на протяжении последнего десятилетия как подход к построению общей теории взаимодействия агентов и сред в сложных распределенных многоагентных системах.
format	Article
author	Летичевский, А.Ад.
author_facet	Летичевский, А.Ад.
author_sort	Летичевский, А.Ад.
title	Инсерционное моделирование
title_short	Инсерционное моделирование
title_full	Инсерционное моделирование
title_fullStr	Инсерционное моделирование
title_full_unstemmed	Инсерционное моделирование
title_sort	инсерционное моделирование
publisher	Міжнародний науково-навчальний центр інформаційних технологій і систем НАН та МОН України
publishDate	2012
topic_facet	Теоретические основы инсерционного моделирования
url	http://dspace.nbuv.gov.ua/handle/123456789/83102
citation_txt	Инсерционное моделирование / А.Ад. Летичевский // Управляющие системы и машины. — 2012. — № 6. — С. 3-14. — Бібліогр.: 32 назв. — рос.
series	Управляющие системы и машины
work_keys_str_mv	AT letičevskijaad insercionnoemodelirovanie
first_indexed	2025-07-06T09:50:12Z
last_indexed	2025-07-06T09:50:12Z
_version_	1836890627420192768
fulltext	УСиМ, 2012, № 6 3 Теоретические основы инсерционного моделирования УДК 519.686.2 А.Ад. Летичевский Инсерционное моделирование Представлен обзор современного состояния инсерционного моделирования – направления, которое развивается на протяже- нии последнего десятилетия как подход к построению общей теории взаимодействия агентов и сред в сложных распределен- ных многоагентных системах. The review of the current state of insertion modeling, – the direction which developed over the last decade as an approach to the con- struction of a general theory of the interaction of agents and environments in complex distributed multi-agent systems is presented. Подано огляд сучасного стану інсерційного моделювання – напрямку, який розвивається на протязі останнього десятиліття як підхід до побудови загальної теорії взаємодії агентів та середовищ у складних розподілених багатоагентних системах. Введение. Инсерционное моделирование пред- ставляет собой направление, развиваемое на протяжении последнего десятилетия как подход к построению общей теории взаимодействия агентов и сред в сложных распределенных мно- гоагентных системах. Основные понятия инсер- ционного моделирования (среда, агенты, функ- ция погружения) ведены в работах [1–3], опуб- ликованных в 90-х годах. Идейным прототипом инсерционного моделирования следует счи- тать модель взаимодействующих управляюще- го и операционного автоматов, предложенную В.М. Глушковым еще в 60-х годах [4, 5] для описания структур вычислительных машин, а также ее развитие в теории дискретных преоб- разователей 70-х годов. В этих моделях систе- ма представляется в виде композиции двух ав- томатов – управляющего и информационного. Управляющий автомат играет роль агента, а информационный – роль среды погружения это- го агента. Модели макроконвейерных парал- лельных вычислений, исследованные в 80-е го- ды [6], еще больше приблизились к современ- ной модели взаимодействия агентов и сред. В этих моделях процессы, соответствующие па- раллельно работающим процессорам, можно рассматривать как агентов, взаимодействующих в среде распределенных структур данных. Другой источник инсерционного моделиро- вания – общая теория взаимодействующих ин- формационных процессов, сформированная в 70-х годах и служащая основой для современ- ных исследований в этой области. Она включает в себя CCS (Calculus of Communicated Processes) [7, 8] и π-исчисление Р. Милнера [9], CSP (Com- municated Sequential Processes) Т. Хоара [10], ACP (Algebra of Communicated Processes) [11] и много различных ответвлений этих базовых теорий. Достаточно полный обзор классической теории процессов представлен в справочнике по алгеб- ре процессов [12], изданном в 2001 г. Модели, исследуемые в этих теориях, можно эквивалент- ным образом представить в виде композиции среды и погруженных в нее агентов. Различные предложения по унификации общей теории вза- имодействия в распределенных системах актив- но обсуждаются, начиная с 90-х годов. К ним относятся чисто математические исследования на основе коалгебр [13], подход, предложен- ный Хоаром [14], логика условного переписы- вания Месегера [15] и др. В последние годы инсерционное моделиро- вание становится инструментом разработки при- кладных систем верификации требований и спе- цификаций распределенных взаимодействующих систем [16–19]. Система VRS, разработанная в Украине по заказу фирмы Моторола с участи- ем сотрудников Института кибернетики, успеш- но применяется для верификации требований и спецификаций в области телекоммуникацион- ных систем, встроенных систем и систем ре- ального времени. Статья носит обзорный характер. Основные понятия теории взаимодействия такие, как тран- 4 УСиМ, 2012, № 6 зиционная система, трассовая и бисимуляцион- ная эквивалентность, алгебра процессов и по- ведений, последовательная и параллельная композиция транзиционных систем предпола- гаются известными. Соответствующие опреде- ления можно найти в [20] и в [21]. Агенты и среды Инсерционное моделирование занимается построением моделей и изучением взаимодей- ствия агентов и сред в сложных распределенных многоагентных системах. Основные положения парадигмы инсерционного моделирования мож- но сформулировать следующим образом.  Мир есть иерархия сред и агентов, погру- женных в эти среды.  Агенты и среды есть сущности, эволю- ционирующие во времени и обладающие на- блюдаемым поведением.  Погружение агента в среду изменяет пове- дение этой среды и порождает новую среду, готовую к погружению в нее новых агентов (если для них есть место в этой среде).  Среда, рассматриваемая как агент, может быть погружена в среду верхнего уровня.  Агенты могут погружаться в среду из сре- ды верхнего уровня, а также производиться внутренними агентами, уже погруженными в среду ранее.  Агенты и среды могут моделировать дру- гие агенты и среды на различных уровнях аб- стракции. Говоря об агентах и средах, мы имеем в ви- ду как технические, так и реальные системы – физические, биологические и социальные, а взаимодействия, интересующие нас – это в первую очередь информационные взаимодей- ствия, абстрагированные от физических про- цессов, которыми они сопровождаются. Переходя к математическим уточнениям, вы- берем в качестве понятия агента наиболее аб- страктное математическое понятие, моделиру- ющее системы, эволюционирующие во време- ни. Таким образом, агент – это размеченная транзиционная система, состояния которой оп- ределяются с точностью до бисимуляционной или трассовой эквивалентности. Главным пре- имуществом понятия транзиционной системы в сравнении с другими моделями систем, эволю- ционирующих во времени, является разделе- ние наблюдаемой части системы, которая вы- ражается в действиях, и скрытой части систе- мы, определяемой ее внутренними состояниями. Среда – это агент, обладающий функцией погружения. Более точно, среда – это набор <E, C, A, Ins>, где E – множество состояний среды (отождествляемых с поведениями), С – множество действий среды, А – множество действий агентов, погружаемых в среду, Ins : E  F (A)  E – функция погружения. Здесь F (A) – полная алгебра поведений агентов с множеством действий A. Таким образом, всякая среда E допускает погружение любого агента с множеством действий A. Поскольку состояния транзиционных систем рассматриваются с точ- ностью до бисимуляционной эквивалентности, то их можно отождествлять с поведениями и говорить о непрерывности функций. Основное требование к среде – это непрерывность функ- ции погружения. Из этого предположения вы- текает ряд полезных следствий. Например, тот факт, что функцию погружения можно зада- вать как наименьшую неподвижную точку сис- темы функциональных уравнений. Результат Ins (e, u) погружения агента, находящегося в состоянии u, в среду, находящуюся в состоя- нии e, обозначается так же как e[u]. Полагая e[u, v] = (e[u])[v], получаем возможность гово- рить о совокупности агентов, погруженных в среду и рассматривать состояния среды вида e[u1, u2, , um] = (((e[u1]) [u2]))[um]. Прини- мая во внимание, что среда есть агент, ее можно погружать в среду верхнего уровня, рассматривая многоуровневые среды вида EEE uueuuee ,...],...],[,,...],[[ 21 22212112111 , где обо- значение e[u1, u2, ]E явно указывает среду E, которой принадлежит состояние e. Поведение u инициализированного агента определяет пре- образование [u]: E  E, определенное соотно- шением [u] (e) = e[u] и инсерционную эквива- лентность агентов E~ относительно среды Е, оп- ределенную соотношением ~Eu v [ ] [ ]u v  . Эта эквивалентность обычно слабее, чем би- симуляционная, играет основную роль в при- УСиМ, 2012, № 6 5 ложениях, поскольку преобразования алгорит- мических и программных реализаций агентов, функционирующих в некоторой среде, следует выполнять как преобразования, сохраняющие инсерционную эквивалентность. Расширенная алгебра поведений Напомним, что алгебра поведений имеет две основные операции: префиксинг ua. и неде- терминированный выбор u + v, где a – дейст- вие, u и v – поведения. Кроме того, в алгебре поведений есть две терминальные константы – успешное завершение  и тупиковое поведе- ние 0 (неопределенное поведение и отношение аппроксимации, используемые при построении полной алгебры поведений, сейчас не понадо- бятся). Всякое поведение можно представить в нормальной форме . εi i u i I u a u    , где u – терминальная константа (если I  , то u = , поскольку u + 0 = 0). Если все поведения в правой части рекурсивно представлены в нор- мальной форме, то для u получится представ- ление в виде ориентированного дерева, воз- можно бесконечного, с дугами, размеченными действиями, и некоторыми вершинами, отме- ченными символом  . Любая конечная часть такого дерева (т.е. конечное множество конеч- ных путей, которые начинаются в корне) назы- вается префиксом поведения. Система поведений    )( )(,,. iJj ijiji IiJIiuau  может рассматриваться как система рекурсив- ных определений. Если она конечна, то пове- дения называются конечно определенными. Та- кие поведения могут быть отождествлены с состояниями конечной транзиционной систе- мы с отношением переходов , ,ija i ju u i I  ( )j J i I  и с множеством заключительных состояний { \| ε }i iU u    . Расширим алгебру поведений, добавив к ней функции погружения, рассматриваемые как би- нарные операции на соответствующих множе- ствах. Формально мы должны рассмотреть мно- гоосновную алгебру, которая получается, если зафиксировать некоторое семейство сред (E)H и алгебр поведений агентов ( )F A  в каче- стве основных множеств. Тогда функция погру- жения будет определена как : ( )Ins E F A    E и выражения, рассмотренные в начале этого раздела, можно будет рассматривать как алгебраические выражения соответствующей многоосновной алгебры. Среда, определенная с помощью такой алгебры, называется много- уровневой средой. Основные свойства функций погружения Будем рассматривать только такие среды, для которых имеет место тождество [ , ]e u   [ ]e u . Состояние среды e называется нераз- ложимым, если из того, что ][uee  , следует, что  uee , . Множество неразложимых со- стояний среды назовем ее ядром. Неразложи- мое состояние среды соответствует состоянию до погружения в нее каких бы то ни было аген- тов, а среда с пустым ядром предполагает, что в нее изначально погружено бесконечное мно- жество агентов. Среда называется конечно-раз- ложимой, если всякое ее состояние можно пред- ставить в виде ],...,[ 1 muue с неразложимым e. В дальнейшем, если не оговорено противное, бу- дут рассматриваться только конечно-разложи- мые среды. Одношаговое погружение определяется пра- вилом ),,( ][][ , cbaP ueue uuee c ba   . Здесь ),,( cbaP – разрешающий предикат. Правило применимо только в том случае, ко- гда разрешающий предикат истинен. Для ко- нечно-разложимой среды, в которую погруже- но несколько агентов, следует воспользоваться производным правилом: ),,( ],...,[],...,[ ],,...,[],...,[ 11 1111 dbcP uueuue uuuueuue m d m m b mm c m    , где e – неразложимое состояние среды. Другая форма правила одношагового по- гружения: ][].)[.(),,( ueuubeeacbaP c  . 6 УСиМ, 2012, № 6 Одношаговое правило можно понимать так. Если агент хочет выполнить действие b (одно из возможных), то среда разрешает это дейст- вие, если у нее найдутся два действия a и с, такие, что имеет место P (a, b, c). В этом случае переход зависит только от того, что среда мо- жет сделать за один шаг. Более общее правило может быть сформули- ровано, если в разрешающий предикат доба- вить поведение среды: P (e, a, b, c). Но для то- го, чтобы обеспечить непрерывность функции погружения, нужно потребовать непрерывность разрешающего предиката: он должен зависеть только от конечного префикса поведения e. Та- кое правило называется правилом одношагово- го префиксного погружения (head insertion). На- конец, еще более общий случай получается, ес- ли разрешающий предикат зависит и от пове- дения агента: P (e, u, a, b, c). Такое погружение называется прогнозирующим. Рассмотренное правило не является полным. Требуются дополнительные правила для тер- минальных состояний среды и агента, а также для недетерминированного выбора. Примерами таких правил могут быть тождества 0[u] = 0 [u] = , e[] = e, которые можно дополнить тождеством e[0] = 0 для неразложимого со- стояния среды e. Функция погружения называется аддитив- ной, если ][][])[(],[][][ veueufeveuevue  . Аддитивность функции погружения может означать, что как среда, так и агент делают свой выбор независимо, но так, чтобы была возмож- ность продолжать движение. При этом следует иметь в виду, что если нет правила, по которо- му возможен переход из e[u]  , то e[u] = 0. Кроме аддитивных, на практике встречаются коммутативные погружения с тождествами e[u, v] = e[v, u] и, как частный случай коммута- тивных, параллельные погружения: e[u, v] = = e[u \|\| v]. Атрибутные среды Для многих практических приложений по- нятие среды и агента слишком абстрактно, по- скольку игнорирует структуру состояний сре- ды и агентов. Кроме того, при переходе в тер- минальное состояние теряется информация о состоянии среды, если она имеет структуру. Всю необходимую информацию можно, разумеет- ся, передавать через действия, но это часто вы- глядит неестественно и громоздко. Для того чтобы решить эту проблему, в [22] было вве- дено понятие атрибутной транзиционной сис- темы. Атрибутные транзиционные системы от- личаются от размеченных тем, что в них раз- мечены не только переходы, но и состояния. Алгебра поведений для атрибутных систем от- личается: поведения могут быть размечены ат- рибутными разметками. Для этой цели, кроме префиксинга, вводится еще одна операция, опе- рация разметки  : u, где u – поведение,  – раз- метка. Теперь вся необходимая информация о состоянии среды может передаваться через ее разметку. В частности может быть много тер- минальных констант, соответствующих успеш- ному завершению или тупику, поскольку они могут иметь различные разметки. Атрибутные среды строятся на основе не- которой логической базы. Эта база включает в себя набор типов (целые, вещественные, пере- числимые, символьные, поведения и т.д.), ин- терпретированных на некоторых областях дан- ных, символы для обозначения констант из этих областей и набор типизированных функцио- нальных и предикатных символов. Часть этих символов интерпретирована (например, ариф- метические операции и неравенства, равенство для всех типов и т.д.). Неинтерпретированные функциональные и предикатные символы на- зываются атрибутами. Неинтерпретированные функциональные символы арности 0 называ- ются простыми атрибутами, остальные – функ- циональными атрибутами (неинтерпретирован- ный предикатный символ рассматривается как функциональный с бинарной областью значе- ний). Функциональные символы используются для определения структур данных, таких как массивы. Над логической базой атрибутной среды строится базовый логический язык. Обычно это язык первого порядка, возможно с кванторами. При необходимости могут включаться некото- рые модальности темпоральной логики. Атри- УСиМ, 2012, № 6 7 бутным выражением называется простой ат- рибут или выражение вида f (t1, , tn), где f – функциональный атрибут арности n, t1, , tn – уже построенные атрибутные выражения или константы подходящих типов. Если все выра- жения t1, , tn константы, то атрибутное вы- ражение называется константным. Ядро атрибутной среды состоит из формул базового языка. Атрибутные среды делятся на два класса: конкретные и символьные. Неразложимое состояние конкретной ат- рибутной среды представляет собой формулу вида t1 = a1    tn = an, где t1, , tn – различные константные атрибутные выражения, a1, , an – константы. Обычно такую формулу представ- ляют в виде частичного отображения с обла- стью определения (t1, , tn) и областью значе- ний, равной множеству всех констант. Конкрет- ные атрибутные среды удобно использовать для формализации операционной семантики языков программирования и языков спецификации про- граммных систем. Состояние среды – это состо- яние памяти (структур данных, объектов, сете- вых конструкций, каналов и т.п.). Программы – это агенты, погруженные в среду. Для парал- лельных языков программирования взаимодей- ствие осуществляется через общую память или обмен сообщениями. При взаимодействии че- рез общую память основную роль играет парал- лельная композиция поведений (асинхронная или синхронизируемая). Обмен сообщениями предполагает использование специальных струк- тур данных в среде для организации взаимо- действия. Действия агентов в конечном итоге сводятся к присваиваниям (x := t, где x – атри- бутное выражение, t – алгебраическое выраже- ние базового языка) и проверкам условий (check , где  – формула базового языка). Со- ответствующие правила имеют вид: ),,( ][][ , : :: txeP ueue uuee tx txtx     ; check check \| [ ] [ ] u u e e u e u       . Разрешающее условие для присваивания мо- жет накладывать ограничение на однознач- ность значений для аргументов левой и правой части присваивания. Программные конструкции (различные ви- ды циклов, ветвления и т.п.) в большинстве случаев достаточно просто моделируются ре- курсивными уравнениями в алгебре поведе- ний. Например, . .if then P else Q check P check Q     , ( ; ) while do P if then P while do P else     . Неразложимые состояния символьной сре- ды – это формулы базового языка произволь- ного вида. Конкретные и символьные состоя- ния атрибутной среды вида F [u1, u2, ] также рассматриваются как формулы. Предполагает- ся, что все погруженные агенты имеют уникаль- ные имена (это могут быть, например, их атри- бутные отметки). Далее, среди атрибутов базо- вого языка есть функциональный атрибут state, определенный на именах агентов и принимаю- щий значения в области их поведений. Если m1, m2, имена агентов u1, u2, , то 1 2 1 1 2 2 [ , ,...] (state( ) ) (state( ) ) ... . F u u F m u m u        Локальные свойства Наиболее известные способы спецификации программ и систем (программных и техничес- ких) находятся в области темпоральной, дина- мической и некоторых других видов модальных логик [23]. Однако в большинстве случаев они применяются тогда, когда уже известна доста- точно подробная модель системы и решается проблема проверки свойств этой системы, за- данных в логической форме (model checking). Другой способ описания требований и спе- цификации систем – описание локальных по- веденческих свойств системы. В математичес- кой форме речь идет о свойствах отношения пе- реходов транзиционной системы, а в случае, когда система представлена в виде композиции среды и агентов, речь идет об описании функ- ции погружения. Рассмотрим локальные свойства системы, представленной как конкретная или символь- ная атрибутная среда. В общем случае локаль- ное свойство атрибутной среды имеет вид фор- мулы x (  < u > ), где x – список (типизи- 8 УСиМ, 2012, № 6 рованных) параметров,  и  – формулы базо- вого языка, u – процесс (конечное поведение специфицируемой системы). Формула  назы- вается предусловием, а формула  – постусло- вием локального свойства. От параметров мо- гут зависеть как условия, так и поведение сис- темы. Локальное свойство может рассматривать- ся как формула темпоральной логики, выража- ющая тот факт, что если (для подходящих зна- чений параметров) состояние системы удовле- творяет условию , то поведение u может быть инициировано, и после его успешного заверше- ния, разметка нового состояния будет удовлет- ворять условию . Не трудно проследить ана- логию между тройками Хоара (формулы ди- намической логики) и локальными свойствами систем. Другая аналогия – это продукции, ши- роко применяемые при описании систем ис- кусственного интеллекта. Локальные свойства, используемые во вход- ном языке системы VRS для представления ин- серционных моделей распределенных взаимо- действующих систем, носят название базовых протоколов. Они привязаны к базовому языку системы VRS, а для представления поведения системы используются MSC диаграммы [24]. Обычно базовые протоколы определяются не- зависимо друг от друга и на них априори не за- дано никаких отношений следования, определя- ющих порядок их применения. Поэтому семан- тика спецификаций на основе базовых протоко- лов не очевидна. В процессе исследования се- мантики языка базовых протоколов было разра- ботано несколько подходов к построению такой семантики. В этих подходах существенную роль играют понятия абстракции и конкретизации, на которых остановимся более подробно. Абстракции. При работе с большими сис- темами, такими как телекоммуникационные сис- темы, сети типа Интернет, многопроцессорные системы с большим числом компонент, невоз- можно манипулировать полными описаниями их состояний. Поэтому, принято заменять состоя- ния таких систем различного рода абстрактны- ми объектами. В инсерционном моделировании в качестве абстракций больших систем исполь- зуются атрибутные системы, состояния кото- рых размечаются формулами базового языка. Если состояния сами представлены формула- ми, получаем символьные атрибутные модели. Для изучения соотношений между абстракт- ными и конкретными моделями в [19] введены понятия абстракции и конкретизации атрибут- ных транзиционных систем. Предполагается, что состояния исходной сис- темы и формулы базового языка связаны от- ношением (семантического) следования s \|= , которое означает, что формула  истинна на разметке состояния s (разметка может не быть формулой). Если же состояние s не размечено, то s \|=  означает, что  есть тождественно ис- тинная формула базового языка, т.е. истинна на любых разметках. Отношение следования определено также на состояниях абстрактной системы, которые размечены формулами базо- вого языка, и в этом случае s \|=  означает, что  есть следствие формулы, которая размечает данное состояние. Пусть S и S – две атрибутные (не обяза- тельно различные) системы с размеченными состояниями, одной и той же логической ба- зой и множеством действий. Пусть BL – ба- зовый язык. Определим отношение абстрак- ции SS Abs таким образом, что ( , ) ( )(( \| ) ( \| ))s s s s         Abs BL . Система S называется прямой абстракцией системы S  , а система S  прямой конкретиза- цией системы S, если существует непустое от- ношение 1  Abs , которое является отноше- нием моделирования, т.е. имеет место следую- щее утверждение: ( , )(( , ) ( )( ( , ) )). a a s S s S s s s t t S s t t t                   Система S называется обратной абстрак- цией системы S  , а система S – обратной кон- кретизацией системы S, если существует не- пустое отношение 1  Abs , которое является отношением обратного моделирования, т.е. име- ет место следующее утверждение: ( , )(( , ) ( )( ( , ) )). a a s S s S s s s t t S s t t t                УСиМ, 2012, № 6 9 Система и ее абстракция связаны следующим образом. Если в прямой абстракции системы из некоторого состояния достижимо заданное свой- ство, то оно также достижимо из некоторого со- стояния самой системы. Для обратной абстрак- ции имеет место двойственное свойство: если из некоторого состояния системы достижимо со- стояние, в котором заданное свойство наруша- ется, то из некоторого начального состояния ее обратной абстракции также достижимо состо- яние, в котором это свойство нарушается. Прикладное значение этих утверждений со- стоит в том, что, комбинируя прямую и обрат- ную абстракции, можно получать различные ре- зультаты по верификации систем и генерации тестов. Например, если есть подозрение в том, что система имеет ошибку, то найти ее можно с помощью прямой абстракции, убедиться же в том, что в системе нет ошибок, можно с помо- щью обратной абстракции. Обратную абстрак- цию удобно также использовать для генерации тестов, обеспечивающих определенную степень покрытия требований, выраженных в виде сис- тем базовых протоколов. Семантика. В [19] была построена общая семантика систем базовых протоколов, сопос- тавляющая каждой системе P базовых прото- колов некоторую фиксированную транзицион- ную систему S(P), определенную с помощью системы уравнений в алгебре поведений. Эта система уравнений строится следующим обра- зом. Сначала по системе P строится множество Pinst конкретизированных базовых протоколов. Конкретизированный базовый протокол (z)   <u (z) > (z) получается из формулы x ((x)   < u (x)> (x)) путем подстановки конкретно- го набора значений z параметров вместо x. Да- лее на множестве действий среды определяет- ся отношение перестановочности, и на базе этого отношения определяется частично после- довательная композиция (()()) поведений. Для атрибутных систем перестановочность может означать их информационную независимость. На множестве конкретизированных свойств оп- ределяются функции app (F, ) = 0,1 и pt (F, ) = F  (предикатный трансформер). Первая использу- ется для определения применимости свойства с предусловием  к состоянию среды F, вторая – для вычисления нового состояния среды с по- мощью постусловия . Основное требование к функции pt состоит в том, чтобы условие  было истинным на состоянии F . Система уравнений для поведений FS системы S(P) в состояниях F, имеет вид:     instPu Fapp FptF u    ,1),( ),( )( SS . Для определения применимости протоколов используются два метода: экзистенциальный и универсальный. Определение применимости по экзистенциальному методу означает выполни- мость конъюнкции F  , применимость по уни- версальному методу означает общезначимость импликации F  . Другой подход к определению семантики базовых протоколов, также рассмотренный в статье [19], состоит в сопоставлении системе базовых протоколов P некоторого множества C(P) конкретных атрибутных систем, которые по определению объявляются реализациями си- стемы P. Было показано, что система S(P) есть абстракцией любой системы из класса C(P). Эта абстракция будет прямой, если выбран уни- версальный метод, и обратной, если выбран экзистенциальный метод. В [25] был предложен новый подход, осно- ванный на общем (абстрактном) понятии реа- лизации системы базовых протоколов. В этой работе базовые протоколы рассматривались с привязкой к интерпретированным MSC диа- граммам системы VRS, используемым в каче- стве способа задания процессов системы. Но понятие реализации легко обобщается и на произвольные локальные свойства. В соответствии с этой семантикой каждая спецификация P на языке базовых протоколов определяет некоторый класс атрибутных тран- зиционных систем, которые объявляются реа- лизациями системы P. Этот класс определяется аксиоматически и включает в себя как конкрет- ные, так и символьные реализации. На состоя- ниях реализации по-прежнему должно быть оп- ределено отношение истинности s \| =  и от- ношение перестановочности действий, которое 10 УСиМ, 2012, № 6 определяет частично последовательную компо- зицию. Основная аксиома, определяющая реа- лизацию, имеет вид [ ]*[ ]( , ), \|B Cappl s s s s     . Здесь B и C – базовые протоколы, [B] и [C] – их процессы. Предполагается, что [B] и [C] перестановочны. Условие  есть предусловие базового протокола B, а условие  его посту- словие. Предикатный трансформер. Каждая фор- мула базового языка соответствует множеству конкретных состояний, на котором она истин- на (покрывает это множество). Поэтому функ- ция погружения для символьной среды должна быть согласованной с функцией погружения со- ответствующей конкретной среды. Эта согла- сованность определяется в терминах предикат- ного трансформера, который сам по себе опре- деляет переходы как в конкретной, так и в сим- вольной атрибутной среде. Если в конкретной системе s s  и s \|= F, то \| ( , )s pr F   . Та- ких функций может быть много, и простейшая из них определяется как ( , )pr F    . Но при этом полностью теряется информация о пре- дыдущем состоянии F. Между тем, часть этой информации может переходить в новое состо- яние. Например, если постусловие меняет зна- чения только нескольких атрибутов, то осталь- ные не меняют своих значений. Среди всех функций, определяющих предикатный транс- формер, может существовать наисильнейшая. Она должна удовлетворять обратному усло- вию: если \| ( , )s pr F   и s s  , то должно быть s \|= F. Вопрос о существовании сильней- шего предикатного трансформера и возможно- сти выразить его средствами базового языка зависит от этого языка. В работе [26] постро- ен сильнейший предикатный трансформер для входного языка системы VRS. Рассмотрим более детально структуру преди- катного трансформера для случая атрибутов про- стых типов. Пусть базовый протокол имеет вид ( ( , , ) ( , , ) ( , ))x z s x u z s x s x    , (1) где x – список параметров, z – список атрибу- тов, которые входят в предусловия, но не вхо- дят в постусловия, s – список атрибутов, вхо- дящих в постусловия. Пусть F(z,s) – формула текущего состояния. Основное предположе- ние, используемое для построения предикат- ного трансформера, состоит в том, что после завершения базового протокола изменить свое значение могут только те атрибуты, которые яв- но входят в постусловие. Условием примени- мости базового протокола служит одно из двух утверждений ( , )( ( , )z s F z s  ( ( , , ))x z s x или ( , )( ( , ) ( ( , , ))z s F z s x z s x  . При использовании первого условия получаем прямую абстракцию всех конкретных моделей, а при использовании второго – обратную. Предикатный трансформер должен сформировать сильнейшее постусло- вие, следующее из условия применимости. Вот это условие (оно будет одним и тем же как для прямой, так и для обратной абстракции): )),(),,(),()(,( xsxyzyzFyx   . После формирования этого условия, преди- катный трансформер должен удалить кванторы, если это возможно. Таким образом, для реали- зации абстрактной модели базовых протоколов нужны дедуктивные средства (прувер и солвер для базового языка). Если в постусловиях используются присва- ивания, то формула модифицируется с исполь- зованием обычной (Хоаровской) семантики при- сваиваний. Возможны также обобщения кон- струкции предикатного трансформера в слу- чае, когда допускаются структуры данных та- кие, как массивы, списки и т.п. Используя семантику базовых протоколов можно генерировать трассы и сценарии функ- ционирования системы как на уровне конкрет- ных, так и на уровне абстрактных моделей. Эти трассы и сценарии можно использовать для ди- намической проверки различных свойств сис- темы, например, доказывать инвариантность или достижимость условий, выразимых в базовом языке, а также условий, выразимых с помощью различных видов темпоральной логики. Исполь- зуя дедуктивные средства, можно также про- водить статическую верификацию. Например, для доказательства инвариантности свойства , достаточно доказать, что это свойство сохра- УСиМ, 2012, № 6 11 няется всеми базовыми протоколами, а сохра- нение свойства  = (z, s) базовым протоколом (1) означает истинность формулы ( , , )( ( ( , ) ( , , )) ( , ) ( , ))z s x y z y z y x s x z s      , смысл которой состоит в том, что если в ка- кой-то момент  было истинным и был приме- ним протокол (1), то после его применения свойство  остается истинным. Верификация. Язык базовых протоколов, ре- ализованный в системе VRS, допускает исполь- зование атрибутов числовых и символьных ти- пов (свободные термы), массивов, списков и функциональных типов данных. Дедуктивная система обеспечивает доказательство утвержде- ний в теории первого порядка, представляющей собой интеграцию теорий целочисленных и ве- щественных линейных неравенств, перечисли- мых типов данных, свободных (неинтерпрети- рованных) функциональных символов и теорию очередей. В дедуктивной системе успешно до- казываются или опровергаются только некото- рые классы формул, поэтому при верификации иногда могут быть получены отказы для неко- торых промежуточных запросов. На практике такие отказы происходят достаточно редко и в большинстве случаев не влияют на получение окончательного результата. В качестве языка процессов используется язык MSC [24] с инсерционной семантикой [27, 28]. Система также допускает использова- ние языка SDL [29] и соответствующих диа- граммных представлений языка UML [30]. Основные средства системы VRS – это кон- кретный и символьный генераторы трасс и средства статической верификации, включаю- щие в себя проверку полноты и непротиворе- чивости базовых протоколов и проверку инва- риантности свойств. Система успешно применялась в ряде прак- тических проектов из области телекоммуника- ции, встроенных систем, телематики и др. Ко- личество требований, формализованных в виде базовых протоколов, достигало 10 000, а коли- чество атрибутов – в пределах 1000. Методика использования системы включает в себя ряд технологий для верификации систем и генера- ции тестов. Одна из типичных технологий применяется для проверки полноты и непротиворечивости базовых протоколов. Два базовых протокола на- зываются непротиворечивыми, если при любой конкретизации этих протоколов их предусловия не могут быть одновременно истинными. Проти- воречивость двух протоколов означает, что для некоторых состояний выбор протокола, который применяется в этих состояниях, происходит не- детерминированным образом. Этот недетерми- низм может быть нежелательным, и система со- общает о противоречивости (предупреждение) разработчику. Система базовых протоколов на- зывается полной, если для любого конкретного состояния существует хотя бы один базовый протокол, применимый в этом состоянии. Не- полнота системы базовых протоколов означает возможность тупикового состояния (dead lock). В вышеприведенной формулировке условия непротиворечивости и полноты проверяются статически путем анализа предусловий базо- вых протоколов с использованием дедуктив- ных средств. На самом деле непротиворечи- вость и полноту следует проверять не на всех состояниях, а лишь на достижимых из множе- ства начальных состояний системы. Если эти состояния можно описать формулой базового языка, то снова можно применить статическую проверку этих свойств, включив их в соответ- ствующие формулы. Если система непротиворечива и полна, про- верка закончена. Если же найден случай проти- воречия или неполноты и он не принят разра- ботчиком в силу того, что не ясно, достижимо ли соответствующее состояние, то возникает но- вая задача – проверка недостижимости условия, выражающего нарушение требования непроти- воречивости или полноты. Поскольку недости- жимость условия означает инвариантность его отрицания, то можно снова применить статичес- кий анализ, пытаясь доказать соответствующие свойства. Если это удается, задача решена, в про- тивном случае можно пытаться усилить соответ- ствующие свойства либо применить динамичес- кую верификацию, т.е. конкретную или сим- вольную генерацию трасс, пытаясь доказать или опровергнуть достижимость искомых свойств. 12 УСиМ, 2012, № 6 Инсерционные машины Для реализации инсерционных моделей не- которого класса используется интерпретатор моделей, который называется инсерционной ма- шиной. Инсерционная машина состоит из трех основных компонент:  Модельный драйвер. Эта компонента уп- равляет движением модели по дереву ее пове- дения, вычисляя переходы из текущего в новое состояние.  Анфолдер поведений агентов. Текущее со- стояние модели представляется в виде алгебра- ического выражения в расширенной алгебре по- ведений. Входной язык допускает использова- ние рекурсивных определений для описания по- ведений агентов и структур данных или состо- яний среды. Анфолдер поведений использует эти описания для того, чтобы получить разло- жение состояния в виде выражения E[u1, u2, ], где E – неразложимое состояние среды.  Интерактор среды. Приводит состояние среды к нормальной форме .i i i I E a E     , используя описание функции погружения. После приведения к нормальной форме драй- веру модели остается только выбрать направ- ление движения i  I и осуществить переход i a EE i или остановиться, если    . Различаются два типа инсерционных машин: машины реального времени или интерактив- ные машины и аналитические инсерционные машины. Машины реального времени работа- ют в реальной или виртуальной среде, взаимо- действуя с внешней средой в реальном време- ни. Аналитические машины используются для анализа моделей, исследования их свойств, ре- шения задач на инсерционных моделях и т.п. Соответственно модельные драйверы также де- лятся на интерактивные и аналитические. Ин- терактивный драйвер после нормализации со- стояния должен выбрать один переход и вы- полнить его путем передачи своего действия во внешнюю среду. Интерактивная машина с учетом внешнего наблюдателя функционирует как агент, погруженный во внешнюю среду с функцией погружения, определяющей законы функционирования этой среды. Внешняя сре- да, например, может изменить поведенческий префикс состояния внутренней среды в соот- ветствии со своей функцией погружения. Интерактивный драйвер организован доста- точно сложно. Он может иметь критерии успеш- ного функционирования и работать как интел- лектуальная система, собирая информацию о прошлом, создавая модель внешней среды и улучшая алгоритмы принятия решений по вы- бору действий с целью повышения уровня ус- пешности своего функционирования. Кроме то- го, интерактивный драйвер может иметь интер- фейс для обмена физическими сигналами с внеш- ней средой (например, прием визуальной или акустической информации, информации о по- ложении в пространстве и т.п.). Аналитическая инсерционная машина, в про- тивоположность интерактивной, может рассмат- ривать различные варианты принятия решений о действиях, возвращаясь в точки выбора и рас- сматривая различные пути в дереве поведения системы. Модель системы может включать в се- бя также и модель внешней среды для этой сис- темы. В общем случае аналитическая машина осуществляет поиск состояний, обладающих за- данными свойствами (достижимость целевых состояний), или состояний, в которых заданные свойства нарушаются. Внешняя среда аналити- ческой машины может быть представлена поль- зователем, взаимодействующим с машиной, фор- мулируя задачи и управляя активностью маши- ны. Аналитические машины, обогащенные ло- гикой и дедуктивными средствами, использу- ются для символьного моделирования систем. Система VRS, помимо инсерционной маши- ны, использующей специализированный вход- ной язык описания требований и специфика- ций, содержит средства для статического ана- лиза инсерционных моделей, генерации тесто- вых наборов, генерации кода и ряд других средств, поддерживающих разработку распре- деленных взаимодействующих систем. Сегодня в Институте кибернетики им. В.М. Глушкова ведется работа над созданием новой системы инсерционного моделирования УСиМ, 2012, № 6 13 IMS (Insertion Modeling System). Эта система представляет собой среду для разработки ин- серционных машин различного типа. Она со- держит ряд прототипов инсерционных машин с различными типами функций погружения и средствами их развития. Базовой системой про- граммирования для IMS является система ал- гебраического программирования APS, обеспе- чивающая гибкость и эффективность при раз- работке новых инсерционных машин. В статье, представленной в этом выпуске, описана инсерционная машина для доказатель- ного программирования. Она ориентирована на верификацию императивных аннотированных программ, использующих различные языки про- граммирования. Когнитивные архитектуры Когнитивные архитектуры или интеллекту- альные агенты – это активно развивающееся в последнее время направление в искусственном интеллекте. Его цель – построение модели че- ловеческого разума, обладающей такими же универсальными возможностями. В отличие от специализированных систем искусственного ин- теллекта, способных эффективно решать спе- цифические классы задач, когнитивные архи- тектуры должны адаптироваться к различным новым, часто неожиданным ситуациям, возни- кающим в результате взаимодействия с внеш- ней средой, обучаться, ставить цели, улучшать свое поведение и т.п. Недавно возникло новое направление BICA (Biologically Inspired Cogni- tive Architectures – биологически мотивиро- ванные когнитивные архитектуры) [32]. В рам- ках этого направления было выполнено сравне- ние большого количества существующих архи- тектур, выделены основные черты, которыми должны обладать такие архитектуры, ежегодно проводятся конференции, собирающие специа- листов из различных областей, заинтересован- ных в продвижении в этом направлении. Нача- ли исследовать возможность создания когни- тивной архитектуры на основе инсерционного моделирования и авторы этой статьи. Наши представления в краткой форме могут быть выражены следующим образом. Инсер- ционная когнитивная архитектура – это инсер- ционная машина, которая осознает себя, имеет центр оценки успешности своего поведения и стремится к многократному достижению мак- симального успеха. Как агент эта машина по- гружена в свою внешнюю среду и имеет сред- ства взаимодействия с ней. Внутренняя среда создает и совершенствует свою модель и мо- дель внешней среды и населяющих ее агентов. Все эти модели строятся как многоуровневые инсерционные среды. Для достижения своих це- лей она использует основные механизмы, вы- работанные в области биологически мотивиро- ванных когнитивных архитектур, а также в об- ласти инженерных проектов, поддерживающих решение сложных интеллектуальных задач. Уверенность в правильности нашего направ- ления основана на следующих гипотезах:  Многоуровневая инсерционная среда может быть с успехом использована для моделирова- ния шести уровней неокортекса (коры голов- ного мозга). Двигаясь от нижних уровней к выс- шим, повышается уровень абстракции, переходя к все более абстрактным символьным моделям. Агенты, погруженные в среды верхнего уров- ня, покрывают классы моделей нижнего уровня.  Человеческий разум должен содержать ме- ханизмы, подобные драйверам инсерционных машин, позволяющие активизировать модели внешних и внутренних сред, произведенные в результате накопления жизненного опыта, обу- чения и унаследованные генетически.  Когнитивная архитектура функционирует как инсерционная машина реального времени, осознавая себя с помощью внутренней среды самого верхнего уровня. Эта среда управляет всеми средами (агентами) нижнего уровня, ак- тивизируя или тормозя их деятельность. Аген- ты всех уровней работают параллельно и неза- висимо до тех пор, пока не попадают под кон- троль сред верхних уровней, осуществляя мо- бильные погружения в них. Заключение. Основной областью примене- ния инсерционного моделирования есть верифи- кация технических систем, однако потенциаль- ные возможности этого направления далеко не исчерпываются этой областью. Инсерционное моделирование можно рассматривать как одно 14 УСиМ, 2012, № 6 из направлений, призванное унифицировать об- щую теорию взаимодействия в распределен- ных системах, и допускающую применения в других прикладных областях. В первую оче- редь следует назвать возможные применения в биологической и экономической информатике. 1. Gilbert D.R., Letichevsky A.A. A universal interpreter for nondeterministic concurrent programming languages / M. Gabbrielli (Ed.) // Fifth Compulog network area meeting on language design and semantic analysis me- thods, Sept. 1996. 2. Letichevsky A., Gilbert D. A general theory of action lan- guages // Кибернетика и системный анализ, 1998. – № 1. – С. 16–36. 3. Letichevsky A., Gilbert D. Interaction of agents and en- vironments / D. Bert, C. Choppy (Eds.) // Resent trends in Algebraic Development technique, LNCS 1827. – Berlin: Springer-Verlag, 1999. – P. 311–328. 4. Глушков В.М. Теория автоматов и вопросы проек- тирования структур цифровых машин // Кибернети- ка. – 1965. – № 1. – С. 3–11. 5. Glushkov V.M., Letichevsky A.A. Theory of algorithms and descrete processors / J.T. Tou (Ed.). // Advances in Information Systems. Science. – Plenum Press, 1969. – 1.–P. 1–58. 6. Капитонова Ю.В., Летичевский А.А. Математиче- ская теория проектирования вычислительных сис- тем. – М.: Наука, 1988. – 295 с. 7. Milner R. A Calculus of Communicating Systems // Lec- ture Notes in Comp. Sci. – Springer-Verlag, 1980. – 92 р. 8. Milner R. Communication and Concurrency. – Pren- tice Hall, 1989. – 250 р. 9. Milner R. The polyadic π-calculus: a tutorial, Tech. Rep. ECS–LFCS–91–180, Laboratory for Foundations of Comp. Sci., Department of Comp. Sci. – University of Edinburgh, UK (1991). 10. Hoare C.A.R. Communicating Sequential Processes. – New Jersey: Prentice Hall, 1985. – 238 р. 11. Bergstra J.A., Klop J.W. Process algebra for synchro- nous communications // Information and Control. – 1984. – 60. – N 1/3. – P. 109–137. 12. Handbook of Process Algebra / J.A. Bergstra, A. Ponce, S.A. Smolka (Eds.) – North-Holland, 2001. – 1342 p. 13. Rutten G. Coalgebras and systems, TCS 249. – Р. 31–52. 14. Hoare C.A.R., Jifeng He. Unifying Theories of Program- ming. – Hemel Hempstead: Prentice Hall, 1999. – 295 р. 15. Meseguer J. Conditional rewriting logic as a unified model of concurrency // Theoretical Comp. Sci., 1992. – 96. – P. 73–155. 16. Leveraging UML to deliver correct telecom applica- tions in UML for Real: Design of Embedded Real-Time Systems / S. Baranov, C. Jervis, V. Kotlyarov et. al. / L. Lavagno, G. Martin, B. Selic (Eds.). – Kluwer Acad. Publ., 2003. –P. 323–342. 17. Validation of Embedded Systems / J. Kapitonova, A. Le- tichevsky, V. Volkov et al. R. Zurawski (Ed.) // The Embedded Systems Handbook. – Miami: CRC Press, 2005. – P. 6–57. 18. Basic Protocols, Message Sequence Charts, and the Verification of Requirements Specifications / A. Leti- chevsky, J. Kapitonova, A. Letichevsky (Jr.) et al. // Comp. Networks, Elsevier. – Amsterdam, 2005. – P. 662–675. 19. Спецификация систем с помощью базовых прото- колов / А.Ад. Летичевский, Ю.В. Капитонова, В.А. Волков и др. // Кибернетика и системный ана- лиз. – 2005. – № 4. – С. 3–21. 20. Semantics of timed MSC language / A.A. Letichevsky, J.V. Kapitonova, V.P. Kotlyarov et al. // Kibernetika and System Analysis, 2002. – N 4. – P. 3–14. 21. Летичевский А.А., Капитонова Ю.В. Инсерционное моделирование // Пр. міжнар. конф. «50 років Інститу- ту кібернетики ім. В.М. Глушкова НАН України». – К.: ИК имени В.М. Глушкова НАН Украины, 2008. – С. 293–301. 22. Спецификация систем с помощью базовых прото- колов / А.А. Летичевский, Ю.В. Капитонова, В.А. Вол- ков и др. // Кибернетика и системный анализ. – 2004. – № 4. – С. 3–26. 23. Bradfield J., Stirling C. Modal Logic and mu-Calculi: An introduction / J.A. Bergstra, A. Ponce, S.A. Smolka (Eds.) // Handbook of Process Algebra. – North-Hol- land, 2001. – 1342. – P. 293–330. 24. ITU-T. Z.120 Recommendation Z.120 (11/99): Lan- guages for telecommunications applications – Message Sequence Charts (MSC), 1999. – 129 р. 25. Insertion modeling in distributed system design / A.A. Le- tichevsky, J.V. Kapitonova, V.P. Kotlyarov et al. // Про- блеми програмування, 2008. – № 4. – C. 13–38. 26. Свойства предикатного трансформера системы VRS / А.А. Летичевский, А.Б. Годлевский, А.А. Летичев- ский (мл.) и др. // Там же. – 2010. – № 4. – С. 3–16. 27. Letichevsky A. Algebra of behavior transformations and its applications / V.B. Kudryavtsev, I.G. Rosenberg (Eds.) // Structural theory of Automata, Semigroups, and Univer- sal Algebra, NATO Science Series II. Mathematics, Phy- sics and Chemistry – Springer, 2005. – 207. – P. 241–272. 28. Semantics of Message Sequence Charts / A.A. Letichev- sky, J.V. Kapitonova, V.P. Kotlyarov et al. // SDL Fo- rum, 2005. – P. 117–132. 29. ITU-T. Z.100 Recommendation Z.100 – Specification and Description Language (SDL), 1999. – 200 р. 30. Object Management Group, Unified Modeling Lan- guage Specification, 2.0. – 2003. – 240 p. 31. http://bicasociety.org/ 32. Roggenbach M., Majster-Cederbaum M. Towards a uni- fied view of bisimulation: a comparative study // TCS. – 2000. – 238. – P. 81–130. Тел. для справок: +38 044 526-0058 (Киев) © А.А. Летичевский, 2012 

Инсерционное моделирование

Institution

Ähnliche Einträge