Автоматическая система анализа и верификации телекоммуникационной системы, описанной на языке MSC, с помощью формализма сетей Петри

Abstract

За останні 20 років формальні методи почали широко використовуватись для специфікації, аналізу, верифікації та відповідного тестування програмних та технічних систем і, зокрема, телекомунікаційних протоколів [1]. В даній роботі пропонується автоматизований технологічний процес формальної специфікації та верифікації телекомунікаційної системи. Формальна модель системи будується у вигляді ординарної мережі Петрі. Аналіз системи виконується за допомогою методів лінійної алгебри.

Last 20 years formal methods are being used widely to specify formally, analyze, verify and test software and hardware systems, particularly, telecommunication protocols [1]. In this paper automated system is presented which specify formally and verify the telecommunication system. The automated system applies the formal modeling technique of Petri nets and is based on linear algebra methods of analysis in order to research some properties of telephone system.