정형 기법(영어: formal methods, 형식 수법)은 컴퓨터 과학, 특히 소프트웨어 공학 분야에서 소프트웨어와 하드웨어 시스템의 명세(specification), 개발, 형식 검증(formal verification)을 위해 수학적 기반 기술을 활용하는 방법론을 총칭한다.
이 용어의 사용은 시스템 설계 과정에서 수학적 분석을 수행함으로써 다른 공학 분야와 마찬가지로 설계의 신뢰성과 내구성을 확보할 수 있다는 기대에서 비롯되었다.
정형 기법은 이론 전산학의 다양한 기초 이론의 응용으로 이해될 수 있다. 구체적으로 논리 계산, 형식 언어, 오토마타 이론, 프로그램 의미론, 형 체계, 대수적 자료형 등이 그 기반이 된다.
정형 기법의 적용 과정은 크게 두 가지로 나누어진다. 첫째는 정형 명세(formal specification)로, 대상 시스템의 기능이나 요구사항을 논리식과 같은 정형 언어로 기술하는 과정이다. 둘째는 정형 검증(formal verification)으로, 기술된 정형 언어에 수학적 증명 기법을 적용하여 시스템의 안전성, 신뢰성, 보안성 등을 확인하는 과정이다.
정형 기법은 안전 필수(safety-critical), 임무 필수(mission-critical), 보안 필수(security-critical) 시스템에서 특히 중요하게 여겨진다. 대표적인 적용 사례로 항공 전자, 의료 기기, 철도 신호 체계, 핵심 보안 시스템 등이 있다. 관련 표준으로는 자동차 소프트웨어 개발 프로세스를 다루는 ISO 26262가 요구사항 작성 단계에서 준정형(semi-formal) 기법의 적용을 권고하는 사례가 있다.
대표적인 정형 기법 관련 언어 및 도구로는 Z 언어, VDM, B-method, 모델 검사기(model checker) 등이 알려져 있다. 다만 이러한 구체적 언어와 도구의 세부 사항은 다양하며, 그 활용 범위는 학술 연구와 산업 현장의 고신뢰성 시스템 개발 영역에 걸쳐 있다.
정형 기법은 수학적 엄밀성을 바탕으로 시스템의 정확성을 보장하는 것을 목표로 하지만, 적용에 전문성이 요구되고 초기 비용이 높다는 점에서 널리 상용화되지 못한 측면이 있다. 이에 따라 전통적으로 학계 중심으로 연구가 이루어져 왔으며, 최근 일부 금융 기술 기업 등에서 이를 실무에 적용하려는 시도가 보고되고 있다.
참고 자료로는 위키백과의 "정형 기법" 항목, 한국정보통신기술협회(TTA) 정보통신용어사전, 그리고 Jean François Monin과 Michael G. Hinchey의 저서 《Understanding Formal Methods》(Springer, 2003) 등이 있다.
