정형 기법 (Formal Methods)

정형 기법 (Formal Methods)

수학적 표기법과 논리적 추론을 사용하여 소프트웨어/시스템의 명세, 설계, 검증을 수행하는 기법

목적: 정확한 명세, 논리적 검증, 결함 조기 발견, 안전성 증명

Z 표기법 (Z Notation)

• •집합론과 1차 술어 논리 기반
• •스키마(Schema) 구조로 상태와 연산 기술
• •ISO 표준(ISO/IEC 13568), 학계에서 널리 사용

VDM (Vienna Development Method)

• •IBM 비엔나 연구소 개발, 모델 기반 명세
• •VDM-SL(명세 언어), 정제(Refinement)를 통한 단계적 개발
• •산업계 적용 사례 다수

Petri-Net

• •동시성, 동기화, 분산 시스템 모델링에 적합
• •Place(상태), Transition(이벤트), Token(자원) 구조
• •데드락/라이브니스/도달 가능성 분석 가능
• •변형: CPN(Colored Petri-Net), 시간 Petri-Net

모델 검사 (Model Checking)

• •시스템 모델의 모든 상태를 자동 탐색하여 속성 검증
• •도구: SPIN, NuSMV, UPPAAL
• •장점: 자동화, 반례 제공
• •단점: 상태 폭발 문제

정리 증명 (Theorem Proving)

• •수학적 증명으로 프로그램 정확성 검증
• •도구: Coq, Isabelle, Lean
• •완전 검증 가능, 자동화 한계

비교: Z/VDM(명세중심/상태기반) vs Petri-Net(동시성/그래프) vs 모델검사(자동/상태폭발) vs 정리증명(완전/수동)

연관: 안전 필수 시스템, DO-178C, MISRA-C, 정확성 검증