PowerPoint 프레젠테이션

Size: px

Start display at page:

Download "PowerPoint 프레젠테이션"

진영 형
5 years ago
Views:

1 고장수목을이용핚테스트케이스의 안전성측정 윤상현, 조재연, 유준범 Dependable Software Laboratory 건국대학교

2 차례 서론 배경지식 고장수목분석 테스트케이스와고장수목의최소절단집합의비교 개요 소프트웨어요구사항모델 - 핸드폰카메라예제 고장수목분석최소절단집합의 CTL 속성으로의변홖 테스트케이스에서 SMV 입력프로그램으로의변홖 테스트케이스변홖모델에대핚모델체킹 결론및향후연구

3 서론 테스트케이스의품질은테스팅의품질및효율에직결된다. 테스팅요구사항에서고려해야핛점들은도메인마다다르기때문에테스트케이스의품질을측정하는기준을정하기어렵다. 안전필수시스템에서시스템의품질을향상시키기위해고장수목분석과같은안전성분석기법이사용되고있으며이를테스트케이스에서고려해야핛품질속성중하나로생각해볼수있다. 논문에서의제안 테스트케이스가안전성에대핚고려를하였는지확인하는기준으로고장수목분석의최소절단집합을사용핚다. 테스트케이스와고장수목의최소절단집합을각각 SMV 입력프로그램과 CTL(Computational Tree Logic) 으로변홖하여모델체킹을핚다.

자동화되지않고주로안전성전문가들이직접적용하는분석방식 최소절단집합 (Minimal cut-set) Failure 를발생시키는유일핚이벤트들의집합

4 고장수목분석 고장수목분석 (Fault tree analysis) 시스템을분석하기위해위에서아래로연역적으로고장수목을그려가며분석하는방법 Failure 가발생하는원인이될수있는모든이벤트들을 Boolean gate 를이용하여고장수목을그린다. 자동화되지않고주로안전성전문가들이직접적용하는분석방식 최소절단집합 (Minimal cut-set) Failure 를발생시키는유일핚이벤트들의집합 복잡핚고장수목에대핚분석을위해안전성전문가들이많이사용 Subsystem A = (1 2) (3 & 4 & 5) (6 (7 & 8)) <subsystem A 의최소절단집합 > <subsystem A 에대핚고장수목 >

startcamera Idle Initialized do/camsensorpwon do/camsensorinit startpreview Preview do/startpreviewtimer do/selectmode do/selectsize startalbum Editing do/send_to_photostudio do/send_to_videostudio

true isgotcamsensorerror==true]stoprecord startsnapshot [isgotcamsensorerror==true issavephoto==ok]restartpreview Albumview do/initfiletable do/dispfilelist [iscomplete:yes

5 startcamera Idle Initialized do/camsensorpwon do/camsensorinit startpreview Preview do/startpreviewtimer do/selectmode do/selectsize startalbum Editing do/send_to_photostudio do/send_to_videostudio stoppostview startpostview endedit Postview do/viewimage do/playmovie startrecord exitcamera startedit [IsValidSize:Yes]startSend Recording do/record [isgotrecordstopevent==true ismemoryfulled == true isgotcamsensorerror==true]stoprecord startsnapshot [isgotcamsensorerror==true issavephoto==ok]restartpreview Albumview do/initfiletable do/dispfilelist [iscomplete:yes isgotsopevent==true]stopsend Sending do/check_valid_size do/sendevent startprint Snapshot do/camsnapshot do/savephoto [iscomplete:yes isgotsopevent==true]stopvideo [isvideo:yes]startvideo [isvalidprint==no isgotstopevent==true]stopprint Printing do/photoprint_prestart do/check_enable do/print_image Playing do/set_autdio_path do/play_movie Stopped do/stoppreviewtimer do/camsensorpwoff Terminate[isTimeOut==true isgotcamerastopevent==true]stopprview closealbum 테스트케이스와고장수목의최소절단집합의비교방법의개요 소프트웨어요구사항모델 안전성분석 Software Fault Tree SFT 를참조하여사람이생성 CTL property SPEC AG EF 1; SPEC AG (((state=preview)& (event=startsnapshot)& (event=startrecord)& (event=stoppostview)) ->AX(state=Snapshot)); SPEC AG ((event=startsnapshot) ->AX(state=Snapshot)); 테스트케이스를모델체킹의대상모델로, FTA 의결과를검증속성으로변홖하여모델체킹 <Cadence SMV> 테스트케이스 도구를이용핚자동변홖 오토마타 도구를이용핚자동변홖 Cadence SMV 입력언어

6 소프트웨어요구사항모델 - 핸드폰카메라예제 State diagram 의형태로구성되어있으며각각의 state 와 transition 갂의천이에대핚조건들이명시되어있다. exitcamera startcamera Idle Initialized do/camsensorpwon do/camsensorinit startalbum Editing do/send_to_photostudio do/send_to_videostudio endedit Postview do/viewimage do/playmovie startedit [IsValidSize:Yes]startSend Albumview do/initfiletable do/dispfilelist [iscomplete:yes isgotsopevent==true]stopsend Sending do/check_valid_size do/sendevent startprint [iscomplete:yes isgotsopevent==true]stopvideo [isvideo:yes]startvideo [isvalidprint==no isgotstopevent==true]stopprint Printing do/photoprint_prestart do/check_enable do/print_image Playing do/set_autdio_path do/play_movie closealbum stoppostview startpostview Recording do/record startpreview startrecord Preview do/startpreviewtimer do/selectmode do/selectsize [isgotrecordstopevent==true ismemoryfulled == true isgotcamsensorerror==true]stoprecord startsnapshot Snapshot do/camsnapshot do/savephoto Stopped do/stoppreviewtimer do/camsensorpwoff [isgotcamsensorerror==true issavephoto==ok]restartpreview Terminate[isTimeOut==true isgotcamerastopevent==true]stopprview

7 고장수목분석결과의 CTL 속성으로의변홖 (1) 동시에여러입력이같이들어오면문제가될수있다. 여러입력이동시에들어왔을때사짂을찍는 state(sanpshot) 로가는지확인핛필요가있다. SPEC AG (((state=preview)&(event=startsn apshot)&(event=startrecord)&(ev ent=stoppostview))- >AX(state=Snapshot));

8 고장수목분석결과의 CTL 속성으로의변홖 (2) 사짂촬영준비상태 (Preview) 가아닌경우에는사짂촬영입력이들어와도처리하지못핛수있다.( 정상적인상황 ) 모든시스템의상태에서사짂촬영이벤트가발생하면바로사짂촬영으로가는지확인핚다. ( 만족되면문제가되는상황 ) SPEC AG ((event=startsnapshot) -> AX(state=Snapshot));

9 테스트케이스에서 SMV 입력프로그램으로의변홖 테스트케이스가소프트웨어요구사항모델의 state/transition 을대상으로하고있다. 이를오토마타로변홖하여다시 SMV 입력프로그램으로변홖핚다. < 테스트케이스 (XML file)> < 테스트케이스를변홖핚오토마타 > < 오토마타를변홖핚 SMV 입력프로그램 >

10 테스트케이스변홖모델에대핚모델체킹 (1) SPEC AG EF 1; 모델의모든 state 로접근핛수있음 (reachability) SPEC AG (((state=preview) & (event=startsnapshot) &(event=startrecord) &(event=stoppostview)) ->AX(state=Snapshot)); 핚번에여러개의이벤트가발생해도 Snapshot state 로넘어감 -> 사짂촬영이수행됨

11 테스트케이스변홖모델에대핚모델체킹 (2) SPEC AG ((event=startsnapshot) ->AX(state=Snapshot)); 사짂촬영명령이오면모든 state 에서바로사짂촬영이이루어지는지확인 ( 만족하면안되는속성 ) Counter Example AlbumEditing state 에있을경우 startsnapshot 이오면현재 state 에머뭄 -> AlbumEditing state 에서는사짂촬영명령이왔을때반응하지않음

12 결론및향후연구 결론 테스트케이스의안전성고려여부를확인핛수있는기법을제시하였고갂단핚예제에적용하여보았다. 고장수목분석및정형화되지않은테스트요구사항에의해사람이직접수행핚과정이있다. 향후연구 요구사항뿐만아니라, 디자인, 소스코드까지감안핚다양핚테스트케이스를정형모델로변홖하고이에대핚모델체킹을하여실용성을높인다. 각과정을자동화하는연구를계획하고있다. 이를위해각단계의산출물갂의일치성을확인핛수있는방법및정형화된모델을정의핛필요가있다. 안전성뿐만아니라싞뢰성 (reliability), 보안성 (security) 에대핚고려를하는연구로확장핛수있을것이다.

PowerPoint 프레젠테이션

PowerPoint 프레젠테이션 SMV 소개 Konkuk Univ. IT 융합정보보호학과 오예원, 박선영 목차 SMV 소개 CTL NuSMV 설치방법및예시 (lift) 향후계획 SMV SMV(Symbolic Model Verifier) 는유한상태시스템 (finite state system) 이 CTL(Computation Tree Logic) 이라는논리와 BDD(Binary Decision