автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.18, диссертация на тему:Моделирование многокомпонентных систем при помощи взаимодействующих X-машин

На правах рукописи (ЗУЧО!^-- ■

Соболев Михаил Сергеевич

МОДЕЛИРОВАНИЕ МНОГОКОМПОНЕНТНЫХ СИСТЕМ ПРИ ПОМОЩИ ВЗАИМОДЕЙСТВУЮЩИХ

Х-МАШИН

Специальность 05.13.18 - математическое моделирование, численные методы и комплексы программ

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

1 1 НОЯ 2010

Москва - 2010

004612384

Работа выполнена на кафедре математических основ управления Московского физико-технического института (государственного университета)

Научный руководитель:

доктор физико-математических наук, профессор, член-корреспондент РАН ФЛЁРОВ Юрий Арсениевич

Официальные оппоненты:

доктор физико-математических наук, доцент

ТОРМАСОВ Александр Геннадьевич

кандидат физико-математических наук НОВИК Константин Валерьевич

Ведущая организация:

Институт точной механики и вычислительной техники имени С.А. Лебедева РАН

О

Защита состоится « 2010 года в /0 час. на

заседании диссертационного совета Д 212.156.05 при Московском физико-техническом институте (государственном университете) по адресу: 141700, г. Долгопрудный Московской обл., Институтский пер. д.9, ауд. 903 КПМ.

С диссертацией можно ознакомиться в библиотеке МФТИ (ГУ).

Автореферат разослан

(й/С/и^и. 2010 г.

Ученый секретарь

диссертационного совета / Федько О.С.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы

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

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

Жесткие требования предъявляются также к надежности и производительности многокомпонентных систем - серверным приложениям, на которые приходится большая часть функциональной ' нагрузки в клиент-серверных системах. Кроме того, в серверных приложениях широко используется параллельное программирование, что затрудняет поиск ошибок и оценку производительности. Часто традиционные методы отладки, используемые при разработке клиентских приложений, не обеспечивают должного уровня тестирования.

Математическое описание программной системы и требований к ней позволяет улучшить качество критически важных систем, в частности многокомпонентных.

При моделировании многокомпонентных систем можно выделить два аспекта: моделирование данных и моделирование алгоритмов. Большинство из существующих формальных методов позволяют полно описать только один из этих аспектов. Для моделирования данных обычно используют иерархические, сетевые или реляционные модели, а для описания алгоритмов - модели, основанные на автоматах (машинах состояний): конечные автоматы, автоматы с магазинной памятью, машины Тьюринга.

Одним из немногих методов, позволяющих сочетать достоинства обоих подходов, является моделирование на основании Х-машин. В определении X-машины к состояниям конечного автомата добавляется память, позволяющая хранить типизированные данные. Это дает возможность описывать как динамические, так и статические аспекты системы.

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

Необходимым условием возможности применения рассматриваемого метода на практике является существование достаточно развитого языка для описания систем взаимодействующих Х-машин, а также программного обеспечения для осуществления моделирования динамического поведения системы.

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

Цель работы

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

Таким образом, в работе решаются следующие задачи:

1. Разработка теоретических основ и метода построения систем взаимодействующих Х-машин, допускающих асинхронное взаимодействие между Х-машинами и поэтапное проектирование;

2. Формальная верификация Х-машин, позволяющая осуществлять тестирование компонентов систем взаимодействующих Х-машин;

3. Описание языка для создания спецификаций систем взаимодействующих Х-машин, а также комплекса программ позволяющего моделировать программные системы;

4. Моделирование распределенного хранилища данных с использованием предложенного метода.

Научная новизна

В работе предложен новый эффективный подход к моделированию многокомпонентных систем, основанный на системах взаимодействующих X-машин. По сравнению с существующими методами данный подход обладает следующими достоинствами:

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

2. Возможность построения систем с асинхронной коммуникацией;

3. Возможность формальной верификации компонент системы;

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

Основные положения, выносимые на защиту

1. Математическая модель системы взаимодействующих Х-машин;

2. Метод формальной верификации Х-машин;

3. .Язык для создания спецификаций систем взаимодействующих Х-машин, а также комплекс программ, позволяющий производить моделирование программных систем при помощи таких спецификаций;

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

Теоретическая и практическая ценность

Большинство современных многокомпонентных систем относятся к классу реактивных систем. Это означает, что работа системы заключается в получении объектов-запросов, их обработке и формировании ответов.

В работе предложен и теоретически описан метод поэтапного моделирования и тестирования компонентов подобных систем. Это позволяет существенно повысить их надежность.

Для практического моделирования реактивных систем в работе создан язык XDL и программная библиотека, позволяющая использовать XDL-описания в программах на Java.

Апробация и публикации

Основные результаты диссертации докладывались и обсуждались на следующих научных семинарах и конференциях:

• Научные конференции МФТИ «Современные проблемы фундаментальных и прикладных наук» (Долгопрудный, 2008, 2009);

• IX международная научно-практическая конференция «Исследование, разработка и применение высоких технологий в промышленности» (Санкт-Петербург, 2010);

• Научные семинары кафедры математических основ управления МФТИ (Долгопрудный, 2007- 2010);

• Научный семинар отдела математического моделирования систем проектирования Вычислительного центра РАН (Москва, 2010).

По теме диссертации опубликовано 7 работ, в том числе две работы - в журналах из Перечня изданий, рекомендованных ВАК РФ [5,6].

Структура и объем диссертации

Диссертация состоит из введения, пяти глав, заключения и списка использованных источников. Общий объём работы составляет 110 страниц, список использованных источников содержит 54 наименования.

СОДЕРЖАНИЕ РАБОТЫ

Во ВВЕДЕНИИ обосновывается актуальность темы диссертации, формулируется ее цели, задачи, представляются результаты, выносимые на защиту, а также определяется научная новизна, теоретическая и практическая значимость полученных результатов.

В ГЛАВЕ 1 анализируются существующие методы моделирования многокомпонентных программных систем. Среди них преобладают модели, основанные на типах данных. Несмотря на то, что эти модели значительно облегчают проектирование программного обеспечения, они недостаточны для описания динамического поведения систем. Другие формальные методы, такие как конечные автоматы или сети Петри, подробно описывают динамику системы, но плохо моделируют изменения внутренних данных во время переходов между состояниями. Существуют методы, хорошо описывающие как динамическое, так и статическое поведение системы, например метод диаграмм состояний, однако эти методы недостаточно формализованы. До сих пор нет подхода, позволяющего описывать программные системы достаточно полно и с разумными трудозатратами.

Далее приведено используемое формальное определение Х-машины:

Определение. Х-машиной называется девятка М =(Q,■L,Г,M,Ф,F,q0,MQ,T):

• ¡2 - конечный набор состояний;

• Е, Г- входной и выходной алфавиты соответственно;

• М - память, конечный набор типизированных переменных;

• Ф - конечный набор частичных фунщий ф, отображающих входной символ и содержание памяти в выходной символ и новое содержание памяти ф: £хМ ->ГхМ;

• F — функция, отображающая состояние и функцию из Ф в новое состояние /: £) х Ф —»<2;

• Мо — начальное состояние и начальное содержимое памяти соответственно;

• Т-множество заключительных состояний.

Проведено сравнение вычислительных возможностей автоматных моделей, доказана следующая теорема:

Теорема 1.1. Пусть Есй к Г с П - два конечных алфавита (О. -

* т-1*

внешний алфавит машины Тьюринга), а /: £ —> Г - частичная функция, вычисляемая магииной Тьюринга (МТ). Тогда существует Х-машина, вычисляющая /.

В ГЛАВЕ 2 даётся теоретическое описание системы взаимодействующих Х-машин, Система взаимодействующих Х-машин состоит из нескольких X-машин, которые могут обмениваться сообщениями. Сообщения отправляются и передаются функциями из Ф в процессе работы Х-машины. Чтение входной строки осуществляется Х-машиной путем чтения стандартного входного порта, а запись в выходную строку - путем записи в стандартный выходной порт. Кроме того, каждая Х-машина может иметь коммуникационные порты, количество которых зависит от количества ее связей с другими Х-машинами.

Часто система может включать в себя несколько однотипных Х-машин, различающихся начальным состоянием и начальным содержимым памяти. Для удобства практического моделирования целесообразно разделить описания внутренней структуры Х-машины от описания начальных параметров. Для этого в предлагаемом подходе вводится понятие типа Х-машины. Для преобразования типа Х-машины в Х-машину вводится специальный оператор. В данном методе реализована объектно-ориентированная парадигма, предусматривающая разделение описания внутренней структуры семейства объектов («тип») от описания конкретного объекта («экземпляра типа»). Оператор создания, таким образом, играет роль метода-конструктора.

Определение. Типом Х-машины называется шестерка

ТМ = (<2,£,Г, М,Ф,.Р), определения элементов которой аналогичны определениям соответствующих элементов Х-машины. Х-машина может быть получена из типа Х-машины с помощью оператора, добавляющего к ней начальное состояние: ШБТ'ЛМ-х^^М^^^-^М^ У^- е £>, М ^-е М.

Для того, чтобы полученные Х-машины могли взаимодействовать между собой в составе системы, к ним нужно добавить входные и выходные порты, а также связать эти порты с частичными функциями из Ф. Кроме того, требуется осуществить преобразование множества Ф, для того, чтобы функции-элементы этого множества осуществляли чтение и запись не входных и выходных строк, а входных и выходных портов. Получившийся после этих преобразований объект называется компонентом системы.

Определение. Компонент системы взаимодействующих Х-маишн - это пятерка ХМ С( =(М//},,Ф№;- ,ФОР-), ¡е N где:

' Щ = ^гТ1>М1>ФС^<10А> ^-машина,

соответствующая этому компоненту. Единственное отличие от одиночной Х-машины - частичные функции Ф(- заменены на ФС-

(подробное описание будет дано ниже);

• 1е N-входные порты компонента, ф;- -

стандартный входной порт;

• ОР• = (ор-,ор^ор-2,...„ор-т), те N-выходные порты

компонента ор/ - стандартный выходной порт;

• Ф1Р^:ФС- —» Щ- частичная функция, связывающая функцию из ФС,- с входным портом;

• ФОР- :ФС- —> ОР^ — частичная функция, связывающая функцию из ФС- с выходным портом.

Множество частичных функций ФС-, заменяющее в соответствующей компоненту Х-машине множество Ф(-, можно получить из Ф- путем отбора необходимых элементов. В ФС;- входит четыре типа функций:

1. Функции, принимающие сообщения из стандартного входного порта и записывающие сообщения в стандартный выходной порт:

={^:а//?Ла(фг.)хМ а1р11а{ор^хМ\ф = (сг,т)-^(у,т')е Ф- л ае а!рка{}р-) л /е а1р1ш(ор¡) л (ф ¡р-)е Ф1Р- л (ф —> ор-) е ФОР-}

2. Функции, принимающие сообщения из стандартного входного порта и записывающие сообщения в коммуникационный выходной порт: 5105; ~{ф:а1р!ш(1р;)хМ -> а1р!ш(ор--)хМ I ф = {а,т) -»(у,т )е

I I Iу

Ф - а ¿те а1р}га(1рЛ л /е а1р1га(ори) л -» /р-)е Ф№ л ->

4 I 1] I I

ор1реФОР1л]<т}

3. Функции, принимающие сообщения из коммуникационного входного порта и записывающие сообщения в стандартный выходной порт:

/550- -{ф:а1р!га(1р;;)хМ —> а1р1ш(ор-)хМ Iф~(а,т)-^(у,т')е

11] I

Ф • л сге а1р1га{1р•■) л ^е а1рИа(ор-) л -> 1ри)еФ1Р< л (0 ->

I у I I] I I

ФОР( Aj<l}

4. Функции, принимающие сообщения из коммуникационного входного порта и записывающие сообщения в коммуникационный выходной порт:

= {£>:а]р}ш(1рц)хМ —> а1р!га(ор%)хМ \ф = (а,т) (у,т')е Ф- лее а/р/ш(ф;у) л /е а!рка(ор-^) л (ф -з> гр(у)е Ф/^- /\—> ор^)е л j<mлk<l} Объединяя их, получаем ФС;- = и ¿УС^ и /550- и /505-.

с^—►

коммукшсашоный порт

r~t

КОММуННКЗШОКЬШ

порт

Рис 1. Четыре типа функций компонента системы.

Для наглядного графического изображения используются специальные обозначения: круг и ромб. Круг означает, что функция получает данные из коммуникационного порта, а не из стандартного входного порта. Аналогично, ромб обозначает вывод данных в выходной коммуникационный порт. На рис. 1 представлены четыре возможных типа функций.

Последней стадией моделирования системы является создание связей между портами входящих в систему Х-машин и связей между портами этих X-машин и самой системой:

Определение. Системой взаимодействующих Х-машин называется

• CR с (OPxIP), где ОР= U ОР-, IP ~ (J Щ - коммуникационное

г = 1 г =1

отношение. Если (op,ip)e CR, ope ОР, ipe IP, то это значит, что сообщения из выходного порта компонента ор отправляются во входной порт компонента ip ;

п

п

• IR с (IPSVSJP) - отображение входных портов системы во входные порты компонентов. Если (ip^le,ip)<= IR, ipn!i.£ ipelP, то это

о V«j jJ Л

значит, что сообщения, поступающие во входной порт системы ipsys, транслируются во входной порт компонента ip ;

• OR с (ОР х OPSyS ) -отображение выходных портов компонентов

системы в выходные порты системы. Если (ор,ор__,.)€ OR, ope ОР, ор^1ее то это значит, что сообщения

J Vi j ул sys

из выходного порта компонента ор транслируются выходной порт системы ор Sy$.

Таким образом, можно выделить несколько последовательных шагов описания системы взаимодействующих Х-машин:

1. Описание типов Х-машин, которое может осуществляться независимо от описания системы в целом. Для создания новой системы можно взять ранее описанные типы Х-машин из других систем;

2. Описание отдельных Х-машин. Каждый экземпляр получается из соответствующего типа путем применения оператора INST. При создании индивидуальной Х-машины задается ее начальное состояние и начальное содержимое памяти;

3. Описание коммуникационных портов, соответствующих каждой из Х-машин, и определение связей этих портов с функциями из Ф. Таким образом, полностью определяется набор компонентов, составляющих систему;

4. Описание взаимодействия компонентов путем задания связей между их коммуникационными портами; описание взаимодействия системы с внешним окружением путем создания коммуникационных портов системы и их связывания с портами компонентов;

5. В случае необходимости, может осуществляться расширение

системы путем добавления новых компонентов.

В ГЛАВЕ 3 предложен новый способ формальной верификации X-машин с помощью так называемой логики X-CTL.

Темпоральные логики представляют собой обобщение логики предикатов операторами, использующими понятие времени (модальные операторы). С помощью этих операторов удобно конструировать логические выражения, которые верны в некий определенный момент времени. В литературе предложена и описана темпоральная логика CTL (Computational Tree Logic), которая позволяет описывать системы с ветвлением вычислений. Выражения CTL позволяют представлять знания естественным образом, особенно в случае ветвящихся временных выражений.

В логике CTL вводятся пять временных операторов, определенных на свойствах, которые принимают некоторые значения вдоль пути вычислений (свойствами могут быть как атомарные высказывания, так и другие CTL-выражения):

• Хр: свойство р должно быть истинным в состоянии, непосредственно следующим за начальным;

• Fp: свойство р должно стать истинным хотя бы в одном состоянии в будущем или в текущем состоянии;

• Gp: свойство р должно быть истинным во всех будущих состояниях и в текущем состоянии;

• pUq: свойство q должно выполниться в некотором состоянии в будущем (или, возможно, в текущем состоянии), свойство р должно выполняться во всех состояниях до этого состояния (не включительно);

• pRq: свойство q должно быть истинным во всех состояниях, предшествующих состоянию, в котором станет истинным свойство р, и в самом этом состоянии. В этом случае говорят, что р «освобождает» q. Если р ложно во всех состояниях, то оператор эквивалентен Gq.

Кроме того, существуют два префикса для описания ветвлений в дереве вычислений:

• А/: выражение / верно для всех ветвей вычисления;

• Е /: выражение / верно хотя бы для одной ветви вычислений. Доказана

Теорема 3.1. Любое выражение CTL может быть преобразовано так, что будет содержать только операторы v, —i, X, U и Е.

Логика CTL имеет ограниченную применимость при верификации X-машин, так как ее операторы не учитывают содержимое памяти. Для осуществления формальной верификации Х-машин, в данной работе предлагается дополнить логику CTL. Назовем новую расширенную логику X-CTL. Для того, чтобы верификация Х-машины при помощи логики X-CTL была возможна, требуется установить дополнительное ограничение на значения памяти: множество всех возможных значений каждой переменной в памяти должно быть конечно. Учитывая эти ограничения, введем следующие обозначения:

• М(0), М( 1), ... - переменные в памяти;

• М^ - множество всех возможных значений памяти в состоянии q. Такое множество конечно, и его можно представить в виде

Mq={m°, ..., т\ ..., mk], 0<i<k, где т1=(М1(0), Ml( 1), ...)- i-e возможное состояние памяти;

• Запись qm'j означает, что Х-машина находится в состоянии q j е Q

и при этом память имеет значение тг еМ Á Состояния q - &Q, таким образом, расщепляются на метасостояния qml-.

Обозначим через МРгор множество всех возможных предикатов, состоящих из переменных памяти и атомарных выражений, например, М(1) = 0 или М(3)*2.

В логике X-CTL введем два новых оператора:

• е МРгор) - выражение р верно при любом состоянии памяти;

• тх(ре МРгор) - существует состояние памяти, в котором

выражение р верно.

Введем понятие выражения состояния (ВС), выражения пути вычислений(ВПВ) и выражения в памяти (ВП). Эти типы выражений определяются рекурсивно.

• Если ре МРгор, то р является выражением в памяти (ВП).

• Если а и b являются ВП, то —i a, avb и алЬ также являются ВП.

• Если а является ВП, то Mха и mд.а являются ВС;

• Если / и g являются ВС, то выражения-1/, / v g, /л g являются

ВС.

• Если fug являются ВС, то выражения X/, F/, G/,/Ug, fR g являются ВПВ.

• Если / является ВПВ, то А/ иЕ/ являются ВС. Доказана

Теорема 3.2. Любое выражение X-CTL может быть преобразовано так, что будет содержать только операторы -î.v.A.EX/n^EU/w^EGm^.

Корректные выражения в X-CTL являются ВС. Для того, чтобы дать формальное определение верификации Х-машин при помощи X-CTL, понадобятся определения означивающей функции, пути вычислений и отношения M,q)- f.

Определение. Ь^ : ()М —> - функция означивания

метасостояний предикатами из МРгор. р е МРгор верно в метасостоянии дт1- тогда и только тогда, когда ре (дт1р. Так же определим к

/ = 0 '

Определение. Путь вычислений Ж в Х-машине М - это последовательность состояний Ж = д^, ... , такая, что для любого />0,

Вфе + Р. Будем обозначать Ж1 -отрезок пути Ж, начинающийся

с ¡-го состояния. Будем обозначатьЖ) - первое состояние в пути Ж.

Определение. Запись означает, что выражение Х-СТЬ /

выполняется в состоянии д в Х-машине М. В случае если р является ВП, М ,срп 1= р означает , что р выполняется в метасостоянии дт'. Если g является ВПВ, то запись М ,Ж\= ^ означает , что £ выполняется вдоль некоторого пути л в Х-машине М. Для прочих случаев отношение 1= определяется по индущии (будем считать, что а,Ь - ВГ1, /,/],/-> - ВС, а Е{,81 - ВПВ):

• М,дт -1= р<=> ре Ьм (дт^), где ре МРгор;

• М а <=> М а\

• М,дт^\=алЬ<^> М,дт^\=аи М,дт^\=Ь\

• М ,дт^\=а\/ Ь <=> М ,дт^\=а или М, дт1^ 1= Ь;

• М,д ; \=М а фэ V 1>0:М,дт'; 1=й;

] л J

• М,д ■ 1-т а <=>3 1>0:М,дт1; \=а;

] х ]

• M,q\=—tf /;

• M ,q\= f2<z> M ,q\= fx иш M ,q\= f2\

• <=> 3i > 0:M, ,/irsi (#')!=/;

• M ,x\=Gf t^>yi>0:M ,first(x*)\= f;

M, first{ni )\= /j;

• M,^I=/jR/2 для V/ > 0, если для V<< j Ai, first {п1)\ф /j, то

M,first{7ti)\=f2,

• M,q\= kg M,я\= g для всех таких путей ж, что first(z) = <7;

• М, <71= Eg <=> существует такой путь я-, что first (л:) = q и М,;rl= g . Теперь можно формализовать задачу верификации Х-машины при

помощи CTL:

Определсние./Тустиь дана Х-маитна М — (Q, Г, Г, М, Ф, F, <j0, Ai0, Г) и X-CTL выражение /. Тогда проверка модели осуществляется путем определения множества состояний, удовлетворяющих f ( {q*e ¡2*1 M,q*\= f}). Х-машина считается прошедшей проверку, если ее начальное состояние входит во множество Q *.

В ГЛАВЕ 4 предложен язык описания систем взаимодействующих X-машин и приведено краткое описания синтаксиса этого языка. Описана библиотека для моделирования разнообразных систем с помощью Х-машин.

Системы Х-машин задаются при помощи языка XDL, после чего преобразуются в автоматическом режиме в исходный код Java. XDL

представляет собой подмножество языка XML. Структура файла описания системы Х-машин задается с помощью XML Schema.

Раздел <x-system> является корневым для описания системы Х-машин, все остальные тэги по отношению к нему вложенные. В файле описания может быть только один тэг <x-system>. В открывающем тэге раздела указывается файл с описанием языка XDL. В значении параметра name у тэга <x-system> указывается имя системы Х-машин. Это имя используется в качестве полного (с указанием пакета) для Java-KJiacca, генерируемого из описания. Далее приводится описание возможных подразделов тэга <x-system>.

Внутри раздела <parameters> задаются возможные параметры, которые могут в дальнейшем быть использованы в описании системы. Значения параметров задаются перед созданием экземпляра соответствующего Java-класса. В XDL-спецификации в дальнейшем на параметры можно ссылаться с помощью конструкции #рагат(имя_параметра).

В разделе <defines> задаются «псевдонимы» выражений, которые будут перед обработкой файла заменены на их значения. Например, для удобства чтения кода, можно задать псевдонимы численных констант.

Все описания Х-машин находятся внутри раздела <x-machines>. Описание системы, включающей заданные ранее Х-машины, содержится в разделе <system>. В этом разделе задаются связи между отдельными X-машинами, определяющие конфигурацию системы.

Система Х-машин может обладать собственными входными и выходными портами. Запись и чтение этих портов осуществляется при помощи специальных методов класса XSystem, в класс-потомка которого преобразуется XML-описание системы. Порты системы задаются в разделе <ports>, который по своему синтаксису аналогичен соответствующему разделу Х-машины.

Для объединения Х-машин в систему требуется задать связи между их входными и выходными портами, а также между портами Х-машин и портами самой системы. Задание таких связей осуществляется в разделе <connections>.

Отдельная связь задается тэгом <соппесноп>, в качестве параметров которого указывается входной и выходной порт, которые требуется связать.

Для того, чтобы ХОЬ-описания могли быть использованы для реального моделирования систем взаимодействующих Х-машин, требовалось разработать программное обеспечение, позволяющее осуществлять моделирование системы в динамике. Основным классом библиотеки является Х8у$1ет, представляющий собой базовый класс для систем Х-машин. Экземпляр этого класса является представлением системы Х-машин, заданной при помощи ХОЬ-описания. Взаимодействие пользовательской программы с этим объектом заключается в записи данных во входные порты и чтении содержимого выходных портов.

Система, представляемая объектом Х5ув1ет, может находиться в одном из следующих состояний: «готовность» и «работа». Сразу после создания система находится в состоянии «готовность», переключить в состояние «работа» её можно с помощью метода гип(). При этом Х-машины, составляющие систему, начинают выполняться и пользователь получает возможность записи во входные порты. Метод гевйО позволяет вернуть систему в состояние «готовность», при этом все Х-машины в системе устанавливаются в начальное состояние, а в их память записывается начальное содержимое. Это дает возможность осуществлять несколько независимых запусков системы без необходимости создания новых объектов Х5ух1еш.

После того, как система переведена в состояние «работа», возможна запись во входные порты при помощи метода шри((). Содержимое выходных портов считывается в асинхронном режиме при помощи класса-обработчика, указанного при создании. Если при создании или взаимодействии с системой происходит ошибка, то возбуждаются исключения, базовым классом для которых является ХЕхсерйоп.

В ГЛАВЕ 5 приведен пример моделирования при помощи системы взаимодействующих Х-машин. Для моделирования была выбрана часто

используемая схема хранения данных - распределенное хранилище. Целью моделирования является выяснение экспериментальной зависимости производительности и надежности в зависимости от параметров системы.

Предлагаемая модель распределенного хранилища данных включает в себя два типа Х-машин: Х-машину для моделирования узла хранилища и X-машину для моделирования функций централизованного управления хранилищем. Эти Х-машины называются узел(НОЗТ) и хранилище (STORE).

Рис 2. Система Х-машин, моделирующая распределенное хранилище данных.

Схема коммуникации в модели представлена на рис. 2. Коммуникация X-машин в системе осуществляется путем передачи сообщений через выходные порты и приема сообщений в входные порты. Все сообщения являются объектами типа MSG. В системе определен ряд типов сообщений, которые записываются в поле type структуры MSG. Тип сообщения является целым числом(нП), но для удобства описания для каждого типа предусмотрен символьный псевдоним, описанный в разделе <defines>.

Построенная система Х-машин была использована для моделирования распределенного хранилища данных с переменным количеством узлов. В качестве данных, находящихся в хранилище, рассматривался набор объектов, размер которых генерировался случайным образом. Каждый из узлов производил последовательное чтение и запись случайно выбранного объекта. Таким образом, моделировалось использование распределенного хранилища несколькими серверами, на каждом из которых исполняется экземпляр веб-приложения.

"' Время ответа, мс

Количество узлов

12 16 20 24

Рис 3. Зависимость среднего времени чтения от количества узлов.

После того, как каждый из узлов выполнил 1000 циклов чтение-запись, вычислялось среднее время чтения для данного количества узлов и в систему добавлялся новый узел. Результат моделирования приведен на графике (рис. 3).

Как видно из графика, не наблюдается роста времени чтения при увеличении размеров системы. Отклонения времени чтения от константы можно объяснить статистическими погрешностями. Хорошее согласие с экспериментальными данными, полученными при тестировании реально существующей системы, позволяет говорить об адекватности модели в данном случае.

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

В ЗАКЛЮЧЕНИИ приведены основные результаты исследования.

ОСНОВНЫЕ РЕЗУЛЬТАТЫ И ВЫВОДЫ ДИССЕРТАЦИИ

1. Предложен математический метод моделирования многокомпонентных систем, использующий взаимодействие Х-машин. Допускается асинхронное взаимодействие между Х-машинами. Возможно поэтапное проектирование Х-машин, реализующих компоненты системы. Доказана эквивалентность вычислительных возможностей Х-машины и машины Тьюринга.

2. Предложена темпоральная логика Х-СТЬ для формальной верификации Х-машин. Доказана достаточность минимального набора операторов.

3. Разработан язык ХБЬ для описания систем взаимодействующих X-машин. Создан программный комплекс в виде .Гауа-библиотеки для моделирования динамического поведения программных систем по их ХБ1_-спецификациям.

4. Предложенный метод использован для моделирования распределенного хранилища данных.

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Соболев М.С. Описание больших систем при помощи Х-машин // Современные проблемы фундаментальных и прикладных наук. Часть VII. Управление и прикладная математика: Труды 51-й научной конференции. -М. - Долгопрудный: МФТИ, 2008. - С.20-22.

2. Соболев М.С. Описание больших систем при помощи Х-машин // Моделирование и обработка информации: Сб.ст./Моск.физ.-тех.ин-т. - М., 2008. -С. 236-245.

3. Соболев М.С. Автоматные модели вычислений // Моделирование и обработка информации: Сб.ст./Моск.физ.-тех.ин-т. -М., 2009. -С. 76-85.

4. Соболев М.С. Описание больших систем при помощи Х-машин // Современные проблемы фундаментальных и прикладных наук. Часть VII. Управление и прикладная математика: Труды 52-й научной конференции. -М. - Долгопрудный: МФТИ, 2009. - С.122-123.

5. Соболев М.С. Описание систем при помощи Х-машин // Информационные технологии и вычислительные системы - 2009. - №4 - С. 22-27.

6. Соболев М.С. Использование логики X-CTL для формальной верификации Х-машин // Информационные технологии и вычислительные системы - 2010. - №3 - С.47-52.

7. Соболев М.С. Автоматные модели вычислений// Высокие технологии, исследования, промышленность. Том 3. Труды IX международной научно-практической конференции «Иследование, разработка и применение высоких технологий в промышленности»/ Изд-во Политехи. Ун-та - Санкт-Петербург, 2010.-С.130-132.

Соболев Михаил Сергеевич

МОДЕЛИРОВАНИЕ МНОГОКОМПОНЕНТНЫХ СИСТЕМ ПРИ ПОМОЩИ ВЗАИМОДЕЙСТВУЮЩИХ Х-МАШИН

.13.18 - математическое моделирование, численные методы и комплексы программ

АВТОРЕФЕРАТ

диссертации на соискание ученой степени кандидата физико-математических наук

Подписано в печать 11.10.2010

Усл.п.л. - 1.0 Заказ №02748 Тираж: ЮОэкз.

Копицентр «ЧЕРТЕЖ.ру» ИНН 7701723201 107023, Москва, ул.Б.Семеновская 11, стр. 12 (495) 542-7389 www.chertez.ru

ВВЕДЕНИЕ.

ГЛАВА 1. СУЩЕСТВУЮЩИЕ ПОДХОДЫ К МОДЕЛИРОВАНИЮ

МНОГОКОМПОНЕНТНЫХ СИСТЕМ.

1.1. Модели данных.

1.2. Машина Тьюринга.

1.3. Сети Петри.

1.4. Конечные автоматы.

1.5. Диаграммы состояний.

1.6. Х-машины.

1.7. Вычислительные способности Х-машин.

1.8. Взаимодействующие Х-машины.

1.8.1. Взаимодействие через матрицу коммуникаций.

1.9. Выводы.

ГЛАВА 2. СИСТЕМЫ ВЗАИМОДЕЙСТВУЮЩИХ Х-МАШИН.

2.1. Поэтапное построение взаимодействующих Х-машин.

2.2. Пример: модель перекрестка со светофорами.

2.3. Расширение системы.

2.4. Выводы.

ГЛАВА 3. ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ Х-МАШИН.

3.1. Логика СТЬ.

3.2. ЛогикаХ-СТЬ

3.3. Пример.

3.4. Выводы.

ГЛАВА 4. ЯЗЫК ОПИСАНИЯ СИСТЕМ Х-МАШИН.

4.1. Краткое описание используемых ХМЬ-технологий.

4.2. Описание конструкция языка ХЕ)Ь.

4.2.1. Параметры.

4.2.2. Псевдонимы.

4.2.3. Типы данных.

4.2.4. Описание Х-машины.

4.2.5. Описание системы Х-машин.

4.3. Библиотека для моделирования Х-машин.

4.3.1. Общее описание библиотеки.

4.3.2. Типы данных.

4.3.3. Ввод и вывод.

4.3.4. Детали реализации.

4.4. Выводы.

ГЛАВА 5. МОДЕЛЬ РАСПРЕДЕЛЕННОГО ХРАНИЛИЩА ДАННЫХ.

5.1. Распределенное хранилище данных.

5.2. Общее описание модели.

5.3. Модель узла.

5.3.1. Взаимодействие с сервером приложений.

5.3.2. Выполнение команд хранилища.

5.4. Модель хранилища.

5.4.1. Отправка отсроченных сообщений.

5.4.2. Чтение и запись.

5.5. Производительность распределенного хранилища.

5.6. Выводы.

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

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

Жесткие требования предъявляются также к надежности и производительности многокомпонентных систем — серверным приложениям, на которые приходится большая часть функциональной нагрузки в клиент-серверных системах. Кроме того, в серверных приложениях широко используется параллельное программирование, что затрудняет поиск ошибок и оценку производительности. Часто традиционные методы отладки, используемые при разработке клиентских приложений, не обеспечивают должного уровня тестирования.

Математическое описание программной системы и требований к ней позволяет улучшить качество критически важных систем, в частности многокомпонентных^].

При моделировании многокомпонентных систем можно выделить два аспекта: моделирование данных и моделирование алгоритмов. Большинство из существующих формальных методов-позволяют полно описать только один из этих аспектов. Для моделирования данных обычно используют иерархические, сетевые или реляционные модели, а для описания алгоритмов — модели, основанные на автоматах (машинах состояний): конечные автоматы, автоматы с магазинной памятью, машины Тьюринга[2].

Одним из немногих методов, позволяющих сочетать достоинства обоих подходов, является моделирование на основании.Х-машин. В определении X-машины к состояниям конечного автомата добавляется память, позволяющая хранить типизированные данные. Это дает возможность описывать как динамические, так и статические аспекты системы.

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

Необходимым условием возможности применения-рассматриваемого метода на практике является существование достаточно развитого языка для описания систем взаимодействующих Х-машин, а также программного обеспечения для осуществления моделирования динамического поведения системы.

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

Целью работы является создание метода моделирования многокомпонентных систем, основанного на взаимодействующих Х-машинах, допускаю5 щего поэтапную разработку и тестирование компонентов и асинхронную коммуникацию между частями системы, а также проверка применимости этого метода на практике.

Таким образом, в работе решаются следующие задачи:

1. Разработка теоретических основ и метода построения систем взаимодействующих Х-машин, допускающих асинхронное взаимодействие между Х-машинами и поэтапное проектирование;

2. Формальная верификация Х-машин, позволяющая осуществлять тестирование компонентов систем взаимодействующих Х-машин;

3. Описание языка для создания спецификаций систем взаимодействующих Х-машин, а также комплекса программ позволяющего моделировать программные системы;

4. Моделирование распределенного хранилища данных с использованием предложенного метода.

5.6. Выводы

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

Значения производительности при разных параметрах, полученные при помощи разработанной модели, хорошо согласуются с экспериментально измеренными в распределенном хранилище 8са1еОШ: 81а1е8егуег значениями. Данная модель может быть применена для расчета оптимального количества реплик, обеспечивающего наилучшую производительность конкретной системы.

ЗАКЛЮЧЕНИЕ

В работе были получены следующие результаты:

1. Предложен математический метод моделирования многокомпонентных систем, использующий взаимодействие Х-машин. Допускается асинхронное взаимодействие между Х-машинами. Возможно поэтапное проектирование Х-машин, реализующих компоненты системы. Доказана эквивалентность вычислительных возможностей Х-машины и машины Тьюринга.

2. Предложена темпоральная логика Х-СТЬ для формальной верификации Х-машин. Доказана достаточность минимального набора операторов.

3. Разработан язык ХОЬ для описания систем взаимодействующих X-машин. Создан программный комплекс в виде 1ауа-библиотеки для моделирования динамического поведения программных систем по их ХОЬ-спецификациям.

4. Предложенный метод использован для моделирования распределенного хранилища данных.

1. Young W. Formal Methods versus Software Engineering: Is There a Conflict? // 4th Symposium on Testing, Analysis and Verification. 1991. Victoria.

2. Соболев M.C. Автоматные модели вычислений // Современные проблемы фундаментальных и прикладных наук. Часть VII. Управление и прикладная математика: Труды 52-й научной конференции. М. - Долгопрудный: МФТИ, 2009. - С. 122-123.

3. Spivey J.M. Understanding Z : a specification language and its formal semantics. // Cambridge tracts in theoretical computer science. 1988, Cambridge Cambridgeshire ; New York: Cambridge University Press, viii, 131 p.

4. Jones C.B. Systematic software development using VDM. 2nd ed. Prentice Hall international series in computer science. 1990, New York: Prentice Hall, xiv, 333 p.

5. Futatsugi K., Jouannaud J-P., Meseguer J. Principles of OBJ2. // Proc.l2th. ACM Symp. Principles of Prog. Lang., 1985: p. 52-66.

6. Jacob I. Using Formal Specifications in the Design of a HumanComputer Interface. // Comm. ACM, 1983. 26(4): p. 259-264.

7. Huzing C. Introduction to Design Choices in the Semantics of Statecharts. // Information Processing, 1991.31.

8. Марков A.A., Нагорный H.M Теория алгоритмов. Мат. логика и основания математики. 1984, М.: Наука. 432 с.

9. Turing A.M. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 1937. 2(42): p. 230-65.

10. Hopcroft J.E., Motwani R., Ullman J.D. Introduction to automata theory, languages, and computation. 3rd ed. 2007, Boston: Pearson/Addison Wesley, xvii, 535 p.

11. Booth T.L. Sequential machines and automata theory. 1967, New York,: Wiley, xiv, 592 p.

12. Boas P.E. Machine Models and Simulations. Handbook of Theoretical Computer Science, 1990. Algorithms and Complexity: p. 3-66.

13. Peterson J.L. Petri net theory and the modeling of systems. 1981, Englewood Cliffs, N.J.: Prentice-Hall, x, 290 p.

14. Girault C. Petri nets for systems engineering : a guide to modeling, verification, and applications. 2003, New York: Springer, xvi, 607 p.

15. Нее K.M., Valk R. Applications and theory of Petri nets : 29th international conference, PETRI NETS 2008, Xi'an, China, June 2327, 2008 : proceedings. Lecture notes in computer science,. 2008, Berlin ; New York: Springer, xiii, 428 p.

16. Axo A.B:, Хопкрофт Д.Э., Улъман Д.Д Структуры данных и алгоритмы. 2010, Москва: Вильяме. 391 с.

17. Хопкрофт Д., Мотвани Р., Улъман Д. Введение в теорию автоматов, языков и вычислений. 2. изд. 2002, М.: Вильяме. 527 с.

18. Серебряков В.А. Лекции; по конструированию компиляторов Рос. АН, ВЦ; 1994, М.: ВЦ РАН. 174 с.

19. Wagner F. Modeling software with finite state machines.: a practical approach: 2006, Boca Raton, FL: Auerbach. xix, 369 p.

20. Harel Di, Politi M. Modeling reactive systems with statecharts : the statemate approach. 1998, New York: McGraw-Hill, xiv, 258 p;

21. Drusinsky D. Modeling and5 verification using UML statecharts : a working guide to reactive system design, runtime monitoring, and execution-based; model checking. 2006; Burlington, MA: Newnes. xii, 306 p.

22. Eilenberg S. Automata, languages, and? machines. Pure and applied mathematics a series of monographs and! text books, 58 i e 59. 1974, New York,: Academic Press.

23. Holcombe M. What are X-Machines? Formal aspects of computing, 2000. 12(6): p. 418-422.

24. Holcombe M. X-machines as a basis for dynamic system specification. Software Engineering Journal 1988. 3(2): p. 69-76.

25. Соболев M.C. Автоматные модели вычислений. Моделирование и обработка информации. -М.: МФТИ, 2009: С 76-85, 2009.

26. Aguado J. Systems of Communicatin X-machines for Specifying Distributed Systems. 2002, University of Sheffield.

27. Cowing A.J.G., Vertran C. A structured way to use channels for communication in X-machines systems. Formal aspects of computing, 2000. 12: p. 485-500.

28. Gheorgescn H. A New Approach to Communicating X-machines Systems. Journal of Universal Computer Science, 2000. 6(5): p. 490502.

29. Barnard J. COMX: a design methodology using Communicating X-machines. Information and Software Technology, 1998. 40: p. 271280.

30. Balanescn T.C., Gheorgescu H., Gheorghe M., Holcombe M., Vertran C. Communicating Stream X-machines are no more than X-machines. Journal of Universal Computer Science, 1999. 5(9): p. 494-507.

31. Kefalas P.E.,Kehris E. Communicating X-machines: a practical approach for formal and modular specification of large systems. Information and Software Technology, 2003. 45(5): p. 269-280.

32. Соболев M.С. Описание больших систем при помощи Х-машин // Современные проблемы фундаментальных и прикладных наук. Часть VII. Управление и прикладная математика: Труды 51-й научной конференции. М. - Долгопрудный: МФТИ, 2008. - С.20-22.

33. Соболев М.С. Описание больших систем при помощи Х-машин // Моделирование и обработка информации: Сб.ст./Моск.физ.-тех.ин-т. М., 2008. -С. 236-245.

34. Chan W.A., Beame R.J., Burns P. Model Checking Large Software Specifications. IEEE Transactions on Software Engineering, 1998. 24(7).

35. Соболев М.С. Описание систем при помощи Х-машин Информационные технологии и вычислительные системы, 2009. 4: р. 22-27.

36. Кларк Э.М., Грамберг С., Пелед Д. Верификация моделей программ: Model Checking. 2002, M.: Изд-во Моск. центра непрерыв. мат. образования. 416 с.

37. Ноаге С: An axiomatic basis for computer programming. Communications of the ACM, 1969.39.