정형검증: Model Checking vs Theorem Proving

** 본 글은 차성덕 교수님의 소프트웨어공학이야기 책을 정리한 글입니다. **

Theorem Proving

• Theorem prover: Coq, Isabelle, PVS 등
  • Theorem prover의 사용법을 배우고 실제로 쓰기 위한 진입장벽이 높다.
  • Theorem prover를 사용하는 개인의 능력과 경험에 따라 증명의 성공 여부가 달라질 수 있다.
  • Theorem prover도 소프트웨어이므로 오류가 있을 수 있음을 명심해야 한다.
• 장점: 상태 폭발의 문제에서 자유롭다.

 

Model Checking

• 도달 가능한 모든 상태에 대해서 사용자가 검증하고자 하는 성질이 만족되는지를 자동적으로 분석한다.
• 장점: 사용이 쉽다. 증명과정 전체가 자동화되어 있다. 성공하면 true를 실패하면 반례를 출력한다
• 단점: 상태 폭발 문제에서 사용 불가능 (푸쉬푸쉬 lv.50)
  but 기술의 발전으로 분석 가능한 크기가 점점 증가하고 있으므로 계속 사용이 증가할 것.
• Finite State Machine으로 표현된 모델 + Temporal Logic 시제 논리로 표현된 증명하고자 하는 성질
• 종류: SMV (FSM, VHDL), SPIN, PathFinder (JAVA), SLAM
• SMV Model checker (모델을 자동으로 SMV input으로 변환 + 성질은 CTL computational tree logic으로 표현)
  
  • 실제 활용 사례 1: 푸쉬푸쉬 게임
    • 정확성을 검증하진 않지만 실제로 답이 존재하는지 검증 가능
    • 해법을 찾는 문제가 FSM의 reachability 문제로 정의될 수 있기 때문
    • 검증하고자 하는 특성을 (~Goal State) 라고 두고 Model Checking
      → Goal state로 가는 답이 없다면 true를 반환하겠지만, 답이 있다면 반례를 반환함.
      → 해당 반례가 바로 답이 됨.
  • 실제 활용 사례 2: 아리랑 2호 
    • AG AF stable - True: 소프트웨어가 부팅되고 난 후 언젠가는 작업을 수행할 수 있는 상태로 항상 도달한다.
    • AG(p->AF(복귀)) - False: p가 만족될 경우, 언젠가는 복귀할 것이다 - 반례 생성 - 추가 요구사항 발견

 

Temporal Logic

• AG: All path, globally
• AF: All path, in the future
• A...
• 예시 Temporal Logic
  • AG(p-> AF q): "p가 참이면, q 또한 언젠가는 참"이 되고 이 조건은 모든 경로에서 만족된다.
  •  AG AF p: "p가 언젠가는 참"이 되는 조건이 모든 경로에서 만족된다.

 

---