Finite State Verification (Model check verification)

Learning Objectives

• Testing과 FSV가 어떻게 서로를 보완하는지 알아보기
• cost와 정확도 사이에서 FSV 모델링하기
• implicit 모델과 explicit 모델 구분하기 ( 왜 implicit이 때때로 효과적인지)

1. 개요

• 프로그램 execution 의 대부분 중요한 속성은 decidable하지 않다.

  (finite state verification은 자동으로 infinite 한 execution space 를 증명한다.)

  Finite state verification can automatically prove some significant properties of a finite model of the infinite execution space.

• trade-off를 잘 균형 맞춰야 한다.

2. Finite State Verfication

1) Cost of FSV

• 사람이 FSM만드는 비용 필요 + automated analysis를 위한 적절한 spec마련

• 반복적인 과정

  (FSM + Property → Model Checker 넣으면 자동으로 검사해 줌)

  1. model 준비하기
  2. 검증
  3. 피드백
  4. 모델의 specification 수정

  

  • 모델이 너무 자세하면 > 무한히 돌아갈 수 있음
  • 모델이 너무 밍밍하면 > 쓸데없는 output만 나옴

  2) Finite State Verificaiton framework

  • Program/Design에서 바로 Property를 체크할 수 없기 때문에 FSV를 수행한다.

    (Halting Problem : 아무리 해도 이게 끝날 지 안 끝날 지 알 수 없음.)

    ⇒ FSM만들어서 model checker에 넣고 자동으로 알고리즈믹하게 검사하기

    

  3) FSV의 적용

  : 주로 직접 테스트하기 힘든 것을 FSV를 이용해서 검증한다.

  • Concurrent (multi-threaded, distributed, ...) system

    : 철저히 test하기 힘든 것

    : 개발 환경과 field 환경이 달라서 sensitive 한 것

  • Data models

    : "corner case"를 알아내기 힘든 것, 테스트하기 힘든 것

  • Security

    : 자주 발생하지 않는 위협(threats)

  4) Modeling Concurrent System

  → 좋은 FSM을 만드는 것이 어렵다.

  • 가정 simplify 하기

    : 쓰레드가 몇 개? , 각 쓰레드들의 FSM 만들기, 쓰레드들 간의 상호작용 하는 부분 찾기

  • System model의 State

    : 각 thread의 state들을 튜플로 나타내기

  • Transition

    

    Thread가 N개, 각 thread 당 state가 M개라고 하면 (M의 N승)

    ⇒ 사람이 할 수 없고 기계적으로 algorithm하게 만들어야 한다.

  3. Example) on-line purchasing system

  : 모든 상황을 가정할 수 없으니 FSV로 검사하겠다.

  • Specification

    

  • Implemetation

    

  • 코드 (double-checked locking idiom 사용)

    

    1) Analysis

    1. 각 thread의 FSM을 만들기

       : 가능한 모든 execution path를 지난다. (자동으로)

       

    ⇒ SPIN model checker를 이용해서 FSV

    2. PROMELA 언어로 시스템 모델링하기

    *PROMELA : 검증 모델링 언어로, SPIN 모델 검사기 분석 언어로 사용한다.

    

    spec에서 바로 PROMELA로 바꿀 수 있지만 어려울 수 있기 때문에

    Naive FSM으로 변경 후 바꾸기도 한다.

    3. SPIN 돌리기

    : 소프트웨어 모델링의 정확성을 확인하기 위한 도구로,

    검사 결과를 sequence diagram을 통해 반례를 나타내 준다.

    • Depth-first search를 통해 가능한 모든 경로를 모두 탐색한다.

      

    

    • Proc1,2,3의 모든 조합을 테스팅한다.
    • Assertion fail → 검증 일찍 끝남
    • Assertion fail 안남 → 정상적으로 동작한다. = property를 만족한다.

    4. 문제점

    1. State Space Explosion Problem

    : Systme의 state 수가 증가하면, 기하 급수적으로 증가하여 모든 process의 경우의 수를 검사하기 힘든 경우가 나온다.

    • Dining Philosophers - SPIN으로 deadlock 을 찾자

    

    2. Model Correspondence Problem

    :모델과 프로그램 사이의 문제

    • Blindly mirroring all details(너무 자세) → state space explosion
    • Omitting crucial detail(너무 밍밍) → false alarm

    ⇒ 모델로부터 소스코드를 자동적으로 만든다.

    ⇒ Conformance testing (적합성 테스팅)

    : FSV랑 testing의 tradeoff를 잘 조절해서 섞어 사용하기

    

    3. Granularity(세분성) (#139)

    : 적절한 세분성을 찾아야 한다.

    • 자바의 컴파일러는 instruction의 순서를 자기마음대로 바꾼다.

      ⇒ model에서 문제가 발생하지 않더라도 code에서 문제가 발생할 수 있고

      ⇒ code에서 문제가 발생하지 않더라도 model에서 문제가 발생할 수 있다.

    • SPIN에서 사용하는 PROMELA는 순서를 지정해줘서 순서가 바뀌지 않는다.

    5. OBDD (Ordered Binary Decision Diagram)

    1. Intentional

    : 무한한 가능한 state를 테스트 하는 것은 사실상 불가능하다.

    → space를 intentional(symbolic) 하게 바꿔서 줄일 수 있다.

    • Intentional model은 represent 크기가 크게 변하지 않는다. (explicit은 세트를 구성하는 수에 따라서 엄청 클 수도, 작을 수도)

    

    2. OBDD - intentional model 사용

    : Pair사이에 Transition이 존재할 때만 True이다.

    (길면 k+1까지, 짧으면 완전 짧음)

    

    3. OBDD to Symbolic Model Checking (#142)
    • 준비물

    6. Intentional VS Explicit Representations (#145)

    아주 큰 state의 집합 S가 주어졌을 때,

    • explicit는 representation이 선택한 요소들의 크기(길이)만큼인데,
    • intentional은 compact on average를 넘지 않는다.

    → Intentional representation이 structure(구조)와 regularity(규칙성)을 탐구할 때 잘 작동한다.

    • S가 엄청나게 큰 집합일 경우에 Explicit하게 S를 나타내는 방법은 특정한 subset의 원소들을 그냥 나열하는 것의 평균보다 효율적이어질 수 없다.

    7. Model Refinement (수정)

    • FSM을 개발할 때 precision과 efficiency 사이의 균형을 잘 잡아야 한다.

    → FSV는 Iterative process가 필요