1. 모델체킹의 개요
1-1. 모델체킹의 정의
- 시스템에 대한 유한 상태 모델과 검증하고자 하는 특성이 논리적으로 정형성의 형태로 주어졌을 때, 해당 시스템이 해당 속성을 만족하는 지를 자동적으로 검사하는 정형 검증 기법
2. 모델체킹의 개념도, 정리증명과 비교
2-1. 모델체킹의 개념도
2-2. 모델체킹과 정리증명의 비교
| 구분 | 모델체킹(Model Checking) | 정리증명 Automated Theorem Proving) |
| 검증목표 | -시스템 모델의 시스템 특성 만족 여부 | -시스템 명세와 특성의 논리학적 정합성 |
| 사용기법 | -정형명세 언어를 통한 시스템 명세(유한상태기계) -시스템 요구사항에 기반하여 시스템 특성 도출 |
-수학/논리학적 공리(Axiom), 규칙(Rule)을 활용하여 시스템명세/특성도출 |
| 장점 | -모델 증명 도구를 통한 자동화 가능 | -무한상태기계도 명세 및 증명 가능 |
| 단점 | -유한상태기계만 명세 및 증명 가능 | -시스템 명세 도출 및 증명이 매우 난해 |
| 활용 예 | -CMU’s SMV, Bell/s SPIN, Berkeley’s VIS | -SPEAR(II), PVS |
3. 모델체킹 적용시 유의사항
'1. IT Story > Basic Studies' 카테고리의 다른 글
| 7S 모델 (0) | 2019.07.08 |
|---|---|
| 가치사슬(Value Chain) (0) | 2019.07.07 |
| 5 Force (0) | 2019.07.06 |
| IEEE 1471 (0) | 2019.07.05 |
| 요구공학(Requirement Engineering) (0) | 2019.07.03 |
| 요구사항분석 (0) | 2019.07.02 |
| 경영환경분석 (0) | 2019.07.01 |
| IT ROI (Return Of Investment) (0) | 2019.06.30 |
운명을바꾸는자
IT와 함께 살아가는 삶
