[SoftwareV&V] 08. Finite State Verification

[원문링크]

https://adorable-aspen-d23.notion.site/SoftwareV-V_08_Finite-State-Verification-014c6687b67c4252833ee0aac8421489

SoftwareV&V_08_Finite State Verification

[2021 - 1학기 수강한 Software V&V 강의 정리본입니다.]

(Software Verification & Validation)

 

Finite State Verification (Model check verification)

Learning Objectives

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

1. 개요

• 프로그램 execution 의 대부분 중요한 속성은 decidable하지 않다.Finite state verification can automatically prove some significant properties of a finite model of the infinite execution space.
• (finite state verification은 자동으로 infinite 한 execution space 를 증명한다.)
• trade-off를 잘 균형 맞춰야 한다.

2. Finite State Verfication

1) Cost of FSV

• 사람이 FSM만드는 비용 필요 + automated analysis를 위한 적절한 spec마련
• 반복적인 과정
  1. model 준비하기
  2. 검증
  3. 피드백
  4. 모델의 specification 수정
• (FSM + Property → Model Checker 넣으면 자동으로 검사해 줌)
• 모델이 너무 자세하면 > 무한히 돌아갈 수 있음
• 모델이 너무 밍밍하면 > 쓸데없는 output만 나옴

2) Finite State Verificaiton framework

• Program/Design에서 바로 Property를 체크할 수 없기 때문에 FSV를 수행한다.⇒ FSM만들어서 model checker에 넣고 자동으로 알고리즈믹하게 검사하기
• (Halting Problem : 아무리 해도 이게 끝날 지 안 끝날 지 알 수 없음.)

3) FSV의 적용

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

• Concurrent (multi-threaded, distributed, ...) system: 개발 환경과 field 환경이 달라서 sensitive 한 것
• : 철저히 test하기 힘든 것
• 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로 검사하겠다.

 

4. 문제점

1. State Space Explosion Problem

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

• Dining Philosophers - SPIN으로 deadlock 을 찾자

1. Model Correspondence Problem

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

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

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

⇒ Conformance testing (적합성 테스팅)

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

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

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

• 자바의 컴파일러는 instruction의 순서를 자기마음대로 바꾼다.⇒ code에서 문제가 발생하지 않더라도 model에서 문제가 발생할 수 있다.
• ⇒ model에서 문제가 발생하지 않더라도 code에서 문제가 발생할 수 있고
• SPIN에서 사용하는 PROMELA는 순서를 지정해줘서 순서가 바뀌지 않는다.

5. OBDD (Ordered Binary Decision Diagram)

1. Intentional

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

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

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

1. OBDD - intentional model 사용

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

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

1. OBDD to Symbolic Model Checking (#142)

• 준비물
  1. FSM→OBDD로 변경한 Model
  2. Logic → OBDD로 변경한 Property
  ⇒ Model Checker에 넣으면 Algorithmic verification을 구현해준다.
• True : Model이 Property를 만족한다.
• False : property를 만족하지 않고 Counter example을 제공 해준다.
• a ⇒ b and c(=) not a or (b and c)

6. Intentional VS Explicit Representations (#145)

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

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

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

• S가 엄청나게 큰 집합일 경우에 Explicit하게 S를 나타내는 방법은 특정한 subset의 원소들을 그냥 나열하는 것의 평균보다 효율적이어질 수 없다.→ 물론 intentional한 경우가 explicit보다 더 최악인 경우 (n+1) 검사하는 경우도 있을 수 있지만 ordering을 잘 한다면 intentional이 더 효율적이라고 할 수 있다.
• ⇒ 따라서 intentional한 표현이 규칙적으로 state space를 잘 활용한다면 explicit보다 더 잘 동작할 수 있다.

7. Model Refinement (수정)

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

→ FSV는 Iterative process가 필요

1. Adding details to the Model (모델을 더 자세히)

• Initial Model은 간단하지만, Final Model은 실제 프로그램의 실행과 상응한다.

1. Adding Premised to the Property(Property에 제한 조건 추가)

• 제약조건을 추가하면 가짜 행동을 제거할 수 있다.

⇒ 언제까지 iterative?

: verification이 성공하고, 타당한 counter example을 만들 때 까지

Summary

• FSV와 tesing은 complementary(보완관계) 에 있다.ex) 거의 발생하지 않는 경쟁상태
• → 한계 ) scope 한계가 있어서, 모든 에러를 찾을 수는 없다.
• → test 할 수 없는 버그를 찾을 수 있을 것이다.
• Checking Model은 model checker를 이용해서 자동으로 진행한다.
• 좋은 모델을 만드는 것은 힘들다.→ 반복적인 싸이클이 필요하다. (model, check, refine)
• → abstraction, granularity(섬세함), 체크되어야 하는 Property 등을 신경써야 함