TY  - JOUR
T1  - Design and Implementation of a Model of a Specification Language for Formal Verification
AU - , Kamrul Hasan Talukder AU - , Ahmed Shah Mashiyat AU - , Rezoanoor Rahman 
JO  - Research Journal of Applied Sciences
VL  - 3
IS  - 4
SP  - 288
EP  - 293
PY  - 2008
DA  - 2001/08/19
SN  - 1815-932x
DO  - rjasci.2008.288.293
UR  - https://makhillpublications.co/view-article.php?doi=rjasci.2008.288.293
KW  - Formal verification
KW  -model checking
KW  -textual specification language
KW  -symbolic model verifier
KW  -message sequence charts
KW  -computational tree logic
AB  - 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.
ER  -