DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Kwon, Yong-Rae | - |
dc.contributor.advisor | 권용래 | - |
dc.contributor.author | Oh, Seung-Uk | - |
dc.contributor.author | 오승욱 | - |
dc.date.accessioned | 2011-12-13T05:58:57Z | - |
dc.date.available | 2011-12-13T05:58:57Z | - |
dc.date.issued | 1998 | - |
dc.identifier.uri | http://library.kaist.ac.kr/search/detail/view.do?bibCtrlNo=134022&flag=dissertation | - |
dc.identifier.uri | http://hdl.handle.net/10203/34269 | - |
dc.description | 학위논문(석사) - 한국과학기술원 : 전산학과, 1998.2, [ ii, 63 p. ] | - |
dc.description.abstract | Model checking is an automated procedure for verifying a system. However model checking has a state explosion problem in generating a system model used in the model checking process. In this paper we develop an efficient procedure for the verification of a Statecharts specification by the model checking method. We propose a state abstraction method for obtaining an abstract Statecharts utilizing the hierarchical structure of Statecharts. Through the state abstraction method we can reduce the state space of system, thus alleviating state explosion from which the model checking suffers. Also we show that the model checking procedure with abstract Statecharts is conservative for verification of ∀CTL properties. To compensate for the conservative model checking procedure, we suggest a stepwise verification procedure. To demonstrate the applicability of our method, we verify an example system using the SMV model checker. For this purpose, we translate the Statecharts specification into an SMV program. Our experiment shows that system can be checked with a reduced state space. | eng |
dc.language | eng | - |
dc.publisher | 한국과학기술원 | - |
dc.subject | State abstraction | - |
dc.subject | Model checking | - |
dc.subject | Statecharts | - |
dc.subject | Verification | - |
dc.subject | Stepwise verification | - |
dc.subject | 단계적 검증 | - |
dc.subject | 상태 추상화 | - |
dc.subject | 모델체킹 | - |
dc.subject | Statecharts | - |
dc.subject | 검증 | - |
dc.title | Stepwise verification of statecharts specification using state abstraction | - |
dc.title.alternative | 상태 추상화를 통한 Statecharts 요구명세의 단계적 검증 | - |
dc.type | Thesis(Master) | - |
dc.identifier.CNRN | 134022/325007 | - |
dc.description.department | 한국과학기술원 : 전산학과, | - |
dc.identifier.uid | 000963375 | - |
dc.contributor.localauthor | Kwon, Yong-Rae | - |
dc.contributor.localauthor | 권용래 | - |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.