Информационная система "Конференции"

Тезисы докладов

Информационные технологии

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

Программная система SPV (SDL protocol verifier) [2], разрабатываемая в ИСИ СО РАН, позволяет создавать и редактировать модели на основе модифицированных иерархических раскрашенных сетей Петри, обогащенных временным механизмом и приоритетами, а так же проводить их симуляцию. Она включает следующие основные компоненты: графический редактор иерархических сетевых моделей, их симулятор, транслятор с языка спецификаций SDL в сетевые модели и верификатор.

Графический редактор позволяет пользователю строить и модифицировать сетевые модели. Симулятор позволяет следить за процессом функционирования модели при заданных начальных условиях, определять ее состояние на любом этапе симуляции. При этом часто удается обнаружить семантические ошибки модели. Верификатор позволяет по сетевой модели проверить, обладает ли моделируемая система теми или иными свойствами. Трансляторы строят сетевую модель исходной системы по ее спецификации на языке SDL.

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

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

В докладе представлена распределенная версия системы SPV, которая полностью удовлетворяет вышеизложенной схеме. Она позволит проводить симуляцию более сложных систем, что крайне важно для прикладного использования. В качестве программного промежуточного слоя для удаленного вызова процедур была использована библиотека Pyro [3].

Данная работа частично поддержана грантом РФФИ 07-07-00173.

Литература

[1] Котов В.Е. Сети Петри. – Москва: Наука, 1984. --- 160 с.

[2] Nepomniaschy V.A., Alekseev G.I., Argirov V.S., Beloglazov D.M., Bystrov A.V., Chetvertakov E.A., Churina T.G., Mylnikov S.P., Novikov R.M. Application of Modified Coloured Petri Nets to Modeling and Verification of SDL Specified Communication Protocols // Proc. 2-nd Intern. Symp. on Computer Science in Russia, Ekaterinburg 2007. Lecture Notes in Computer Science. --- Berlin: Springer, 2007. 301-314 c.

[3] Официальный сайт Pyro --– http://pyro.sourceforge.net

Примечание. Тезисы докладов публикуются в авторской редакции

Ваши комментарии Обратная связь

[Головная страница] [Конференции]

© 1996-2000, Институт вычислительных технологий СО РАН, Новосибирск
© 1996-2000, Сибирское отделение Российской академии наук, Новосибирск
    Дата последней модификации: 06-Jul-2012 (11:48:14)