Research Journal of Applied Sciences

Year: 2008
Volume: 3
Issue: 4
Page No. 288 - 293

Design and Implementation of a Model of a Specification Language for Formal Verification

Authors : Kamrul Hasan Talukder , Ahmed Shah Mashiyat and Rezoanoor Rahman

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.

How to cite this article:

Kamrul Hasan Talukder , Ahmed Shah Mashiyat and Rezoanoor Rahman , 2008. Design and Implementation of a Model of a Specification Language for Formal Verification. Research Journal of Applied Sciences, 3: 288-293.

Design and power by Medwell Web Development Team. © Medwell Publishing 2022 All Rights Reserved