A study on implementation of model checking tool for verifying LTS specifications
Jae-Youn Jung, Youngeung Kim, Yeondae Chung, Cheoljoo Jeong, Sungun Kim · 2002
This paper presents an implementation of model checking tool for LTS process specification which checks deadlock, livelock and reachability for the state and action. The implemented formal checker using modal mu-calculus is able to verify whether properties expressed in modal logic are true on specifications. We prove experimentally that it is powerful to check, livelock and reachability for the state and action on LTS. The tool is implemented by C/sup ++/ language and runs on IBM PC under Windows NT.