Алгебраическая теория взаимодействия и киберфизические системы

Розглянуто нову модель кібер-фізичних систем, яка узагальнює відомі моделі типу гібридних та часових автоматів. Обговорюються питання застосування методів моделювання та верифікації, накопичених в області програмування, до розробки кібер-фізичних систем....

Full description

Saved in:

Bibliographic Details
Date:	2017
Main Author:	Летичевский, А.А.
Format:	Article
Language:	Russian
Published:	Інститут кібернетики ім. В.М. Глушкова НАН України 2017
Series:	Проблемы управления и информатики
Subjects:	Методы обработки информации
Online Access:	https://nasplib.isofts.kiev.ua/handle/123456789/208596
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:	Алгебраическая теория взаимодействия и киберфизические системы / А.А. Летичевский // Проблемы управления и информатики. — 2017. — № 5. — С. 37-55. — Бібліогр.: 34 назв. — рос.

Institution

Digital Library of Periodicals of National Academy of Sciences of Ukraine

id	irk-123456789-208596
record_format	dspace
spelling	irk-123456789-2085962025-11-03T01:12:38Z Алгебраическая теория взаимодействия и киберфизические системы Алгебраїчна теорія взаємодії і кібер-фізичні системи Algebraic interaction theory and cyber-physical systems Летичевский, А.А. Методы обработки информации Розглянуто нову модель кібер-фізичних систем, яка узагальнює відомі моделі типу гібридних та часових автоматів. Обговорюються питання застосування методів моделювання та верифікації, накопичених в області програмування, до розробки кібер-фізичних систем. A new model of cyber-physical systems is considered. The model generalizes known models like hybrid and time automata. The application of modeling and verification methods accumulated in the field of programming to the development of cyberphysical systems is discussed. 2017 Article Алгебраическая теория взаимодействия и киберфизические системы / А.А. Летичевский // Проблемы управления и информатики. — 2017. — № 5. — С. 37-55. — Бібліогр.: 34 назв. — рос. 0572-2691 https://nasplib.isofts.kiev.ua/handle/123456789/208596 519.68 10.1615/JAutomatInfScien.v49.i9.10 ru Проблемы управления и информатики application/pdf Інститут кібернетики ім. В.М. Глушкова НАН України
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	2017
topic_facet	Методы обработки информации
url	https://nasplib.isofts.kiev.ua/handle/123456789/208596
citation_txt	Алгебраическая теория взаимодействия и киберфизические системы / А.А. Летичевский // Проблемы управления и информатики. — 2017. — № 5. — С. 37-55. — Бібліогр.: 34 назв. — рос.
series	Проблемы управления и информатики
work_keys_str_mv	AT letičevskijaa algebraičeskaâteoriâvzaimodejstviâikiberfizičeskiesistemy AT letičevskijaa algebraíčnateoríâvzaêmodíííkíberfízičnísistemi AT letičevskijaa algebraicinteractiontheoryandcyberphysicalsystems
first_indexed	2025-11-03T02:06:30Z
last_indexed	2025-11-04T02:05:15Z
_version_	1847823607636426752
fulltext	© А.А. ЛЕТИЧЕВСКИЙ, 2017 Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 37 МЕТОДЫ ОБРАБОТКИ ИНФОРМАЦИИ УДК 519.68 А.А. Летичевский АЛГЕБРАИЧЕСКАЯ ТЕОРИЯ ВЗАИМОДЕЙСТВИЯ И КИБЕР-ФИЗИЧЕСКИЕ СИСТЕМЫ Введение Термин «кибер-физическая система» (cyber-physical system — cps) стал попу- лярным сравнительно недавно. Он использовался в контексте четвертой промыш- ленной революции наряду с такими популярными терминами, как «интернет ве- щей», «облачные вычисления» и др. Кибер-физические системы — это системы, в которых компьютерные программы взаимодействуют с физическими объектами. Такие системы использовались и раньше (встроенные системы, системы управле- ния промышленными объектами и т. п.). В данном случае речь идет о значительно более сложных системах, использующих современные технологии, в том числе интернет и средства его взаимодействия с пользователями [1]. Разработка современных кибер-физических систем активизировала теорети- ческие исследования в области моделирования и верификации таких систем [2, 3]. Основные математические модели, которые используются в настоящее время для ис- следования кибер-физических систем, — это временные и гибридные автоматы [4–6] и их разновидности. Также отмечается, что существующие модели недостаточны для преодоления проблем, возникающих в процессе разработки современных ки- бер-физических систем [1]. К таким проблемам относятся, в частности, проблема масштабируемости (scalability), т.е. возможность работы с распределенными сис- темами, содержащими большое число разнообразных компонент, средства описа- ния параллельных взаимодействующих процессов, проблема сложности алгорит- мов верификации и тестирования, а также ряд других более специфических про- блем. Относительно полный анализ современного состояния теории кибер- физических систем представлен в [7]. В настоящей статье предлагается новая математическая модель для кибер- физических систем, построенная на базе алгебраической теории взаимодействия и технологии инсерционного моделирования. Она отличается более высоким уровнем абстракции по сравнению с другими моделями и, следовательно, позволяет описы- вать более широкий класс систем. В то же время этот уровень абстракции сохраняет возможность строить алгоритмы анализа, синтеза и верификации, а также адаптиро- вать существующие средства для работы с кибер-физическими системами. В основе новой модели лежит понятие полугрупповой транзиционной системы, которое позволяет, в частности, отвлекаться от деталей, связанных с непрерыв- ным течением времени, или от явления интерливинга, присущего функциониро- ванию многоагентных систем. Далее мы показываем, как строить полугрупповые атрибутные среды и их функции погружения. Затем обсуждается структура среды моделирования и основные задачи, которые необходимо решать для построения системы моделирования. Основная идея этих рассмотрений состоит в демонстра- ции возможности перенесения основных приемов технологии инсерционного мо- делирования на область кибер-физических систем. 38 ISSN 0572-2691 Алгебраическая теория взаимодействия Общая теория информационных взаимодействий начинается с нейронных сетей Мак-Каллока Питса (MP43). Теория нейронных сетей привела к появлению теории абстрактных автоматов, которая позволяет изучать поведение и взаимо- действие эволюционирующих систем независимо от их структуры. Первоначаль- но теория автоматов развивалась как теория конечных автоматов, и алгебра Кли- ни–Глушкова [8, 9] служила основным средством описания их поведения. В даль- нейшем теория автоматов концентрировалась на исследовании вопросов анализа и синтеза, изучении обобщений конечных автоматов и на вопросах сложности. Сети из автоматов исследовались в прикладных областях, связанных с проектиро- ванием электронных схем компьютеров. Взаимодействие в явной и общей алгеб- раической форме появилось только в 70-х годах прошлого века как теория взаи- модействующих информационных процессов. Она включает CCS (исчисление взаимодействующих процессов) [10, 11], π-исчисление Милнера [12], CSP (взаи- модействующие последовательные процессы) Хоара [13], ACP (алгебра взаимо- действующих процессов) [14] и много других ответвлений этих базовых теорий. Одновременно начали развиваться модели параллельных вычислений под влиянием практических запросов параллельного программирования. Наиболее абстрактные модели — это сети Петри [15], модели акторов (актеров) [16], а так- же широко распространенные идеи объектно-ориентированного (параллельного) программирования. Они занимают промежуточное место между сетевыми мо- делями (нейронные и автоматные сети, схемы потоков данных) и моделями теории процессов. Инсерционное моделирование сформировалось в 1990-е годы как одно из направлений общей теории взаимодействия. Первоначальное название — модель взаимодействия агентов и сред. Основные понятия инсерционного моделирования (среда, агенты, функция погружения) введены в работах [17–19], опубликованных в 90-х годах. Идейным прототипом инсерционного моделирования следует счи- тать модель взаимодействующих управляющего и операционного автоматов, предложенную В.М. Глушковым еще в 60-х годах прошлого века [20, 21] для опи- сания структур вычислительных машин, а также ее развитие в теории дискретных преобразователей 70-х годов. В этих моделях система представляется в виде ком- позиции двух автоматов — управляющего и информационного. Управляющий ав- томат играет роль агента, а информационный — роль среды, в которую погружен этот агент. Распределенные модели макроконвейерных параллельных вычисле- ний, исследованные в 1980-е годы [22], еще больше приблизились к современной модели взаимодействия агентов и сред. В этих моделях процессы, соответствую- щие параллельно работающим процессорам, можно рассматривать как агенты, взаимодействующие в среде распределенных структур данных. Модели, исследуемые в теории процессов, можно эквивалентным образом представить в виде композиции среды и погруженных в нее агентов. С начала 2000-х инсерционное моделирование становится инструментом разработки прикладных систем, верификации требований и спецификаций распределенных взаимодействующих процессов [23–27]. Система VRS, разработанная в Украине по заказу фирмы Моторола с участием сотрудников Института кибернетики им. В.М. Глушкова, применяется для верификации требований и специфика- ций в области телекоммуникационных систем, встроенных систем и систем ре- ального времени. Новая система инсерционного моделирования IMS [28], разра- ботанная в Институте кибернетики, существенно расширяет область применения инсерционного моделирования. В настоящее время ведутся работы по адаптации этой системы к задачам исследования кибер-физических систем. Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 39 Полугрупповые транзиционные системы Размеченные транзиционные системы. Базовое понятие классической теории взаимодействия — размеченная транзиционная система. Она опреде- ляется множеством состояний S, множеством действий А (в зависимости от приложений употребляются также термины сигналы, метки, обозреваемые символы, операторы, сообщения) и отношением переходов .SASG ××⊆ Вы- сказывание Gsas ∈′),,( так же, как и сама тройка ),,( sas ′ (переход системы), обозначается выражением ,ss a ′⎯→⎯ а конечная или бесконечная последова- тельность сопряженных переходов вида ...... 121 21 ⎯⎯ →⎯⎯→⎯⎯→⎯⎯→⎯ +nn a n aaa sss называется историей функционирования системы. Два перехода сопряжены, если первый из них оканчивается в состоянии, в котором начинается второй. Последо- вательность действий ......21 naaa называется трассой, порожденной данной исто- рией. Именно трассы служат основой построения инвариантов эквивалентности состояний транзиционных систем. Трассовая эквивалентность состояний опреде- ляется как равенство множеств трасс, порождаемых историями, которые начина- ются в этих состояниях, а бисимуляционная эквивалентность — как эквивалент- ность деревьев трасс, которые растут из этих состояний. Трассы в дискретных моделях рассматриваются как элементы свободной полугруппы слов ,∗A порожденной множеством действий. Единица этой полу- группы (пустое слово) может использоваться для разметки так называемых «скрытых» переходов. Модели систем, построенные на размеченных транзиционных системах, бу- дем называть дискретными моделями. Обычно они привязываются к дискретному времени, хотя множества состояний и действий могут быть бесконечными и даже континуальными. В то же время при рассмотрении физических (технических) систем могут использоваться вещественные параметры, которые изменяются не- прерывным образом и которые желательно включать в модель системы на соот- ветствующих уровнях абстракции. В этом случае история может включать в себя непрерывные компоненты, которые не могут быть однозначно разделены на дис- кретную последовательность переходов и действий. Для того чтобы охватить эти обстоятельства, предлагается новый тип транзиционных систем. Полугрупповые транзиционные системы. Так же, как и размеченная тран- зиционная система, полугрупповая транзиционная система состоит из трех ком- понент ,,, >< GHS где S — пространство состояний, H — полугруппа трасс (на- блюдаемых процессов полугрупповой транзиционной системы), G — параметри- зованное отношение переходов. В отличие от размеченной транзиционной системы отношение переходов параметризуется временными параметрами: }.\|{ R⊆∈××⊆= TtSHSgG t Здесь Т — множество моментов времени, которое предполагается аддитивной подполугруппой полугруппы R вещественных чисел по сложению. Будем использовать следующие обозначения: .),,()( ,),,( t h tt h gshsТtss gshsss ∈′∈∃⇔′⎯→⎯ ∈′⇔′⎯→⎯ 40 ISSN 0572-2691 Параметр t перехода ss t h ′⎯→⎯ называется его длительностью. Не исключа- ются переходы длительности 0. Компоненты полугрупповой транзиционной сис- темы должны удовлетворять следующим аксиомам: ).,(),,(,,.4 ..3 ).(),()(.2 .,.1 ssshhhshhTttssA sssssA ssSsHhSsA TttTttA t h t h tt h tt hh t h t h h ′⎯→⎯′′⎯→⎯′′′=′′′′′∃⇒∈′′⎯→⎯ ′′⎯⎯→⎯⇒′′⎯→⎯′⎯→⎯ ′⎯→⎯∈′∈∃∈∀ ∈′+⇒∈′ ′ ′′′ ′+ ′′+ ′ ′ ′ Аксиома А1 называется аксиомой полугруппы. Она выражает тот факт, что Т — полугруппа, а время направлено в сторону увеличения. В частности, если по- лугруппа Т имеет хотя бы один положительный элемент, то она бесконечна «вправо», т.е. имеет сколь угодно большие значения. С другой стороны, если в Т есть хотя бы один отрицательный элемент, она бесконечна также и «влево», т.е. имеет сколь угодно большие по модулю отрицательные значения. Примерами полу- групп моментов времени, которые используются в приложениях, могут служить следующие подгруппы: — всех вещественных чисел (обычно рассматривается как группа); — всех натуральных чисел (целых положительных); — неотрицательных целых чисел; — Z всех целых рациональных чисел (положительных, отрицательных, а также 0); — всех вещественных чисел вида xδ , где Z;∈>δ x,0 — всех неотрицательных вещественных чисел, больших некоторого .0>δ Использование этой полугруппы позволяет избегать парадоксов Зенона, связан- ных с делением конечных интервалов на бесконечное множество отрезков. Аксиома А2 называется аксиомой продолжения. Из этой аксиомы следует, что любая история в полугрупповой системе может быть продолжена. Таким об- разом, вместо тупиковых состояний в полугрупповой системе могут быть непод- вижные точки. Аксиома А3 называется аксиомой свертывания. Она показывает, что любую- конечную историю можно свернуть до одного перехода. В этой аксиоме предпо- лагается, что все переменные связаны неявно квантором общности. Такое предпо- ложение будем делать и в дальнейшем для свободных переменных в формулах, если не указано противное. Аксиома А4 называется аксиомой развертывания. Она показывает, что лю- бой достаточно длинный переход можно развернуть в историю из нескольких пе- реходов. Эту аксиому также можно использовать для восстановления движения в прошлом из движений в настоящем (включая движение в обратном направлении, если полугруппа T содержит отрицательные числа). Мы не исключаем недетер- минированность системы как при движении вперед, так и при движении в обрат- ном направлении. Поэтому разложение перехода большой длительности на пере- ходы меньшей длительности может быть неоднозначным. Полугрупповая система порождает множество историй, конечную или беско- нечную последовательность попарно сопряженных переходов вида ...,... 1 1 2 2 1 1 21 + +⎯⎯ →⎯⎯→⎯⎯→⎯⎯→⎯ n n n n t h nt h t h t h sss а каждая конечная история длины n порождает трассу ,...1 nhh элемент полу- группы трасс. Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 41 Множество параметризированных отношений переходов образует коммута- тивную полугруппу, если умножение определить с помощью формулы ).,(),,(,,( ssshhhshhggshs t h t h tt ′⎯→⎯′′⎯→⎯′′′′′=′′′′′∃⇔∈′ ′′′ ′ Теорема 1. Для всех ., tttttt gggggTtt ′′+′ ==⇒∈′ Доказывается как следствие из аксиом свертывания и развертывания. Дейст- вительно, из tt ggshs ′∈′),,( следует посылка аксиомы свертывания и включение .tttt ggg ′+′ ⊆ Пусть теперь .),,( ttgshs ′+∈′ Тогда по аксиоме развертывания и определению произведения имеем .),,( tt ggshs ′∈′ Первое равенство доказано, второе следует из коммутативности полугруппы ).( ttttT +′=′+ Таким образом, полугруппа отношений переходов есть коммутативная полу- группа. Если полугруппа отношений переходов имеет неприводимую систему об- разующих, то ее можно построить путем определения переходов, принадлежащих образующим этого отношения, а затем замкнуть путем добавления произведений. Примеры полугрупповых систем. Рассмотрим некоторые важные примеры полугрупповых транзиционных систем. Размеченные транзиционные системы. Пусть S — размеченная транзици- онная система со множеством действий Y и отношением переходов .ss y ′⎯→⎯ По- ложим ...},,2,1{== NT в качестве полугруппы трасс Н возьмем свободную по- лугруппу, порожденную множеством Y, и определим переход за единицу времени полугрупповой системы >< GHS ,, соотношением .,1 ssYhss hh ′⎯→⎯∈⇔′⎯→⎯ Переходы произвольной длительности определим рекурсивно соотношением ).,,(),,( 11 snsshzhSsHhYzss hz n h ′⎯→⎯′′⎯→⎯′=∈′′∈′∈∃⇒′⎯→⎯ ′ + Множество G однозначно определяется отношением переходов ,1g которое явля- ется единственным образующим полугруппы параметризированных отношений переходов. Именно это отношение обычно и берут в качестве определения отно- шения переходов размеченной транзиционной системы. Для моделирования скрытых переходов нужно взять свободную полугруппу с единицей, и использовать эту единицу для разметки скрытых переходов. Фазовые потоки. Для описания фазовых потоков, используемых в теории динамических систем, следует абстрагироваться от полугруппы трасс. Поэтому, чтобы не терять общности, полагаем }{ε=H (единичная полугруппа) и трассы на переходах не пишем. Отношение переходов предполагается функциональным, т.е. отношение переходов — это преобразование множества состояний: ).(, ,)(,:, 0 sgssss s ssgSSgT ttt t =′′→⇔′⎯→⎯ =→= ε R Теорема 2. Полугруппа отношений переходов для фазового потока — ком- мутативная группа преобразований множества S, а отношения переходов взаим- но-однозначны. Единицей группы переходов служит преобразование ,0g произведение оп- ределяется равенствами ,tttt ggg ′+′ = обратный элемент .1 tt gg − − = Частными случаями фазовых потоков являются полугрупповые транзиционные системы с многомерными евклидовыми пространствами nR в качестве множества состоя- ний, переходами, определяемыми с помощью групп диффеоморфизмов или сис- темами обыкновенных дифференциальных уравнений, разрешенных относитель- но первых производных. 42 ISSN 0572-2691 Полугрупповые гибридные автоматы Основное определение гибридного автомата принадлежит Т. Хенцингеру [5]. В литературе используются различные модификации. В качестве альтернативного определения гибридного автомата рассмотрим понятие полугрупповой системы, достаточно близкое к оригинальному определению Хенцингера. Назовем эту сис- тему полугрупповым гибридным автоматом. Полугрупповой гибридный автомат представляет собой параллельную ком- позицию двух транзиционных систем. Эта композиция будет рассматриваться как полугрупповая транзиционная система. Одна из систем композиции — обычная размеченная система со множеством действий (событий по терминологии Хен- цингера) .Σ Она играет роль управляющей системы, другая — непрерывная ди- намическая система (управляемая компонента), обладающая несколькими режи- мами функционирования. Переключение режимов функционирования определя- ется управляющей системой. Полугруппа моментов времени 0≥= RT — множество неотрицательных ве- щественных чисел, состояния всей системы ,SV ×⊆S где V — множество со- стояний управляющей компоненты, ,2DS = ,XD R= }...,,,{ 21 mxxxX = — множество вещественных переменных, определяющих фазовое пространство не- прерывной части гибридного автомата, полугруппа H — свободная полугруппа с единицей ,ε порожденная множеством событий .Σ Пространство XR использу- ется вместо традиционного ,mR во-первых, чтобы подчеркнуть, что порядок на множестве переменных Х не играет роли, и, во-вторых, чтобы использовать эти переменные в логических формулах в качестве атрибутов для определения свойств областей фазового пространства. Состояния управляющей компоненты определяют режимы функционирования непрерывной компоненты, ее переходы vv ′⎯→⎯σ соответствуют переключениям режимов от v к .v′ Состояния непрерывной компоненты представляют собой пары .),( 2Duus ∈= & Первый элемент пары определяет положение u компоненты в фазовом пространстве, второй — скорость в точке u. Переходы за время t непрерывной компоненты гиб- ридного автомата определяются условием: ⇔′⎯→⎯ε ),(),( svsv t существует диф- ференцируемая функция Dt →ϕ ],0[: такая, что ),())(),(()()(()0(,))(),((,))0(),0(( vflowvinvtstts ∈τϕτϕ∧∈τϕ<τ<∀′=ϕϕ=ϕϕ &&& где inv и flow — теоретико-множественные функции Хенцингера, определенные на состояниях управляющей системы: .2:,2: 2DD →→ VflowVinv Класс всех дифференцируемых функций, определенных на интервале ],0[ t и удов- летворяющих вышеуказанному условию (1), обозначим tvF , и будем называть их свидетелями перехода ).,(),( svsv t ′⎯→⎯ε Заметим, что переход ),(),( 0 svsv ⎯→⎯ε логически следует из определения переходов управляемой компоненты. Переходы управляющей компоненты в составе гибридного автомата опреде- ляют смену режимов. Они осуществляются за нулевое время и определяются сле- дующим условием: ),(),(),(),( 0 σ∈′∧′⎯→⎯⇔′′⎯→⎯ σσ jumpssvvsvsv Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 43 где 2 2: S→Σjump — еще одна теоретико-множественная функция Хенцингера. Переходы непрерывной компоненты и переходы смены режимов будем рас- сматривать как переходы, порождающие параметризированное отношение пере- ходов полугруппового автомата. Теперь строим это отношение индукцией по длине трасс, полагая , 0 )(U ∞ = = n n tt gg где },,\|)},(),{()0( SsVvsvsvg tt ∈∈′⎯→⎯= ε },),,(),(),(),(\|),(),{( 0 )1( tttsvsvsvsvsvsvg tttt =′′+′′′⎯→⎯′′′′⎯→⎯′′⎯→⎯′′⎯→⎯= ′′ εσ ′ εσ .1},),,(),(),(\|),(),{()()1( ≥=′′+′′′⎯→⎯′′′′⎯→⎯′′⎯→⎯∪= ′ σ ′′ σ+ ntttsvsvsvsvsvgg tt h t hn t n t Переменные ,,,, sstt ′′′′′′′′ фигурирующие в условиях, определяющих свойства пе- реходов, предполагаются связанными квантором существования. Теперь все ком- поненты полугрупповой системы определены и для доказательства того, что сис- тема соответствует определению полугрупповой системы, осталось показать ис- тинность ее аксиом. В соответствии с определением параметризированного отношения переходов любой переход системы можно представить в виде конечной истории, в которой чередуются переходы непрерывной компоненты, имеющие длительность, отлич- ную от нуля, и переходы смены режимов, имеющие нулевую длительность. Начи- наться и кончаться эта история может как переходом непрерывной компоненты, так и переходом смены режима. Такие представления назовем стандартными разложениями переходов гибридного автомата. Докажем аксиомы гибридного автомата, рассматриваемого как полугрупповая система. Аксиома продолжения следует из того, что ).,(),( 0 svsv ⎯→⎯ε Для доказательства аксиомы свертывания для истории ),(),(),( svsvsv t h t h ′′′′⎯→⎯′′⎯→⎯ ′ ′ следует рассмотреть четыре случая стандартных разложений первого и второго переходов и провести доказательство индукцией по сумме длин историй для этих переходов. 1. Первая история кончается, а вторая начинается сменой режимов. Тогда эти смены можно представить в виде ).,(),(),(),(),( 11011110011 svsvsvsvsv ′′′′⎯⎯ →⎯′′⇒′′′′⎯→⎯′′⎯→⎯′′ σ ′′σ′σ ′′σ′ Выполнив соответствующую подстановку, сократим длину первой истории. 2. Первая история кончается сменой режимов, а вторая начинается переходом непрерывной компоненты: ).,(),(),(),(),( 111111011 svsvsvsvsv tt ′′′′⎯→⎯′′⇒′′′′⎯→⎯′′⎯→⎯′′ ′′ σ′ ′′ εσ′ Соответствующая подстановка сократит длину второй истории. 3. Первая история кончается переходом непрерывной компоненты, а вторая начинается сменой режимов. Рассматривается аналогично предыдущему случаю. Сокращается длина первой истории. 44 ISSN 0572-2691 4. Первая история кончается, а вторая начинается переходом непрерывной компоненты: ).,(),(),(),(),( 1111112111 2121 svsvsvsvsv tttt ′′′′⎯→⎯′′⇒′′′′⎯→⎯′′⎯→⎯′′ + εεε Действительно, пусть свидетель первого перехода — функция ,ϕ а второго — функция .ψ Тогда функция );( ψϕ=ξ — свидетель композиции двух переходов. Функция ξ определена на интервале ],0[ 21 tt + так, что .),()(,0),()( 21111 ttttt +≤τ<−τψ=τξ≤τ≤τϕ=τξ Оператор (( );( )) склеивает графики двух функций и называется последовательной графической их композицией. Базис индукции получается, если каждая из исто- рий состоит из одного перехода. Для доказательства аксиомы развертывания полезна следующая лемма. Лемма. Для любых ).),(),(),((),(),(,, svsvsvssvsvTtt tttt ′⎯→⎯′′⎯→⎯′′∃⇒′⎯→⎯∈′ ′ εε ′+ ε Переход ),(),( svsv tt ′⎯→⎯ ′+ ε означает существование функции ., ttvF ′+∈ϕ Но эта же функция будет свидетелем перехода )),(,(),( tvsv t ϕ⎯→⎯ε а функция ,ψ определенная на интервале ],0[ t ′ так, что ,0),()( ttt −′≤τ≤τ+ϕ=τψ является свидетелем перехода ).,())(,( svtv t ′⎯→⎯ϕ ′ ε Таким образом, следствие в утвержде- нии леммы будет истинным при ).)(),(( tts ϕϕ=′′ & Лемма доказана. Он позволяет разделить любой переход непрерывной компоненты в последовательность из двух переходов в любой момент времени протекания исходного перехода. Для доказательства аксиомы развертывания рассмотрим стандартное разло- жение перехода .0,),,(),( >′′′⎯→⎯ ′+ ttsvsv tt h Стандартное разложение — это конечная история. Префикс истории — это последовательность переходов, которые стоят в начале этой истории. Пусть t ′′ — минимальная длительность префикса рассматриваемого разложения, большая или равная t. Сворачивая префикс дли- тельности t ′′ и оставшуюся часть истории в один переход, получим разложение ).,(),(),( svsvsv ttt h t h ′′⎯→⎯′′′′⎯→⎯ ′′−′+ ′′ ′′ ′ Возможны два случая: ., tttt >′′=′′ В первом случае искомое разложение получе- но. Во втором случае в силу минимальности t ′′ получим, что в интервале ],[ tt ′′ смена режимов не происходила. Поэтому, используя лемму 1, получаем разложение ).,(),(),(),( svsvsvsv ttt h ttt h ′′⎯→⎯′′′′⎯→⎯′′′′′⎯→⎯ ′′−′+ ′′ −′′ ε′ Наконец, свернув переходы после t, получим разложение ),,(),(),( svsvsv t h t h ′′⎯→⎯′′′′′⎯→⎯ ′ ′′′ что и требовалось доказать. Таким образом, рассмотренная конструкция гибридного автомата действи- тельно есть полугрупповая система. Сравнение с автоматом Хенцингера. Полугрупповой гибридный автомат отличается от автомата Хенцингера в нескольких аспектах. Во-первых, в качестве областей значений функций inv, flow и jump у Хенцингера используются предикаты, у нас — множества, на которых эти предикаты истинны. Это различие несущественно. Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 45 Более существенно различие в выборе состояний непрерывной компоненты. У Хен- цингера это точка фазового пространства, в полугрупповом автомате состояние включает в себя скорость, что позволяет более свободно манипулировать исто- риями функционирования гибридного автомата. В частности, при моделировании многоагентных систем реального времени часто возникает вопрос о синхронизации модельного времени. Аксиомы свертывания и развертывания позволяют решать эту задачу более просто по сравнению с автоматом Хенцингера. В работе [5] рассматривается два варианта гибридного автомата. Один вариант связывается со свойством безопасности (safety semantics), другой — со свойством жизненности (liveness semantics). Первый вариант ближе всего подходит к понятию полугруппового гибридного автомата. Во втором варианте множество трасс сокра- щается путем исключения бесконечных трасс, имеющих конечную длительность (эффект парадоксов Зенона). Для полугрупповых систем это свойство можно обеспе- чить более конструктивным образом, поэтому опускаем эти рассмотрения. Полугруппы трасс. Рассмотрим некоторые классы полугрупп трасс, которые важны для приложений. Свободные полугруппы. Традиционно используются для построения трасс при моделировании программных систем. Символы образующих такой полугруппы связываются с операторами, которые выполняются программой. При этом мы аб- страгируемся как от времени, которое требуется для выполнения оператора, так и от содержания самого оператора. Свободная полугруппа с единичным элементом (моноид) может использоваться для моделирования трасс со скрытыми переходами. При моделировании кибер-физических систем переходы, размеченные образующими свободной полугруппы (дискретные переходы), обычно чередуются с переходами в непрерывном времени. Частично коммутативные полугруппы. Это такие полугруппы, часть обра- зующих которых удовлетворяет соотношению перестановочности. Перестановочные символы обычно соответствуют операторам, не связанным информационно. Использование соотношений перестановочности позволяет преобразовывать модели параллельных программ для уменьшения интерливинга (значительно уменьшается число трасс, которые необходимо рассматривать для решения проблемы достижимости). Технику оптимизации интерливинга можно перенести и на модели кибер-физических систем. Полугруппы операторов присваивания. Последовательность операторов присваивания эквивалентна одному параллельному присваиванию. В сочетании с условными присваиваниями используются для сворачивания трасс при доказа- тельствах свойств программ. Дискретные абстракции трасс в непрерывном време- ни эквивалентны условным присваиваниям. Поэтому такие полугруппы могут ис- пользоваться и для доказательства свойств кибер-физических систем. Полугруппы с непрерывным временем. Элементы таких полугрупп проще всего порождать с помощью функций ),))(,0[: YhLh → заданных на полуоткры- тых временных интервалах }.\|{),[ btaTtba <<=∈= Умножение в таких полу- группах задается соотношениями ).()()()),(())(( ),(),())(( hLhLthLhLththh hLtththh ′+<≤−′=′∗ <=′∗ Полугруппы с непрерывным временем удобно, в частности, использовать для моделирования нейронных сетей с непрерывными сигналами. Другой пример — среди вещественных переменных гибридного автомата можно выделить множество наблюдаемых переменных и рассмотреть полугруппу трасс, порожденную фрагмен- тами непрерывного изменения этих переменных на полуоткрытых интервалах. 46 ISSN 0572-2691 Эквивалентность и алгебра поведений Модели реальных систем используются для исследования их поведений. Поведение системы связано с некоторой эквивалентностью. Именно две системы эквивалентны, если они имеют одно и то же поведение. Алгебра поведений харак- теризует поведения систем и позволяет производить вычисления, необходимые для порождения трасс и доказательства свойств систем. Эквивалентность. Полугрупповая система может рассматриваться как обычная размеченная транзиционная система, действия которой есть элементы полугруппы H, а переходы размечены временными параметрами так, что выпол- няются аксиомы полугрупповой системы. Если длительности переходов перенести в действия, т.е. рассматривать в качестве действий пары ,,),,( TtGhth ∈∈ то получим дискретную систему, а эквивалентность состояний дискретной системы можно перенести на исходную полугрупповую систему. Понятия трассовой и биси- муляционной эквивалентности, а также алгебра поведений определены для дискрет- ных систем. Остается перенести эти понятия на полугрупповые системы. Рассмотрим эту ситуацию более подробно. Состояния полугрупповых тран- зиционных систем так же, как и в дискретном случае, рассматриваются с точно- стью до трассовой или бисимуляционной эквивалентности. Трассовая эквивалентность. Сначала рассмотрим трассовую эквивалент- ность. Функционирование полугрупповой системы так же, как и в обычном слу- чае характеризуется историями, т.е. конечными или бесконечными последова- тельностями сопряженных переходов. Пусть nt h t h ss n n⎯→⎯⎯→⎯ ...1 1 0 — конечная история функционирования полугрупповой системы. Нормированной трассой, порожденной этой историей, назовем пару )....,...( 11 nn tthh ++ Пусть )(sL — множество всех нормированных трасс, порожденных исто- риями, которые начинаются в состоянии s. Состояния s и s′ называются трассо- во эквивалентными, если )()( sLsL ′= . Любую конечную историю полугрупповой системы можно свернуть в один переход, длительность которого равна сумме длительностей переходов этой истории. Пусть )}(\|{)( ssshsg t h t ′⎯→⎯′∃= — мно- жество переходов длительности t, которые начинаются в состоянии s. Теорема 3. Имеет место следующая эквивалентность: )).()()(()()( sgsgTtsLsL tt ′=∈∀⇔′= Формула )),()()(( sgsgTt tt ′=∈∀ смысл которой состоит в том, что все полу- групповые разметки переходов одинаковой длительности для двух состояний совпадают, представляет собой необходимое условие трассовой эквивалентности. Докажем достаточность. Пусть ).(),( sLth ∈ Если свернуть историю, порож- дающую эту трассу, получим историю )( ss t h ′⎯→⎯ длины 1, трасса которой должна принадлежать множеству ).(sL ′ Теорема доказана. Таким образом, рассматривая состояния полугрупповой системы с точностью до трассовой эквивалентности, абстрагируемся от состояний. Условие трассо- вой эквивалентности теоремы 3 позволяет абстрагироваться и от представле- ния элементов полугруппы трасс на историях с сохранением временных ха- рактеристик трасс. Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 47 Бисимуляционная эквивалентность слабее трассовой и определяется более тонким образом. Именно, бинарное отношение R на множестве состояний полу- групповой системы назовем отношением бисимуляции (bisimulation), если для любой пары ),( ss ′ состояний имеют место следующие утверждения: ).),((),()2 ),),((),()1 rsRrrrrsRss rsRrrrrsRss t h t h t h t h ⎯→⎯∧∈′∃⇒′⎯→⎯′∧∈′ ′⎯→⎯′∧∈′′∃⇒⎯→⎯∧∈′ Состояния s и s′ полугрупповой системы называются бисимуляционно экви- валентными (bisimilar), если существует отношение бисимуляции R такое, что .),( Rss ∈′ Обычно в системах выделяется множество начальных состояний, и в этом случае система называется инициальной. Когда речь идет об инициальной систе- ме, в определение отношения бисимуляции нужно добавить еще требование: если Rss ∈′),( и одно из этих состояний является начальным, то и другое тоже. Эквивалентность систем (трассовая или бисимуляционная), как правило, определяется эквивалентностью их состояний. Для инициальных систем две системы объявляются эквивалентными, если каждое начальное состояние одной из них эквивалентно некоторому начальному состоянию другой. Различие ме- жду трассовой и бисимуляционной эквивалентностью проявляется только для случая недетерминированных систем. Полугрупповая система называется де- терминированной, если она имеет только одно начальное состояние и из ss t h ′⎯→⎯ и ss t h ′′⎯→⎯ следует, что s′ и s ′′ эквивалентны. Две детерминиро- ванные системы бисимуляционно эквивалентны тогда и только тогда, когда они трассово эквивалентны. Поведение размеченной транзиционной системы является инвариантом экви- валентности состояний. Для конструктивного определения поведений строится алгебра поведений и поведения рассматриваются как решения систем уравнений вида )(xFx = в этой алгебре ( ...),,( 21 xxx = допускается и бесконечное множе- ство уравнений и неизвестных). Полугрупповая алгебра поведений для полугрупповых транзиционных сис- тем строится так же, как и алгебра поведений для их дискретных моделей: двух- основная алгебра, основное множество — поведения, другое множество — дейст- вия. Две операции: префиксинг ua. и недетерминированный выбор vu + (а — действие, u и v — поведения), две константы 0 (тупиковое поведение) и ⊥ (неоп- ределенное поведение). На алгебре поведений определяется частичный порядок с наименьшим элементом .⊥ Недетерминированный выбор — это ассоциативная, коммутативная и идемпотентная операция. Единственным отличием полугруппо- вой алгебры поведений является то, что на множестве действий определена полу- групповая операция. В связи с этим в полугрупповой алгебре поведений возникает еще одно тождество: .).(.. uabuba = Для вычисления поведений нужна полная алгебра поведений (каждое на- правленное множество имеет наименьшую верхнюю грань). Конструкция полной полугрупповой алгебры поведений повторяет конструкцию, описанную в [29] для размеченных транзиционных систем. Теперь можно решать уравнения в алгебре поведений и определить поведение системы в заданном состоянии. 48 ISSN 0572-2691 Пусть задана некоторая полугрупповая система. Сопоставим каждому состоя- нию s поведение )(sbeh системы в этом состоянии. Поведения — это элементы полу- групповой алгебры поведений. Эти поведения удовлетворяют системе уравнений: ∑ ∑ ∈ ′⎯→⎯ ′= Tt ss t h sbehthsbeh .)().,()( Это бесконечная система, однако при достаточно конструктивном задании переходов она может использоваться для последовательного порождения историй и трасс. Для полугрупповой алгебры поведений может быть доказана теорема о связи поведений с бисимуляционной эквивалентностью состояний. Теорема 4. Два состояния полугрупповой системы бисимуляционно эквива- лентны, если и только если их поведения совпадают. Доказательство практически повторяет доказательство соответствующей теоремы для обычной алгебры поведений, оно здесь не приводится. Теорема 4 позволяет нормализовать транзиционные системы путем представления их состоя- ний в виде выражений алгебры поведений. Для решения некоторых задач вместо бисимуляционной эквивалентности лучше использовать более сильную трассовую эквивалентность. Важнейший при- мер такой задачи — задача распознавания достижимости некоторого свойства со- стояний транзиционной системы. Для трассовой эквивалентности в качестве ал- гебры поведений используется алгебра, которая получается из алгебры поведений добавлением тождества дистрибутивности: ...).( vauavua +=+ Если заменить операцию префиксинга последовательной композицией поведений, то получим хорошо известную алгебру Клини. Выражения этой алгебры определяют множества трасс, порождаемых состояниями транзиционных систем. Алгебру поведений обычно обогащают, добавляя новые операции, которые определяются с помощью систем уравнений. К стандартным обогащениям отно- сятся последовательная и параллельная композиции. Атрибутные полугрупповые среды Полугрупповые транзиционные системы так же, как и временные или гиб- ридные автоматы, удобно использовать для моделирования простейших систем, состоящих из небольшого числа управляемых (непрерывных) и управляющих (дискретных) компонент. Для моделирования более сложных распределенных многоуровневых систем с большим числом взаимодействующих компонент необ- ходимо использовать дополнительные средства, позволяющие моделировать структурные свойства таких систем. В технологии инсерционного моделирования такими средствами являются средства описания взаимодействия агентов и сред. Атрибутная полугрупповая среда. Строится так же, как и атрибутная среда в инсерционном моделировании. Среда и агенты суть полугрупповые транзиционные системы, а их композиция определяется с помощью функции погружения. Описание среды представляет собой набор функциональных символов (сигнатура) многосорт- ного языка исчисления предикатов, который используется для описания свойств сис- темы (базовый логический язык). В приложениях инсерционного моделирования к верификации софтверных систем используется язык первого порядка, возможно, дополненный некоторыми модальностями темпоральной логики и lambda- выражениями для определения функционалов высших порядков. При использовании объектно-ориентированного программирования (ООП) описание среды реализуется описанием класса (для многоуровневых сред это может быть иерархия классов разных типов), а различные типы агентов, погруженных в соответствующие среды, определяются объектами своих классов (классов агентов). Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 49 Функциональные символы делятся на интерпретированные и неинтерпре- тированные. Интерпретированные символы не меняют свою интерпретацию в те- чение функционирования системы (например, арифметические операции и функ- ционалы, функции, определенные с помощью компьютерных программ (методов при использовании объектно-ориентированного программирования) и т.п.). Неин- терпретированные символы, которые называются атрибутами, изменяют свою интерпретацию с течением времени. Они определяют состояние системы. При моделировании кибер-физических систем удобно различать непрерывные и дис- кретные атрибуты. Непрерывные атрибуты меняют свои значения непрерывно с течением времени, дискретные — только в моменты выполнения действий, кото- рые эти значения изменяют. В остальные моменты времени они сохраняют значе- ния, полученные при последнем изменении. Простые атрибуты (функциональные символы арности 0) меняют свои значения целиком, функции меняют значения в конечном множестве точек для дискретных атрибутов или областей (для непре- рывных функциональных атрибутов). Для описания функции погружения (взаимодействие агентов и сред) исполь- зуются локальные описания (по другой терминологии — базовые протоколы). Общая форма локального описания остается традиционной: ).)()()(( xxPxxВ β>→<α∀= Здесь х — список переменных простых типов (параметры локального описания), )(xα и )(xβ — формулы базового языка (пред- и постусловия), причем )(xβ может содержать операторы присваивания и другие операторы, равносильные операторам вызова методов или процедур. Эти операторы рассматриваются как формулы темпоральной логики, которые связывают значения атрибутных выра- жений после выполнения оператора с их значениями до выполнения оператора. К ним, в частности, относятся операторы, которые изменяют законы эволюции непрерывных атрибутов. Процесс )(xP определяет наблюдаемый переход системы, как элемент полугруппы трасс, и длительность этого перехода. Локальное описание системы определяет ее свойство, которое неформально можно описать следующим образом. Пусть система, представленная в виде ком- позиции атрибутной полугрупповой среды и погруженных в нее агентов, нахо- дится в состоянии s. Тогда если для некоторого набора значений параметров x на состоянии s истинно предусловие ),(xα то по истечении времени, определяемого процессом ),(xP система перейдет в новое состояние ,s′ на котором будет ис- тинным условие ).(xβ При этом переходе будет наблюдаем элемент полугруппы трасс атрибутной среды, определяемый процессом ).(xP Локальные описания можно рассматривать двояким образом. С одной сторо- ны, это формула, которая определяет некоторое свойство системы. С другой сто- роны, локальное свойство определяет множество разметок переходов системы для некоторого класса ее состояний или недетерминированный оператор на множест- ве состояний среды. Когда локальное описание используется в таком качестве, на- зываем его базовым протоколом. Базовые протоколы используются для порождения историй и трасс атрибут- ной среды. Возможны два подхода для решения этой задачи. Первый называется конкретным, второй — символьным моделированием. В первом случае имеем де- ло с конкретными состояниями атрибутной среды, т.е. такими состояниями, в ко- торых все атрибуты, необходимые для вычисления предусловия, заданы точно. Новое состояние также должно быть конкретным. Переход вычисляется для кон- 50 ISSN 0572-2691 кретного набора значений параметров. Для вычисления перехода должны быть заданы алгоритмы решения двух задач: вычисление предусловия и выбор кон- кретных значений атрибутов среды, таким образом, чтобы постусловие было ис- тинным на новом состоянии среды. Переход возможен только при истинном зна- чении предусловия и существовании состояния, на котором истинно постусловие. При символьном моделировании состояние среды определяется свойствами этой среды, выраженными на базовом логическом языке. Условием применимо- сти перехода является выполнимость конъюнкции формулы текущего состояния среды и предусловия локального описания. Для выполнения перехода используется предикатный трансформер — преобразование формулы исходного состояния в формулу, определяющую возможные новые состояния. Подробные описания предикатных трансформеров для дискретных сред и достаточно широкого класса формул представлены в [27]. Для полугрупповых атрибутных сред описания преди- катных трансформеров предполагается представить в дальнейших публикациях. Пример. Для иллюстрации основных понятий атрибутной полугрупповой среды рассмотрим простейший пример. Это слегка модифицированная модель термостата из статьи [5]. Среда состоит из дискретного атрибута l:enum (on, off) перечислимого типа, непрерывного атрибута x:real, интерпретированных функций символьного типа Fon: symb – > symb, Foff: symb – > symb, вещественных констант delta 0 < = delta1 и оператора z: = evolution (z0, F)while(u). Атрибут l представляет два режима работы термостата: on (включен) и off (выключен). Режимами управляет контроллер, агент, погруженный в среду термостата, [delta 0, delta 1] — интервал переключения контроллера. Атрибут x представляет непрерывно изменяющееся состояние термостата (температуру) как функцию времени. Если y — символ вещественного переменного, то Fon(y) и Foff(y) суть алгебраические выражения, которые определяют функции от y. Они используются для определения эволюции термостата с помощью оператора z: = evolution(z 0, F(z)) while(u(z)). Семантика этого оператора определяется сле- дующим образом. Пусть f: T – > R — решение уравнения F(z)z =& с начальным условием z(0) = z0. Тогда закон эволюционирования атрибута z меняется от пре- дыдущего на новый закон z(t) = f(t). При этом новый закон определен на макси- мальном интервале, на котором выполняется условие u(z). В примере Хенцингера Fon(y)=5 – 0,1x, Foff= – 0,1x. Функция погружения контроллера в среду термостата определяется следую- щими локальными описаниями: Launchon: Forall (t, tau) ( t = current time, delta < = tau < = delta1 & x < 19 – >< after tau (l: = on) > l: = on, x: = evolution (x(t + tau), Fon(x)) while(x < = 22) ); Launch off: Forall(t, tau) ( t = current time, delta < = tau < = delta1 & x > 21 – >< after tau (l: = off) > l: = off, x: = evolution(x(t + tau), Foff(x)) while(x > = 18) ) В описании этого примера использован шрифт и синтаксис ввода информа- ции в систему IMS. Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 51 Непрерывный атрибут current time управляется средой и обычно обозначает время активации базового протокола, который обращается к этому атрибуту. От- считывается от начала вызова первого протокола, с которого начинается генера- ция текущей трассы. Для данного примера это может быть и относительное вре- мя, отсчитываемое от предыдущего переключения режима работы термостата. Момент времени t+tau служит моментом окончания предыдущего перехода среды и началом нового перехода со сменой режима. Таким образом, если в начальном состоянии термостата x(0)<=18.1, а закон его эволюции определяется уравнением 0,=x& то история функционирования термостата будет иметь вид ...30 : 322 0 : 2110 : 11 22 110 ssss sssss onl taut offl taut onl tau ⎯⎯ →⎯⎯→⎯′⎯→⎯ ⎯⎯ →⎯⎯→⎯′⎯→⎯⎯⎯ →⎯⎯→⎯ =εε =εε=ε С помощью аксиомы свертывания эту историю можно преобразовать в ...4 : 3 : 2 : 1 : 1 3322110 sssss taut offl taut onl taut offl tau onl + = + = + == ⎯⎯ →⎯⎯⎯ →⎯⎯⎯ →⎯⎯⎯ →⎯ Приведенные базовые протоколы могут служить как для конкретного, так и для символьного моделирования. Конкретное моделирование может служить в основном для теоретических исследований. К недетерминизму приводит уже, ска- жем, выбор момента времени переключения режимов. Важную роль играет точ- ность вычислений, ошибки округления, устойчивость решений и другие факторы. Поэтому при моделировании кибер-физических систем предпочтением пользуют- ся символьные методы вычислений. В этом примере недетерминизм проявляется только в выборе задержки tau при выполнении переключения режимов. При конкретном моделировании доста- точно рассмотреть нижнее, верхнее и среднее значения tau. При символьном мо- делировании в формуле состояния будет фигурировать только одно неравенство для tau. Для остальных непрерывных величин current time и х также будут спра- ведливы ограничения, которые следуют из ограничений для tau. Моделирование полугрупповой среды. Основная задача моделирования со- стоит в порождении трасс, удовлетворяющих заданным условиям, по модели сис- темы. Эти условия могут определять свойства заключительных состояний трасс (целевые состояния, goal states), их максимальные длительности, условия продол- жения или отсечения трасс, условия безопасности (safety) и т.п. Рассмотрим атрибутную среду, заданную системой локальных описаний. Для такой среды удобно сначала построить ее абстракцию, рассматривая базовые про- токолы как действия. Полученная модель называется крупношаговой моделью. Полугруппа трасс для крупношаговой модели — это свободная полугруппа с еди- ницей, порожденная базовыми протоколами. Базовые протоколы рассматривают- ся как неделимые сущности, параллельные композиции базовых протоколов вы- полняются по правилу интерливинга. Недетерминизм остается только в выборе следующего протокола для исполнения. Каждая трасса крупношаговой модели после ее завершения превращается в мелкошаговую трассу путем раскрытия процессов, содержащихся в базовых протоколах, и преобразовании одного пере- хода в последовательность переходов, совершаемых при выполнении действий процессов базовых протоколов. Затем строится мелкошаговая трасса, которая преобразуется в соответствии с тождествами соответствующей полугруппы (обычно это частично-коммутативная полугруппа). Семантика мелкошагового моделирования для дискретных систем представлена в [25]. 52 ISSN 0572-2691 Состояние среды в общем случае имеет вид ...],,,[ 21 uuE где Е — неразло- жимое состояние среды, ...,,, 21 uu — состояния агентов, погруженных в среду. Неразложимость состояния среды означает, что ее нельзя представить в виде не- тривиальной композиции среды и агентов, погруженных в нее. При символьном моделировании состояние среды представляет собой формулу базового логиче- ского языка, определяющую ограничения на атрибуты среды и атрибуты агентов для многоуровневой структуры системы. Будем предполагать, что все непрерыв- ные атрибуты суть атрибуты среды и они изменяют свое состояние непрерывно в соответствии с установленными для них законами эволюции, а изменение этих законов выполняется с помощью операторов типа evolution. Эти операторы могут задавать закон эволюции явно или неявно в виде уравнений или в виде ограниче- ний, которым должны удовлетворять эти законы. Первая задача, возникающая при моделировании среды, состоит в выборе протокола, который будет выполняться первым. С каждым базовым протоколом связаны атрибутные выражения, которые этот протокол использует и которые он изменяет. В случае дискретного времени в каждый момент проверяется примени- мость всех базовых протоколов и выбираются протоколы, которые могут быть выполнены в этот момент времени. В случае непрерывного времени примени- мость протоколов в идеале должна проверяться непрерывно. Это можно обеспе- чить путем приближенных оценок, проверяя условия применимости с некоторым малым шагом по времени. В силу того, что вычисления с вещественными числами выполняются приближенно, результаты моделирования будут зависеть от вре- менного кванта и, уменьшая его, можно получать все более точные результаты, хотя при этом будет увеличиваться количество трасс и соответственно сложность вычислений. Более эффективная проверка может быть выполнена путем решения задачи вычисления или оценки минимального времени, когда предусловие рассматри- ваемого протокола может быть выполнимо на заданном состоянии среды в это время. Время применимости протокола зависит только от законов эволюции непре- рывных атрибутов, которые используются или изменяются в данном протоколе. Другой метод состоит в том, чтобы встроить проверку определенных условий в законы эволюции непрерывных величин. В моменты, когда выполняются эти условия, включаются проверки всех предусловий, которые могут быть выполни- мы. Реализовать этот метод можно путем декомпозиции закона эволюции на от- резки, вставив на границах этих отрезков передачу сообщения среде о необходи- мости проверки применимости некоторых протоколов. В приведенной выше мо- дели термостата оператор эволюции можно заменить более сложным оператором. Для протокола launchon это может быть x: = evolution ((x (t+tau), Fon(x)) while(x>21); check point; continue while(x < = 22)). Получив сообщение checkpoint, среда включает протокол launch on, если l = off, или launch off, если l = on. Наконец, уменьшить количество проверок можно путем введения отношения следования на множестве базовых протоколов и введения двухуровневого управ- ления моделью. Используемые методы двухуровневой генерации трасс для дис- кретных систем представлены в [27]. Они без труда переносятся на кибер- физические системы. Верификация моделей. Модель может выражать требования к системе и то- гда мы рассматриваем задачу верификации требований. Нас могут интересовать полнота и непротиворечивость требований, сохранение свойств безопасности и достижимость состояний, удовлетворяющих определенным требованиям. Эти же Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 53 вопросы могут интересовать нас и в случае, когда модель построена по уже суще- ствующей системе и тогда нарушение определенных свойств модели может озна- чать их нарушение и в системе. Особый случай представляют модели, выражен- ные в виде программ в языках высокого уровня. Для разных классов моделей ме- тоды верификации могут быть разными. Рассмотрим два подхода (статический и динамический) в том виде, как они применяются в системе IMS. Статическая верификация. Обычно статическая верификация состоит в том, что по модели строятся некоторые логические формулы и общезначимость таких формул означает, что нужные свойства будут выполняться и для любой правильной реализации модели. Начало статическим методам положено работами Хоара и Флойда [30, 31], современные реализации [32] используют метод кон- трактного программирования. К статическим методам относят также абстрактную интерпретацию [33]. В системе IMS требования формализуются в виде локальных описаний. Две главные задачи верификации, которые рассматриваются в IMS, — это про- верка свойств безопасности (safety) и проверка достижимости свойств. Для формулировки свойств состояний среды с погруженными в нее агентами исполь- зуются формулы базового языка модели (формулы многосортного исчисления предикатов первого порядка). Свойство безопасности — это свойство, которое сохраняется на протяжении всего времени функционирования системы, на- пример, некоторые величины непрерывных компонент должны удовлетворять определенным неравенствам, уравнениям и т.д. Для выполнения свойства безопасности достаточно, чтобы оно сохранялось каждым базовым протоколом. Точнее, пусть ))()()(( xxPxxВ β>→<α∀= — базовый протокол, а γ — свойство безопасности. Тогда должно выполняться условие ))),(),(()(( xxprxx βα∧γ→α∧γ∀ где pr — предикатный трансформер, о котором говорилось выше. Условие со- хранения является достаточным, но не необходимым условием безопасности. Просто одно из состояний, в котором нарушается условие сохранения, может быть недостижимым. Статические методы могут применяться также для доказательства недости- жимости некоторых условий. Условие недостижимо, если его отрицание является условием безопасности. Если не удается доказать безопасность или недостижи- мость, то приходится прибегать к динамическим методам. Динамическая верификация состоит в выполнении модели путем конкрет- ного или символьного моделирования (генерация трасс). В процессе выполнения модели проверяются условия безопасности и целевые условия. В случае, когда модель имеет конечное число состояний, полная верификация может быть дос- тигнута исчерпывающим прохождением всех состояний. Эта техника использует- ся в области проверки моделей [34] с языком темпоральной логики в качестве языка спецификаций. Основная область применения — верификация автоматных моделей технических устройств или конечных моделей программ, использующих достаточно высокий уровень абстракции. Для динамической верификации моде- лей с бесконечным множеством состояний невозможно осуществить исчерпы- вающее прохождение всех состояний, но, порождая все трассы ограниченной длины, можно найти нарушение условий безопасности или достижение целевых состояний. В IMS динамическая верификация выполняется путем символьного моделирования для моделей, заданных в виде систем базовых протоколов с ис- пользованием различных средств сокращения пространства поиска (количества генерируемых трасс и состояний). Различные уровни абстракции достигаются вы- бором формул для начальных состояний. 54 ISSN 0572-2691 Заключение Основной результат статьи состоит в рассмотрении новой модели кибер- физических систем, которая обобщает известные модели типа гибридных и вре- менных автоматов. После соответствующей адаптации эта модель может быть положена в основу дальнейшего развития систем инсерционного моделирования и их использования для разработки алгоритмов моделирования, верификации и тестирования многоагентных кибер-физических систем с многомерными непре- рывными компонентами. В остальном статья носит обзорный характер, обсужда- ются вопросы применения методов моделирования и верификации, накопленных в области программирования, к разработке кибер-физических систем. О.А. Летичевський АЛГЕБРАЇЧНА ТЕОРІЯ ВЗАИМОДІЇ І КІБЕР-ФІЗИЧНІ СИСТЕМИ Розглянуто нову модель кібер-фізичних систем, яка узагальнює відомі моделі типу гібридних та часових автоматів. Обговорюються питання застосування методів моделювання та верифікації, накопичених в області програмування, до розробки кібер-фізичних систем. A.A. Letichevsky ALGEBRAIC INTERACTION THEORY AND CYBER-PHYSICAL SYSTEMS A new model of cyber-physical systems is considered. The model generalizes known models like hybrid and time automata. The application of modeling and verification methods accumulated in the field of programming to the development of cyber- physical systems is discussed. 1. Khaitan S.K, McCalley J.D. Design techniques and applications of cyber physical systems : survey // IEEE Systems Journal. — 2014. 2. Lee E.A. and Seshia S.A. Introduction to embedded systems, a cyber-physical systems approach. — Cambridge : MIT Press, 2017. — 564 p. 3. Alur R. Principles of cyber-physical systems. — Cambridge : MIT Press, 2015. 4. Raskin J.F. An introduction to hybrid automata // in Hristu-Varsakelis / Dimitrios ed. // Hand- book of Networked and Embedded Control Systems. — 2005. — P. 491–517. 5. Henzinger T.A. The theory of hybrid automata in Inan, M. Kemal and Kurshan R. P. ed. // Verifi- cation of digital and hybrid systems. — Berlin; Heidelberg : Springer, 2005. — P. 265–292. 6. Bengtsson J. and Yi W. Timed automata: semantics, algorithms and tools, in Desel J., Reisig W. and Rozenberg G. // Lectures on Concurrency and Petri Nets: Advances in Petri Nets. — Berlin; Heidelberg : Springer, 2004. — P. 87–124. 7. Летичевский А.А., Летичевский А.А. мл., Скобелев. В.Г., Волков В.В. Кибер-физические системы // Кибернетика и системный анализ. — 2017 — № 6. — C. 3–19. 8. Kleene, Stephen C. Representation of events in nerve nets and finite automata, in Shannon, Claude E.; McCarthy, John // Automata Studies. — Princeton University Press. — 1956. — P. 3–42. 9. Глушков В.М., Об одном алгоритме синтеза абстрактных автоматов // Украинский матема- тический журнал. — 1960 — 12, № 2. — C. 147–156. 10. Milner R.A. Calculus of communicating systems // Lecture Notes in Computer Science. — N.Y. : Springer-Verlag, 1980. — 92. 11. Milner R. Communication and concurrency. — N.Y. : Prentice Hall, 1989. 12. Milner R. The polyadic π-calculus: a tutorial. : Tech. Rep. ECS—LFCS—91—180. Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edin- burgh, UK. — 1991. Международный научно-технический журнал «Проблемы управления и информатики», 2017, № 5 55 13. Hoare C.A.R. Communicating sequential processes. — New Jersey : Prentice Hall, 1985. 14. Bergstra J A. and Klop J.W. Process algebra for synchronous communications // Information and Control. — 1984. — 60 (1/3). — P. 109–137. 15. Petri C.A. Kommunikationmit automaten. — Bonn : Institut fur InstrumentelleMathematik, Schriften des IIM. — 1962. — N 2. 16. Carl Hewitt, Peter Bishop, and Richard Steiger. A universal modular actor formalism for artifi- cial Intelligence, IJCA, 1973. 17. Letichevsky A.A., Gilbert D.R. : A universal interpreter for nondeterministic concurrent program- ming languages, in M. Gabbrielli, ed. // Fifth Compulog network area meeting on language design and semantic analysis methods. — 1996. 18. Letichevsky A. and Gilbert D. A general theory of action languages // Cybernetics and Systems Analysis. — 1998. — N 1. 19. Letichevsky A. and Gilbert D. A model for interaction of agents and anvironments, in D. Bert, C. Choppy, P. Moses, ed. Recent trends in Algebraic Development Techniques // Lecture Notesin Computer Science . — 1999. — 1827. 20. Глушков В.М. Теория автоматов и вопросы проектирования структур цифровых машин // Кибернетика. — 1965. — № 1 — C. 3–12. 21. Glushkov V.M. and Letichevsky A.A., Theory of algorithms and discrete processors // Advances in Information Systems Science. — N. Y. : Plenum Press. — 1969. — 1. — P. 1–58. 22. Капитонова Ю.В., Летичевский А.А., Математическая теория проектирования вычисли- тельных систем. — М. : Наука, 1988. — 295 с. 23. Baranov S., Jervis C., Kotlyarov V., Letichevsky A., and Weigert T. Leveraging UML to deliver correct telecom applications in UML for Real: Design of Embedded Real-Time Systems by L.Lavagno, G. Martin, and B. Selic, ed. — Kluwer : Academic Publishers, 2003. — P. 323–342 24. Kapitonova J., Letichevsky A., Volkov V. and Weigert T. Validation of embedded systems, in R., Zurawski, ed. // The embedded systems handbook. — Miami : CRCPress, 2005. 25. Летичевский А. Ад., Капитонова Ю.В., Волков В.А., Летичевский А.А., Баранов С.Н., Кот- ляров В.П., Вейгерт Т. Спецификация систем с помощью базовых протоколов // Киберне- тика и системный анализ. — 2005. — № 4. — C. 3–21. 26. 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 // Computer Networks. — 2005. — 47. — P. 662–675. 27. Letichevsky, A.A. Letychevskyi O.A., Peschanenko V.S., Weigert T. Insertion modeling and sym- bolic verification of large systems // Lecture Notes in Computer Science. — 2015 — 9369. — P. 3–18. 28. Letichevsky A.A., Letychevskyi O.A. and Peschanenko V.S. Insertion Modeling System LNCS. — 2015. — 7162. — P. 262–272. 29. Letichevsky A. Algebra of behavior transformations and its applications in V.B. Kudryavtsev and I.G. Rosenberg, ed. // Structural theory of automata, emigroups, and universal algebra, NATO Science. Series II. Mathematics, Physics and Chemistry. — 2005. — 207. — P. 241–272. 30. Hoare C. A. R. An axiomatic basis for computer programming // Communications of the ACM. — 1969. — 12(10) — P. 576–580, 583. 31. Floyd R. Assigning meanings to programs. In Mathematical Aspects of Computer Science // Pro- ceedings of Symposia in Applied Mathematics. — American Mathematical Society, Providence, Rhode Island. — 1967. — 19. — P. 19–32. 32. https://www.microsoft.com/en-us/research/pro-ject/boogie-an-intermediate-verification-language, 2008. 33. Patrick Cousot. Abstract interpretation based formal methods and future challenges // Informat- ics, 10 years back — 10 years ahead, R. Wilhelm, ed. // Lecture Notes in Computer Science. — 2001. — 2000. — P. 138–156. 34. Edmund M. Clarke and Qinsi Wang. 32 years of model checking. International Andrei Ershov. Memorial Conference on Perspectives of System Informatics, PSI 2014: Perspectives of System Informatics. — 2014. — P. 26–40. Получено 19.06.2017

Алгебраическая теория взаимодействия и киберфизические системы

Institution

Similar Items