In this thesis, modeling and analysis for telecommunication systems represented by CCITT/SDL are described.
We suggest Extended Numerical Petri Net(ENPN) for modeling and analysis of systems represented by CCITT/SDL, and we show that all of the SDL representations can be transformed into ENPN by suggesting mapping rules. And also, we define ENPN description language, in machine-processable form, to describe ENPN. The ENPN allows to represent the static structure and dynamic behaviors of the model at any levels of details.
As algorithm to create Reachability Graph and methods to analyze the dynamic behaviors of systems via Reachability Graph, are presented. Analysis methodology based on stepwise refinement provides practical ways for analysis of complex and large systems. Reachability Graph allows us to analyze the dynamic behaviors of systems such as event sequence, reachability, liveness, safeness, boundedness, coverability and conservation problem.