모델기반의 커널 테스팅 프레임워크MOdel-based KERnel Testing (MOKERT) Framework
| DC Field | Value | Language |
|---|---|---|
| dc.contributor.author | 김문주 | ko |
| dc.contributor.author | 홍신 | ko |
| dc.date.accessioned | 2011-01-04T03:04:29Z | - |
| dc.date.available | 2011-01-04T03:04:29Z | - |
| dc.date.created | 2012-02-06 | - |
| dc.date.created | 2012-02-06 | - |
| dc.date.issued | 2009-07 | - |
| dc.identifier.citation | 정보과학회논문지 : 소프트웨어 및 응용, v.36, no.7, pp.523 - 530 | - |
| dc.identifier.issn | 1229-6848 | - |
| dc.identifier.uri | http://hdl.handle.net/10203/21346 | - |
| dc.description.abstract | 최근 내장형 시스템이 점점 많은 분야에 사용되며, 시스템에 특화된 운영체제 커널에 대한 필요성이 커지고 있다. 하지만, 커널 개발은 코드의 복잡성 등의 이유로 말미암아 테스팅에 큰 비용이 소요됨에도 불구하고, 높은 신뢰성을 달성하기가 어려운 실정이다. 이러한 커널 개발 및 테스팅의 어려움을 극복하기 위해, 운영체제 커널의 동시성 오류 검출을 지원하는 모델 기반의 커널 테스팅 (MOKERT) 프레임워크를 제안한다. MOKERT 프레임워크는 주어진 C 프로그램을 Promela 정형 명세 모델로 변환하고 나서 Spin 모델검증기를 사용하여 검증하고, 검증반례가 생성된 경우, 이 검증반례를 실제 커널 코드에서 실행을 시켜서 진위를 확인한다. 본 연구에서는 MOKERT 프레임워크를 리눅스 proc파일시스템에 적용하여, ChangeLog에 보고된 오류가 실제로 자원경쟁문제를 일으킴을 확인하였을 뿐만 아니라, 커널 패닉을 일으키는 새로운 오류도 발견하였다. | - |
| dc.language | Korean | - |
| dc.language.iso | ko | en |
| dc.publisher | 한국정보과학회 | - |
| dc.title | 모델기반의 커널 테스팅 프레임워크 | - |
| dc.title.alternative | MOdel-based KERnel Testing (MOKERT) Framework | - |
| dc.type | Article | - |
| dc.subject.alternative | model checking | en |
| dc.subject.alternative | testing | en |
| dc.subject.alternative | counter example analysis | en |
| dc.subject.alternative | model extraction | en |
| dc.type.rims | ART | - |
| dc.citation.volume | 36 | - |
| dc.citation.issue | 7 | - |
| dc.citation.beginningpage | 523 | - |
| dc.citation.endingpage | 530 | - |
| dc.citation.publicationname | 정보과학회논문지 : 소프트웨어 및 응용 | - |
| dc.identifier.kciid | ART001364303 | - |
| dc.contributor.localauthor | 김문주 | - |
| dc.contributor.nonIdAuthor | 홍신 | - |
| dc.subject.keywordAuthor | 모델검증 기법 | - |
| dc.subject.keywordAuthor | 테스팅 | - |
| dc.subject.keywordAuthor | 검증반례 분석 | - |
| dc.subject.keywordAuthor | 모델추출 | - |
| dc.subject.keywordAuthor | model checking | - |
| dc.subject.keywordAuthor | testing | - |
| dc.subject.keywordAuthor | counter example analysis | - |
| dc.subject.keywordAuthor | model extraction | - |
- Appears in Collection
- CS-Journal Papers(저널논문)
- Files in This Item
- 22950.pdf(503.06 kB)Download
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.