A Study on Implementation of Model Checking Program for Verifying LTS Specification 


Vol. 5,  No. 4, pp. 995-1004, Apr.  1998
10.3745/KIPSTE.1998.5.4.995


PDF
  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, safety and liveness for the state and action on LTS. The tool is implemented by C language and runs on IBM PC under Windows NT.

  Statistics
  Cite this article

[IEEE Style]

P. Y. Bum, K. T. Kyun, K. S. Un, "A Study on Implementation of Model Checking Program for Verifying LTS Specification," The Transactions of the Korea Information Processing Society (1994 ~ 2000), vol. 5, no. 4, pp. 995-1004, 1998. DOI: 10.3745/KIPSTE.1998.5.4.995.

[ACM Style]

Park Yong Bum, Kim Tae Kyun, and Kim Sung Un. 1998. A Study on Implementation of Model Checking Program for Verifying LTS Specification. The Transactions of the Korea Information Processing Society (1994 ~ 2000), 5, 4, (1998), 995-1004. DOI: 10.3745/KIPSTE.1998.5.4.995.

Forms

Search
(IN TITLE, AUTHOR, ABSTRACT,KEYWORDS)

Advanced Search ▼

POPULAR KEYWORDS
(TOP 10 KEYWORDS)

Recent Publications
(LAST 3 YEARS)

Old Journals

Indexing

All publications of TKIPS is indexed in DOI, EBSCO, Google Scholar, Crossref, and CrossCheck.

TKIPS is also selected as the Journal for Accreditation by NRF (National Research Foundation of Korea).

Related Journals