Abstract: The world is moving towards automation and automation requires correctness. So the importance of formal verification tools is increasing rapidly as it is an automatic technique for verifying finite state concurrent systems. However, the industrial usability of formal verification tools remains limited for the complexities and expertise needed for modeling the behavior of a system. In this study, we present a methodology that can model the behavior of a system in Textual Specification Language (TSL) based on Message Sequence Charts (MSC�s) with less expertise and effort. For proper illustration of TSL, we convert the TSL specification into Symbolic Model Verifier (SMV) code using a Turbo C/C++ program and then verify some properties of the system expressed in Computational Tree Logic (CTL) with the help of the SMV model checker, producing verdicts or counter example.