Title :
A study on implementation of model checking tool for verifying LTS specifications
Author :
Jung, Jaeyoun ; Kim, Youngeung ; Chung, Yeondae ; Jeong, Cheoljoo ; Kim, Sungun
Author_Institution :
Dept. of Telematics Eng., Pukyong Nat. Univ., Pusan, South Korea
Abstract :
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++ language and runs on IBM PC under Windows NT
Keywords :
formal logic; formal verification; process algebra; C++; IBM PC; LTS specifications; Windows NT; deadlock; livelock; modal logic; model checking tool; mu-calculus; reachability; Calculus; Logic; Postal services; Power system modeling; Prototypes; Safety; Software engineering; Specification languages; Systems engineering and theory; Telematics;
Conference_Titel :
Information Networking, 1998. (ICOIN-12) Proceedings., Twelfth International Conference on
Conference_Location :
Tokyo
Print_ISBN :
0-8186-7225-0
DOI :
10.1109/ICOIN.1998.648443
