SMT Solve를 이용한 Simulink Stateflow Model의 Test Case 생성
Test Case Generating for Simulink Stateflow Model using SMT Solver
- 주제(키워드) 모델 기반 테스트 , Simulink/Stateflow
- 발행기관 아주대학교
- 지도교수 정기현
- 발행년도 2014
- 학위수여년월 2014. 2
- 학위명 석사
- 학과 및 전공 일반대학원 전자공학과
- 실제URI http://www.dcollection.net/handler/ajou/000000016303
- 본문언어 한국어
- 저작권 아주대학교 논문은 저작권에 의해 보호받습니다.
초록/요약
안전이 중요한 임베디드시스템의 철저한 검증 절차가 요구됨에 따라 테스팅의 중요성이 부각되고 있다. Simulink/Staflow는 임베디드 시스템의 제어로직을 표현한 정교하게 모델링 하는데 널리 사용된다. 작성된 모델은 테스트 케이스를 생성하는데도 사용된다. 하지만 Simulink/Stateflow 모델에는 State 계층구조 및 암묵적인 Back-Tracking이 존재하여 동작의 분석이 어려워 효과적인 테스트 케이스 생성이 어렵다. 기존의 테스트 케이스 생성 방법들은 테스트 케이스 생성 시 랜덤방식을 기반한 방법으로 테스트 입력을 찾기 때문에 복잡한 로직이 표현 될 경우 테스트 입력을 찾기가 어렵다. 본 논문에서는 Simulink 모델을 SMT로 표현하고, 변환된 모델을 해석하여 테스트 케이스을 찾는 방법을 제안한다. 모델을 SMT Solver가 해결할 수 있게 하기 위해, Simulink Stateflow의 변수와 제어의 흐름을 순차구조로 표현, 변환과정을 거쳐 SMT의 입력언어로 변환하는 방법을 제시한다. 또한, 제안된 방법을 이용하여 최대의 커버리지를 만족하기 위한 새로운 테스트 생성기의 알고리즘을 제시한다. 제안된 알고리즘은 실제 시스템에 적용하여 테스트 케이스를 생성하여 그 효용성을 검증받는다.
more목차
제 1 장 서론 - 12 -
제 2 장 관련 연구 - 15 -
제 1 절 SMT(SATISFIABILITY MODULO THEORIES) - 15 -
제 1 항 SAT와 SMT - 15 -
제 2 항 Yices - 16 -
제 2 절 SMT를 이용한 테스트케이스 생성 - 17 -
제 3 절 STATEFLOW의 정적 단일 배정 형태와 FLOWGRAPH 전개 - 18 -
제 4 절 SIMULINK 모델의 테스트케이스 생성 - 19 -
제 3 장 SIMULINK 모델의 SMT 변환 - 20 -
제 1 절 YICES VARIABLE - 20 -
제 1 항 변수의 범주 - 20 -
제 2 항 변수의 Type 결정 - 22 -
제 2 절 구조상의 전처리 - 26 -
제 1 항 From, Goto Block의 전처리 - 26 -
제 2 항 Sink/Source Block의 전처리 - 26 -
제 3 절 변수의 흐름을 제어하기 위한 처리 - 27 -
제 1 항 Memory Block의 처리 - 27 -
제 2 항 Stateflow의 처리 - 29 -
1 Flowgraph - 29 -
2 Decomposition OR인 State - 46 -
3 Decomposition AND인 State - 50 -
4 Function - 55 -
5 Type Conversion - 59 -
제 4 절 SMT 언어로 변환하기 - 60 -
제 1 항 기본 동작에 대한 변환 - 60 -
제 2 항 Block의 Behavior의 변환 - 61 -
1. Stateflow - 61 -
2. Gain Block - 65 -
3. Lookup - 65 -
4. Delay - 66 -
5. Subsystem - 66 -
제 4 장 테스트 케이스 생성 - 67 -
제 1 절 COVERAGE TARGET - 67 -
제 1 항 State Coverage Target - 67 -
제 2 항 Transition(Path) Coverage Target - 68 -
제 3 항 MC/DC Coverage Target - 71 -
제 2 절 SMT SOLVER의 활용 - 72 -
제 1 항 SMT Model Assert - 72 -
제 2 항 SMT Solver Output - 73 -
제 3 절 CONFIG - 76 -
제 1 항 Config의 의미 - 76 -
제 2 항 Config의 생성 - 79 -
제 3 항 Config Stability - 79 -
제 4 절 COVERING TARGET - 82 -
제 1 항 Cover - 82 -
제 2 항 Target Cover 알고리즘 - 83 -
1. Target Cover with Time - 83 -
2. New Candidate Config - 85 -
3. Timer Stable 검색 - 87 -
4. Covering Target List - 89 -
5. Cover from previous Test Tree - 91 -
제 5 절 TEST SCRIPT - 92 -
제 5 장 실험 - 95 -
제 1 절 구현 - 95 -
제 2 절 검증 - 96 -
제 6 장 결론 - 100 -
