[SoftwareV&V] 05. Finite Models

[원문링크]

https://adorable-aspen-d23.notion.site/SoftwareV-V_05_Finite-Models-95a4069f07c64b179bfa2ea5478d0f34

SoftwareV&V_05_Finite Models

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

(Software Verification & Validation)

 

Basic Techniques - Finite Models

: Test & Analysis 와 개발 프로세스는 함께 움직여야 한다! (개별적 NO!)

Learning Objectives

• Finate state abstraction의 Goal과 함축적 의미 파악하기
• program control > Control Flow 모델링 하는 법 배우기
• sw system structure > Call graph 모델링 하는 법 배우기
• finite state behavior > Finite State Machine 모델링 하는 법 배우기

1. 기본 용어

• Model : artifact를 추상화 시켜서 simple해진 것
• Directed graph with Labels
• : 방향 그래프의 노드에 program의 코드를 넣음 (program execution 표현 가능)
• Finite Abstractions
  1. Corsening of execution model : 모델이 정교하지 않게 된다.
  2. 2) Introduction of nondeterminism : 어떤 것을 선택해야 할지 모름

2. Control Flow Graph (Intraprocedural)

: 프로그램이 실행 중에 횡단할 수 있는 모든 경로를 그래프 표기법을 사용하여 표현한 것

https://ko.wikipedia.org/wiki/제어_흐름_그래프

• Node = basic block : maximal program region(single entry and single exit point)
• 프로그램에서 추출 가능하다.

1. CFG의 용도

• Testing의 철저한 기준을 세우기 위할 때
• 철저한 criteria를 세우는 다른 model을 정의할 때
• ex) LCSAJ (Linear code sequence and jump)

3. Call Graphs (Interprocedural)

: 컴퓨터 프로그램의 서브 루틴 간의 호출 관계를 나타내는 제어 흐름 그래프입니다.

• Node : Procedures, methods, functions
• CFG보다 design issue와 trade-off가 더 많다.
  • call relation의 과대평가
  • : 절대 실행되지 않는데 그려 놓는 것도 있음.
  • context의 sensitive(파라미터 등 존재)/ insensitive (일반적임)

4. Finite State Machines

: 유한한 상태를 가진 추상기계, 한 번에 하나의 상태만을 가질 수 있으며 Event에 의해 전이(transition)가능하다.

• 코드 작성 이전에 완성되며(requirement, design 단계) , specification으로의 역할을 수행한다.
• CFG ↔ FSM 왔다 갔다 가능
• Nodes : 유한한 states
• SRS, SDS를 가지고 FSM을 만들고, code가 작성된다. 이후 CFG 만들어짐
• FSM을 모델링 하기 위한 abstract function
• : CFG를 만들 때는 기계적으로 가능하지만 FSM을 만들기 위해서는 사람의 개입이 필요하다.

Summary

• Model은 단순해야 한다.
• Model은 충분히 자세해야 한다.
• CFG는 software program으로 부터 만들어진다.
• FSM은 code작성 전(sw program 전) 에 document behavior를 위해서 만들어진다.