Конференции ИВТ СО РАН

VIII Всероссийская конференция молодых ученых по математическому моделированию и информационным технологиям

27 - 29 ноября 2007 года, Новосибирск

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

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

Верификация взаимодействия функциональностей в телефонных сетях с помощью раскрашенных сетей Петри

Белоглазов Д.

ИСИ СО РАН (Новосибирск)

Проблема взаимодействия функциональностей (feature interaction problem, FIP) [1] уже в течение многих лет изучается мировым научным сообществом, так как является одной из наиболее интересных, практически значимых и сложных проблем в области информационных тех-нологий. Проблема взаимодействия функциональностей возникает в комплексных системах, включающих в себя несколько модулей со смежной функциональностью. Модули могут взаимодействовать друг с другом, вызывая тем самым отклонения от ожидаемого поведения системы в целом. Такие отклонения могут быть безвредными, однако в большинстве случаев они оказываются нежелательными и даже опасными. В нашей работе рассматривается классический случай FIP-проблемы: телефонная сеть с дополнительными функциональностями.

Нами построена абстрактная модель в виде взаимодействующих конечных автоматов, имеющая клиент-серверную структуру: автоматы-абоненты взаимодействуют с автоматом-станцией. Сначала была построена автоматная модель базовой модели звонков (basic call state model). Затем она была дополнена функциональностями "перевод звонка", "прямое соединение" и "запрет входящих". Нами впервые разработан алгоритм трансляции полученной автоматной модели в модифицированные раскрашенные сети Петри - ИВТ-сети [2]. Для различных автоматных моделей при помощи полученного алгоритма построены ИВТ-сети.

Для выявления взаимодействия функциональностей телефонной сети, моделируемой ИВТ-сетями, в работе используется набор компонент системы SPV [2], предназначенной для верификации распределённых систем, представленных в виде раскрашенных сетей Петри и ИВТ-сетей. Верификация проводится методом проверки моделей, представленных в виде графов достижимости ИВТ-сетей, для свойств, которые выражены формулами ч-исчисления.

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

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

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

Литература
Keck D.O., Kuehn P.J. The Feature and Service Interaction Problem in Telecommunications Sys-tems: A Survey // IEEE Transactions on Software Engineering, vol. 24, no. 10, October 1998.
2. V.A. Nepomniaschy, G.I.Alekseev, V.S. Argirov, D.M. Beloglazov, A.V. Bystrov, E.A. Chetverta-kov, T.G. Churina, S.P. Mylnikov, R.M. Novikov Application of Modified Coloured Petri Nets to Modeling and Verification of SDL specified Communication Protocols // CSR 2007, LNCS 4649, pp. 303 - 314.

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

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

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