Study on Measurement Program in each Maturity Level of CMMI 


Vol. 12,  No. 1, pp. 91-102, Feb.  2005
10.3745/KIPSTD.2005.12.1.91


PDF
  Abstract

Given a model and a property, model checking determines whether the model satisfies the property. In case the model does not satisfy the property, model checking gives a counterexample which explains where the violation occurs. Since counterexamples are useful for model debugging as well as model understanding, counterexample generation is one of the indispensable components in the model checking tool. This paper presents efficient counterexample generation techniques when a safety property is falsified. These techniques are used to solve Push Push games which consist of 50 games. As a result, all the games are solved with the proposed techniques. However, with the original NuSMV, 42 games are solved but 8 failed. In addition, we obtain 86% time improvement and 62% space improvement compared to the original NuSMV in solving the game.

  Statistics
  Cite this article

[IEEE Style]

Y. M. Yu and H. S. Han, "Study on Measurement Program in each Maturity Level of CMMI," The KIPS Transactions:PartD, vol. 12, no. 1, pp. 91-102, 2005. DOI: 10.3745/KIPSTD.2005.12.1.91.

[ACM Style]

Young Moo Yu and Hyuk Soo Han. 2005. Study on Measurement Program in each Maturity Level of CMMI. The KIPS Transactions:PartD, 12, 1, (2005), 91-102. DOI: 10.3745/KIPSTD.2005.12.1.91.

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