상태폭발: 정형검증 : 정리증명(수학/명제)/모델체킹(자동검증/입력모형)/SAT(불린?함수이용/성공여부판단)/이퀄발란스체킹(FSM/BDD or SAT 2개만선택, 결과를 비교)

1.
  가.개념 : 주어진 시스템 또는 컴포넌트의 모든 요구사항에 대한 테스트 또는 테스트 케이스의 평가척도 
              제공위한 구조기반 기법
  나.중요성 : SW품질의 정량화, SW오류원인/분포 탐지
2.
  가.종류 
    1) 제어흐름기반 : 구문(SC), 결정(DC), 조건/결정(C/DC), 변형조건결정(MCDC), 다중조건(MCC)
    2) 자료흐름기반 :All Node(AN, 보장성 낮음), 
                     All Edge(AE, 효율적), 
                     All Defs(AD, 특정변수 값이 변경전에 활용되도록 Path 설정, 간단), 
                     All Uses(AU, 노드의 변수에 대해 dcu, dpu 만족하는 Path 선정, AN 포함), 
                     All DU Paths(모든 Path를 포함시켜 테스트케이스 선정, AU보다 강력)
  나.최적화 방법 
    - Pairwise Test, Orthogonal Array Test, Mutation Test 통한 테스트케이스 최적화하여 테스트 
      투입 비용 효율성 확보 필요