컴퓨터 과학에서 정형 기법(영어: formal methods) 또는 형식 수법소프트웨어하드웨어 시스템의 명세, 개발, 형식 검증을 위한 특정한 종류의 수학적 기반 기술이다.[1] 소프트웨어, 하드웨어 디자인의 정형 기법의 이용은 다른 공학 분야처럼 적절한 수학적 분석을 수행하면 디자인의 신뢰성과 내구성에 도움이 될 수 있다는 기대에서 비롯된다.[2]

Z 언어를 이용한 형식 명세서의 예

정형 기법은 매우 다양한 이론 전산학 기초의 응용(특히 논리 계산, 형식 언어, 오토마타 이론, 프로그램 의미론, 더 나아가 소프트웨어와 하드웨어 명세 및 검증의 문제에 대한 형 체계, 대수적 자료형)이라고 말할 수 있다.[3]

참조 편집

  1. R. W. Butler (2001년 8월 6일). “What is Formal Methods?”. 2006년 11월 16일에 확인함. 
  2. C. Michael Holloway. “Why Engineers Should Consider Formal Methods” (PDF). 16th Digital Avionics Systems Conference (27–30 October 1997). 2006년 11월 16일에 원본 문서 (PDF)에서 보존된 문서. 2006년 11월 16일에 확인함. 
  3. Monin, pp.3-4

참고 문헌 편집

  • Jean François Monin and Michael G. Hinchey, Understanding formal methods, Springer, 2003, ISBN 1-85233-247-6.
  • Jonathan P. Bowen and Michael G. Hinchey, Formal Methods. In Allen B. Tucker, Jr. (ed.), Computer Science Handbook, 2nd edition, Section XI, Software Engineering,Chapter 106, pages 106-1 – 106-25, Chapman & Hall / CRC Press, Association for Computing Machinery, 2004.
  • Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods. In Philip A. Laplante (ed.), Encyclopedia of Software Engineering, Taylor & Francis, 2010, pages 308–320.

외부 링크 편집