'자동 추론 (Automated Deduction)'에 해당되는 글 1건

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. 모델체킹 적용시 유의사항

'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와 함께 살아가는 삶

,