Проектирование мультимедийных систем с использованием алгебры процессов

Размещено на http://www.allbest.ru

Размещено на http://www.allbest.ru

Проектирование мультимедийных систем с использованием алгебры процессов

Баркова Н.Н.

На конференции ACM Multimedia, организованной в 1997 году Лори Скарлатос (Lori Scarlatos) в Бруклинском колледже обсуждались вопросы использования различных метафор и парадигм при построении мультимедийных систем [1]. Джеми Синглар [2] дал классификацию метафор, которые применяются в различных пакетах прикладных программ для разработки подобных систем. Примером подобного пакета является Flash, который использует метафору временной шкалы. Не смотря на то, что на рынке программных продуктов достаточно много средств для разработки мультимедийных систем, все они имеют довольно существенный недостаток. Одна из основных задач возлагаемых на подобные средства - это взаимоотношения между объектами мультимедийной системы и пользователем.

Решение данной проблемы предлагают Арбаб Ф. (Arbab F.), Херман И. (Herman I.), Рейнолдс Г. Дж. (Reynolds G. J.) [3] с использованием объектной модели, основанной на двух основных концепциях: активных объектах и делегировании, Карла Д. (Karla D.), Барр А. (Barr A.) [4] с использованием временных объектов и событий. Дэвис Дж.С. [5] предлагает описывать мультимедийные системы при помощи двух упорядоченных множеств, описывающих порядок действий и содержание системы.

Все описанные выше подходы не позволяют верифицировать получаемые системы, а также убедиться в их безопасности и эффективности. Подобную задачу позволяют решить формальные методы. Боуэн Дж. в работе [6] привел примеры использования формальных спецификаций при построении систем различных классов.

Алгебра процессов Хоара (CSP) [7] является формальной спецификацией и имеет простой язык, что позволяет пользователю довольно быстро разбираться в описании системы. Цель алгебры процессов - показать, что свойства композиции гарантируют, безопасность построения процессов согласно определенному критерию. Достижение этой цели означает, что алгебра процессов может быть использована для математической верификации характеристик разрабатываемой системы.

Алгебра процессов Хоара позволяет описывать систему в виде совокупности процессов, которые являются основными элементами CSP. Синтаксис можно определить следующим образом:

1) END - процесс, успешно завершивший свою работу.

2) a -> P - процесс, который участвует в событии a, а затем ведет себя как процесс Р. Операция "->" называется префиксом.

3) (a -> P | b -> Q) - процесс, который участвует в событии a, а затем ведет себя как Р или участвует в событии b, а затем ведет себя как Q. Операция "|" - называется выбором.

4) P;Q - процесс, описывающий последовательную композицию. После завершения процесса P, начинает работу процесс Q.

5) P || Q - параллельная композиция процессов.

Алгебра процессов Хоара имеет довольно мощный инструмент для работы с каналами. Опишем необходимые операторы:

1) c!v - вывести значение v по каналу с;

2) c?v - v присвоить значение, поступившее по каналу c.

3) P >> Q - процесс, описывающий объединение транспортеров. и другие.

Любую мультимедийную систему можно рассматривать как набор процессов. Основная задача - обеспечение взаимодействия между процессами без возникновения тупиковых ситуаций.

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

лист[i] - перелистывание i-ой страницы

демо[i] - демонстрация i-ой страницы

щелчок - щелчок кнопкой мыши по странице

Если данный процесс назвать КНИГА, то отдельная страница будет иметь имя КНИГА[i], а сам процесс в виде, предложенном Меги Дж. и Крамером Дж. [8], будет выглядеть следующим образом:

мультимедийный метафора прикладной

КНИГА = КНИГА[0],

КНИГА[i:0..N] = (when (i<N) лист[i]->КНИГА[i+1]

|when (i==N) лист[N]->КНИГА

|when (i<=N) щелчок -> демо[i] ->END

). (1)

где when - аналог условного оператора.

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

щелчок -> демо.0 -> END

лист.0 -> щелчок -> демо.1 -> END

лист.0 -> лист.1 -> щелчок -> демо.2 -> END

лист.0 -> лист.1 -> лист.2 -> лист.0 -> лист.1 -> лист.2 -> …

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

В случае, если необходимо продолжить просмотр книги, то процесс примет вид:

КНИГА = КНИГА[0],

КНИГА[i:0..N] = (when(i<N) лист[i]->КНИГА[i+1]

|when(i==N) лист[N]->КНИГА

| when (i<=N) щелчок -> демо[i] ->щелчок->КНИГА[i]

). (2)

В данном случае, описанный процесс бесконечен, т.к. нетрудно заметить, что после операций над последней страницей происходит переход в начало процесса.

Представленные примеры (1) и (2) можно рассматривать как набор взаимно рекурсивных определений, содержательность которых вытекает из того факта, что правая часть каждого уравнения является предваренной.

Конечный автомат для (2) с условием того, что книга содержит четыре страницы, построенный с использованием анализатора LTS, предложенного Меги Дж. и Крамером Дж. [8], представлен на рисунке 1, где BOOK - это процесс КНИГА, list[i] - соответствует событию лист[i] , demo[i] - событию демо[i] , click - событию щелчок. Понятно, что для книги, содержащей большее количество страниц конечный автомат будет более сложным и содержать большее количество состояний и переходов. Однако, на примере рисунка 2 можно проанализировать автомат и сделать заключение о беступиковости процесса (2).

Рисунок 1 - Конечный автомат процесса "Книга"

Беступиковость данного процесса можно доказать аналогично (1), однако, Хоар доказал, что любой рекурсивный процесс свободен от дедлока.

Хоар доказал, что процессы подобные (1) и (2) можно представить как последовательные процессы. Таким образом, в нашем случае процесс КНИГА можно описать как:

КНИГА=КНИГА[0]; КНИГА[1];… ;КНИГА[N] (3)

Если не произойдет успешного завершения процесса КНИГА[i], то и не завершится КНИГА.

Представленные выше процессы (1) и (2) состоят из нескольких процессов, каждый из которых на самом деле описывает поведение отдельной страницы. При реализации данных процессов необходимо осуществлять взаимодействие между отдельными процессами. Хоар для решения данной задачи предложил использовать концепцию передачи сообщений по некоторому каналу.

Процесс, описывающий отдельную страницу примет вид:

КНИГА [i]= (when (i<N) лев?i -> (лист[i]->прав!(i+1)

|щелчок->демо[i]->щелчок->лист[i]->прав!(i+1))

| when(i==N) лев?N->(лист[N]->прав!0

|щелчок->демо[i]->щелчок->лист[N]->прав!0))

где лев - входной канал, прав - выходной канал. Процесс КНИГА[i] имеет только два канала, следовательно он является транспортером. Основной процесс может иметь следующий вид:

КНИГА= КНИГА[0] >> КНИГА[1] >>… >>КНИГА[N]. (4)

Операция сцепления (">>") соединяет процессы только одним каналом, поэтому не угрожает системе дедлоком. Однако, для подобных процессов существует новая опасность - замыкание. Такая ситуация может возникнуть в том случае, когда КНИГА [i] и КНИГА [i+1] будут все время проводить во взаимодействии друг с другом. Процесс КНИГА [i] является предваренным слева, что согласно доказательству преведенному Хоаром позволяет утверждать, что процесс КНИГА свободен от замыкания.

Реализация процессов при помощи каналов может быть особенно полезна при конкретной реализации. Подобное решение может быть использовано при выполнении задачи с помощью Java Communicating Sequential Processes (JCSP)[9] или Communication Threads in Java (CTJ)[10], в основе которых лежит концепция синхронной передачи сообщений по каналу.

Перепишем исходный процесс в виде, предложенным Меги Дж. и Крамером Дж. [8]:

КНИГА = КНИГА[0],

КНИГА[i:0..N] = (when (i<N) канал.получ[i]->(лист[i]->канал.отправ[i+1]-> КНИГА[i+1]

|щелчок->демо[i]->щелчок->лист[i]->канал.отправ[i+1]->

КНИГА[i+1])

| when(i==N) канал.получ[N]->(лист[N]->канал.отправ[0]->

КНИГА

|щелчок->демо[i]->щелчок->лист[N]->канал.отправ[0]->

КНИГА)

)/{канал/канал.{отправ, получ}}.

В данном процессе добавлены два события: канал.получ[i] - получение сообщения; канал.отправ[i] - передача сообщения. Однако, при реализации подобного процесса в JCSP или CTJ необходимо построить сеть процессов и потребуется некоторый процесс, который будет управлять всеми остальными, т.е. передавать необходимые сообщения процессам. В JCSP и CTJ эта задача решается вводом параллельного процесса. Исходная задача будет иметь следующее решение:

КНИГА1=КНИГА || УПРАВЛЕНИЕ. (5)

где УПРАВЛЕНИЕ - процесс, управляющий передачей сообщений между страницами.

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

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

Системы, основанные на формальных методах, как описано в [6], способны укладываться в график, в бюджет и завершаться созданием правильно работающего программного или аппаратного обеспечения, которое хорошо структурировано, легко обслуживается и полностью удовлетворяет всем требованиям заказчика.

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

Использование алгебры процессов предполагает, что код появляется на гораздо более поздней стадии цикла разработки. В спецификации же вкладывается значительно больше сил, чем при разработке стандартными методами. В данном случае, также гораздо больше число ошибок, устраняемых на этом этапе. Все это позволяет быстрое создание прототипа системы, что особенно важно для заказчика.

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

Литература

1. Designing Interactive Multimedia / L.L. Scarlatos, K. Harada, C. Heeter, R. Muller, B. Shneiderman [Электронный ресурс], 1997. - Режим доступа: http://www.acm.org/sigs/sigmm/MM97/papers/Scarlatos/ - Загл. с экрана. - Яз. англ.

2. Siglar J. Multimedia Authoring Systems FAQ (1/2) / Siglar J. [Электронный ресурс], 1997. - Режим доступа: http://omicron.felk.cvut.cz/FAQ/articles/a1133.html - Загл. с экрана. - Яз. англ.

3. Arbab F. An Object Model for Multimedia Programming / F.Arbab, I. Herman, G.J. Reynolds // Computer Graphics Forum, Vol. 12, No. 3, pp. C-101 - 113, 1993.

4. Karla D. Modeling with Time and Events in Computer Animation / D. Karla, A.H. Barr // Computer Graphics Forum (EUROGRAPHICS '92 Proceedings), Vol. 11, No. 3, pp. 45--58, Sep. 1992.

5. Davis J.S. Order and Containment in Concurrent System Design / Ph.D. thesis in Engineering-Electrical Engineering and Computer Science. - University of California at Berkeley - 2000. - p. 110

6. Боуэн Дж. П. Десять заповедей формальных методов / Дж.П. Боуэн, М.Дж. Хинчи // Мир ПК, № 9 -10. - 1997.

7. Хоар Ч. Взаимодействующие последовательные процессы: Пер. с анг. / Ч. Хоар. - М.: Мир, 1989. - 264с., ил.

8. Magee J. Concurrency: State Models & Java Programs / J.Magee, J. Kramer // Wiley, 1999. - p. 374.

9. Welch P.H. The JCSP Home Page.

10. Hilderink G.H. The CTJ (Communicating Threads in Java) Home Page [Электронный ресурс], 1998 / G.H. Hilderink. - Режим доступа: http://www.ce.utwente.nl/javapp/ - Загл. с экрана. - Яз. англ.

Размещено на Allbest.ru