모델체킹(Model Checking)

1. 모델체킹의 개요

 1-1. 모델체킹의 정의

   - 시스템에 대한 유한 상태 모델과 검증하고자 하는 특성이 논리적으로 정형성의 형태로 주어졌을 때, 해당 시스템이 해당 속성을 만족하는 지를 자동적으로 검사하는 정형 검증 기법

 

2. 모델체킹의 개념도, 정리증명과 비교

 2-1. 모델체킹의 개념도

- 검증하고자 하는 SW를 레이블이 있는 상태전이 기계의 형식으로 표현, 목표를 시제 논리로 명세하여 시스템 공간을 엄밀하게 탐색하는 방식

 

 

 2-2.  모델체킹과 정리증명의 비교

구분	모델체킹(Model Checking)	정리증명 Automated Theorem Proving)
검증목표	-시스템 모델의 시스템 특성 만족 여부	-시스템 명세와 특성의 논리학적 정합성
사용기법	-정형명세 언어를 통한 시스템 명세(유한상태기계) -시스템 요구사항에 기반하여 시스템 특성 도출	-수학/논리학적 공리(Axiom), 규칙(Rule)을 활용하여 시스템명세/특성도출
장점	-모델 증명 도구를 통한 자동화 가능	-무한상태기계도 명세 및 증명 가능
단점	-유한상태기계만 명세 및 증명 가능	-시스템 명세 도출 및 증명이 매우 난해
활용 예	-CMU’s SMV, Bell/s SPIN, Berkeley’s VIS	-SPEAR(II), PVS

 

3. 모델체킹 적용시 유의사항