DocumentCode
1654616
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
fYear
1998
Firstpage
539
Lastpage
543
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Information Networking, 1998. (ICOIN-12) Proceedings., Twelfth International Conference on
Conference_Location
Tokyo
Print_ISBN
0-8186-7225-0
Type
conf
DOI
10.1109/ICOIN.1998.648443
Filename
648443
Link To Document