Белоглазов Д.М., Непомнящий В.А. "МОДЕЛИРОВАНИЕ И ВЕРИФИКАЦИЯ ВЗАИМОДЕЙСТВИЯ ФУНКЦИОНАЛЬНОСТЕЙ В ТЕЛЕФОННЫХ СЕТЯХ ПРИ ПОМОЩИ КОНЕЧНЫХ АВТОМАТОВ И РАСКРАШЕННЫХ СЕТЕЙ ПЕТРИ"

МОДЕЛИРОВАНИЕ И ВЕРИФИКАЦИЯ ВЗАИМОДЕЙСТВИЯ ФУНКЦИОНАЛЬНОСТЕЙ В ТЕЛЕФОННЫХ СЕТЯХ ПРИ ПОМОЩИ КОНЕЧНЫХ АВТОМАТОВ
И РАСКРАШЕННЫХ СЕТЕЙ ПЕТРИ

Для моделирования, анализа и верификации телекоммуникационных систем обычно применяются такие модели, как конечные автоматы, сети Петри и их обобщения. Цель данной работы – представить новый двухуровневый метод моделирования и верификации телекоммуникационных систем. На первом этапе этого метода теле-коммуникационные системы моделируются в виде расширенных конечных автоматов, а на втором этапе автоматные модели транслируются в раскрашенные сети Петри. Данный метод применяется к исследованию проблемы взаимодействия функциональностей в телефонных сетях. В качестве примера рассматривается базовая модель звонков (Basic Call State Model) с дополнительными функциональностями. Для построения графов достижимости раскрашенных сетей Петри используется система CPN Tools, а для верификации методом проверки моделей используется система Petri Net Verifier. Описанные эксперименты позволили выявить некоторые нежелательные взаимодействия функциональностей в телефонных сетях.
Ключевые слова: телекоммуникационные системы, конечные автоматы, раскрашенные сети Петри, взаимодействие функциональностей, телефонные сети, верификация, метод проверки моделей.

D. M. Belogolazov, V. A. Nepomniaschy
Modeling and Verification of Feature Interaction in Telephone Networks
Using Finite Automata and Coloured Petri Nets
For modeling, analysis and verification of telecommunication systems, the models such as finite automata, Petri nets and their generalizations are usually applied. The goal of our work is to represent a new two-level approach for modeling and verification of telecommunication systems. On the first level telecommunication systems are modeled by extended finite automata, while on the second level the automata models are translated into coloured Petri net (CPN). This method is applied to investigation of feature interaction problem in telephone networks. As an example, Basic Call State Model with additional features is considered. CPN Tools is used for construction of reachability graphs of CPN. We used the Petri Net Verifier for verification of the net models by model checking method. Described experiments allowed us to detect some undesirable feature interactions in telephone networks.
Keywords: telecommunication systems, finite automata, coloured Petri nets, feature interaction, telephone networks, verification, model checking method.

http://lib.nsu.ru:8080/jspui/handle/nsu/113