정형적 명세 기법

기법		설명
상태모형 기반 (모델기반)	- 시스템을 상태모형으로 인식, 집합과 수열 등의 수학적 요소로 표현  - 시스템에 있는 오퍼레이션(연산)들이 시스템의 상태를 어떻게 변화시키는가에 초점  - 시스템연산이 어떻게 시스템 모델의 상태에 영향을 미치는 지를 정의하여 시스템 연산을    정의할 수 있다.
	Z	• 집합론(Set Theory), 논리, 모델기반 명세기법 • 논리를 기반으로 한 Calculus 적 표현을 사용하여 여러 특성을 VDM보다    함축적으로 표현. • 모든 특성을 스키마안에 순서대로 기술하며 모듈화와 재사용성이 우수함 • Z스키마 구조 - 스키마 이름, 스키마 시그니쳐, 스키마 술어 • 모듈간의 재사용성이 우수하다. • 스키마간의 연산이 가능하다.
	VDM	Vienna Development Method • 시스템의 비기능적인 요구사항을 제외한 기능적인 요구사항에만 한정되   며 이와 관련한 기능 요구 명세와 검증 설계에 관해 적절한 표기법인    검증 방법을 제공함.
	Decision Table  (판단표)	• 복잡한 의사결정논리를 기술하는데 사용되며,    판단표는 4개의 4분원으로 구성
	Event Table (사건표)	• 여러 사건이 상이한 조건하에서 발생되었을 때 취해야 할 행위를 기술
	Transition Table (전이표)	• 시스템내의 상태변화를 기술하는데 사용됨.
	finite state machine  (유한상태기계	FSM • 컴퓨터 프로그램과 전자논리회로를 설계하는데에 쓰이는 수학적 모델이다. • 유한한 개수의 상태로 구성된 하나의 기계를 의미한다. • 일종의 Flow chart 로서 조금 다른 점은 닫혀있다는 것.    즉 모든 게임은 단발로 끝나는게 아니라 영원히 도는 프로그램임.
	Petri Net	• 그래프에 의한 표기법을 제공하며, 병렬 처리를 기술할 때 유한상태기계의   한계성을 극복하도록 고안되었다
대수학적 기반	• 오퍼레이션들과 이들 사이의 관계로 시스템을 표현하며, • 시스템을 분할된 서브시스템들의 인터페이스로 본다. • 클래스나 추상데이터타입을 오퍼레이션 사이의 관계들로 정의하 것과 유사하다. • 대수명세는 객체 연산이 객체 상태와 독립적인 경우에 인터페이스를 정의하는데    이용될 수 있다.   즉 연산을 적용한 결과는 앞의 연산과 무관하다는 것이다 예) Larch, OBJ, Lotos
관계형표기법	함의방정식	문제의 해결방법을 기술하지 않고 해법의 성질을 기술
	순환관계
	대수공리
	정규표현

1. 모델기반 명세기법 - Z, B, VDM
2. 대수적 명세기법 - LARCH, OJB, Lotos

종류	순차언어	병렬언어
대수학적 명세	Larch, OBJ	Lotos
모델기반 명세	Z,VDM,B	Petri Nets, CSP

정형명세의 특징
 - 엄격하고 오류없는 소프트웨어 개발에 적합
 - 소프트웨어의 신속한 인도 및 Time To Market 이 요구되는 경우에는 부적합
 - 확장성이 떨어짐
 - 규모가 작고 중요한 커널시스템 등에 많이 쓰임.



정형기술검토(FTR)

- SW 엔지니어가 수행하는 SW 품질보증 활동   - 개발자들이 모여 산출문서 등을 검토하여 산출물의 오류를 발견하기 위한 공식적인 활동 1. 제품을 검토하다 2. 논쟁과 반박을 제한 3. 해결책이나 개선책에 대해서 논하지 말것. 4. 의제를 정하고 그것을 유지 (시간일정 할당) 5. 문제 영역을 명확히 표현 6. 작성할 노트준비(사전준비 강요) 7. 참가자의 수를 제한 8. 모든 검토자를 위한 의미있는 교육 실행 9. 초기검토를 재검토