Formal Methods 정형 기법

- 수학적인 이론에 기반하여 소프트웨어와 하드웨어 시스템의 명세, 개발, 형식 검증을 위한 기술

- 안전/보안이 중요한 소프트웨어 및 시스템에서 사용됨

- 명확하고 정형적으로 정의된 semantics를 기반으로 함

- 자동화된 분석이 가능함 (시뮬레이션, 테스트케이스 생성, 정형 검증 등)

 

• 장점: 에러를 빨리 발견 가능, 제품 품질 향상
• 단점: 비용이 많이 들고 어려움

 

• 정형 명세(Formal Specification): 수리, 논리를 이용하여 시스템의 기능, 행위, 동작 환경을 기술하는 것.
  • 모호함을 없애는 것이 목적
  • 요구사항 간 inconsistency를 없애고 설계가 요구사항을 만족하는지 증명 가능
  • Finite State Machine, Statechart, Petri Net 등이 해당됨

 

• 정형 검증(Formal Verification): 수리, 논리를 이용하여 시스템의 명세, 설계, 요구사항을 검증. 모델 기반의 시뮬
  레이션 또는 테스팅(시스템의 행동들을 조사)
  • 조사되지 않은 부분은 치명적인 에러를 포함할 수 있음
  • 전문적인 지식이 필요
  • Model checking: 이상이 없으면 true, 있으면 false와 반례를 반환
  • Theorem proving
    • 수학적 증명. 매우 어려움.
    • 모든 종류의 input에 대하여 작동이 가능하다는 것을 보임.
    • state explosion의 문제에서 자유로움. (*state-explosion problem: 시스탬 내의 state 변수의 개수가 증가함에 따라 시스템 state space의 크기가 지수적으로 증가함)
  • Model checking
    • 자동화된 exhaustive search. 사용하기 쉬움. 강력한 디버깅 능력.
    • FSM에서 도달가능한 모든 상태에서 특정 properties를 만족하는지 확인.
    • 만족하지 않으면 반례 하나를 보여줌.
    • goal state -> initial state로 증명하고자 하는 property를 negation함으로써 정답인 반례를 얻음.
    • 증명하고자 하는 property를 temporal logic(시제 논리)으로 표현.
    • Model Checker: SMV(Symbolic Model Verifier) - language 변환기 존재
    • Temporal Operators
      • G g: Global, 항상 조건 g가 만족됨
      • f U g: Until, 조건 g가 만족될 때까지 f 조건 만족
      • X g: neXt, 다음에 조건 g를 만족
    • CTL: Syntax - 특성을 기술하는 방법. 시제논리 사용.
      • Path quantifier - A: for all paths, E: there exist a path
      • Path quantifier + Temporal Operator
•  

---

• Statechart
  • 기존의 state diagram은 state를 정의하는 파라미터의 모든 유효한 조합에 대하여 노드를 만들면서 복잡하고 가능성이 낮음. 
  • statechart는 그 내부에 multiple cross-functional state diagrams를 모델링하며 각각은 다른 state machine에 영향을 미치지 않고 내부적으로 transition이 가능함.
  • 시스템은 해당 상태에 해당하는 input에만 반응 → 이벤트가 발생했다고 가정하여 분석하는 등 모델을 사용할 수 있음 → 모델 수정 가능(몰랐던 요구사항의 오류를 수정 가능)
  • 모델을 만들면 자동적인 검증 도구를 이용하게 분석을 할 수 있음
  • 시뮬레이션 도구: 각각의 변수 값 변화에 따른 결과를 시각화: 직관적, 시각적. 내가 생각하지 못한 시나리오는 보지 못함.
  • Reachability(reachable) - 초기 상태에서 도달가능한지

• e[g] / A : e-event, g-guard(조건), A-sequence of actions
• entry / A : 들어올 때
• exit / A : 나갈 때
• do / A : State에 있을 때
• 독립적인 region를 표시(구분하는 점선이 and). 각 region이 end state가 되어야 밖으로 나갈 수 있음.

• parallelization node: initial node가 아닌 다른 노드로 직접 들어갈 수 있음
• synchronization node: end node가 아닌 밖의 다른 노드로 직접 나갈 수 있음
• Ⓗ - 얕은 이력(ShallowHistory; 같은 level state로)
• H*(동그라미) - 깊은 이력(DeepHistory; 마지막 active substate로)
• ChoicePoint(선택지점) - 여러 나가는 화살표를 가지는 동그라미
• JunctionPoint(분기) - 빨간 동그라미, 어떤 state에서 들어오더라도 한 개 이상의 output으로 나감
• broadcasting : 한 input이 여러 상태로 이동하게 함 

---

• Petri Net

• 사각형 - transition, 동그라미 - place (pre/post-condition)
• transition의 input인 모든 place가 토큰을 가져야 해당 transition이 발생가능함
• A -o B : inhibitor arc, A에 토큰이 없어야만 B가 발생(버퍼가 비어야만 넣을 수 있는 상황 등 표현)
• Initial Marking: 초기 상태의 토큰 표시
• Reachability graph: 각 place에 있는 토큰의 개수를 표시하고 상태 변화를 그림
• 모델이 크고 복잡해질 수록 이해하기 어려움 → high-level / colored petri net 사용
• high-level / colored petri net: 토큰의 변수명과 타입 정의, 기대하는 패킷(1)일 경우 받고 아니면 버림(null). 받으면 k+1(2)을 보내서 기대하는 패킷을 알림. 기존 petri net보다 표현력이 좋음.
• 모델링 툴: CPN → 그림을 자동으로 그려주며 어떤 상태가 도달가능한지 편리하게 알 수 있음.