정형 검증 (formal verification)
쉽게 풀면
정형 검증은 테스트처럼 몇 가지 경우만 실행해 보고 '잘 동작하는 것 같다'고 확인하는 것이 아니라, 수학적 증명을 통해 '가능한 모든 입력과 상황에서 이 시스템은 절대 특정 오류를 일으키지 않는다'는 것을 논리적으로 보장하는 방법이다. 항공기 제어 소프트웨어나 CPU 설계, 암호 프로토콜처럼 오류가 치명적인 결과를 낳는 시스템에서 특히 중요하게 쓰인다. 정리 증명기(theorem prover)나 모델 체커 같은 도구를 이용해 수행된다.
왜 중요한가
테스트는 확인한 경우에 대해서만 정확성을 보장하지만, 정형 검증은 원칙적으로 가능한 모든 경우에 대한 보장을 목표로 하기 때문에 컴퓨터과학에서 신뢰성이 극도로 중요한 시스템을 다루는 연구의 핵심 축을 이룹니다. CPU나 컴파일러 같은 기반 소프트웨어부터 스마트 컨트랙트, 자율주행 제어 로직에 이르기까지, 오류가 큰 비용이나 인명 피해로 이어질 수 있는 분야일수록 정형 검증 기법을 적용한 논문이 많이 나옵니다.
논문에서는 이렇게 쓰입니다
테스트만으로는 보장할 수 없는 시스템의 안전성이나 정확성을 수학적으로 증명했음을 강조할 때 사용된다.
컴파일러가 코드를 최적화하는 과정에서 프로그램의 동작 자체가 바뀌지 않는다는 사실을 수학적으로 확인했다는 뜻입니다.
블록체인 상의 자동 계약 코드가 특정한 잘못된 상태에 절대 빠지지 않는다는 것을 논리적으로 보였다는 의미입니다.
조금 더 깊게 보면
정형 검증은 크게 두 가지 접근으로 나뉘는 경우가 많은데, 하나는 사람이 보조 도구(정리 증명기)를 이용해 단계적으로 증명을 구성하는 방식이고, 다른 하나는 상태 공간을 자동으로 탐색해 속성 위반 여부를 확인하는 모델 체킹 방식입니다. 후자는 자동화 수준이 높지만 상태 공간이 커질수록 계산량이 급격히 늘어나는 상태 폭발 문제가 흔히 언급됩니다. 또한 검증 대상 시스템이 실제로 무엇을 만족해야 하는지를 기술하는 명세 언어(specification language)를 어떻게 작성하느냐가 검증 결과의 의미를 좌우하기 때문에, 명세 작성 자체도 정형 검증 연구의 중요한 부분으로 다뤄집니다.
주의할 점
정형 검증은 명세 자체가 정확하다는 전제 위에서 성립하므로, 명세가 실제 요구사항을 잘못 반영하고 있다면 검증이 통과해도 실제 시스템에 문제가 있을 수 있다.