테스트의 한계와 형식 기법 — 「부재」 를 증명하는 또 하나의 길

제 1 화 에서, 테스트라는 행위의 원점으로 하나의 경구를 놓아두었다. 에츠허르 다익스트라 (Edsger W. Dijkstra) 는 1969 년 NATO 소프트웨어 공학 회의에서의 논의를 거쳐, 1970 년 논문 「Notes on Structured Programming」 (EWD249) 에 다음과 같이 적었다.

“Program testing can be used to show the presence of bugs, but never to show their absence!” (프로그램 테스트는 버그의 존재를 보이는 데는 쓸 수 있지만, 버그의 부재를 보이는 데는 결코 쓸 수 없다)

테스트는 유한 개의 입력 · 경로를 실행한 결과에 지나지 않는다. 무한한 입력 공간을 가진 프로그램에 대해, 「시도한 범위에서 버그가 나오지 않았다」 는 것은 보일 수 있어도, 「시도하지 않은 범위에 버그가 없다」 는 것은 원리적으로 아무것도 보장하지 못한다. 이는 테스트를 꼼꼼히 한다고 해결되는 문제가 아니라, 테스트라는 방법 자체가 지닌 구조적 한계다.

이 글은 그 한계를 어떻게 메워왔는가 하는 반세기에 걸친 대답 —— 형식 기법 (Formal Methods) 을 따라간다. 수학적으로 엄밀한 표기법으로 시스템을 기술하고, 그 시스템이 명세를 만족함을 수학적으로 증명 · 검증하는 접근법의 총칭이다.

테스트가 닿지 않는 영역

형식 기법은 「테스트의 상위 호환」 이 아니다. 둘은 강점을 발휘하는 영역이 다르다.

	테스트	형식 기법
대상	실제로 동작하는 코드	명세 (모델) 또는 코드 자체
보증의 성질	표본 추출적	망라적
결함 부재의 증명	불가능	조건부로 가능
비용	상대적으로 낮음 ~ 중간	상대적으로 높음
강점 영역	통합 부분 · 실제 환경 의존 · UI	병행성 · 프로토콜 · 분산 정합성

형식 기법이 특히 힘을 발휘하는 것은, 테스트로는 검출하기 어려운 병행성 버그 · 분산 시스템의 정합성 · 프로토콜의 안전성 (safety) 과 생존성 (liveness) 같은 성질이다. 실무에서는 핵심이 되는 알고리즘이나 프로토콜에만 형식 기법을 적용하고, 주변부는 기존의 테스트로 담보하는 「구분 사용」 이 일반적이다.

모델 체킹 — 모든 상태를 기계적으로 훑다

모델 체킹 (Model Checking) 은 시스템의 동작을 유한 상태 기계로 모델링하고, 그 모델이 취할 수 있는 모든 상태 를 망라적으로 탐색하여, 지정한 성질이 항상 성립하는지를 자동으로 검증하는 기법이다.

이론적 기반은 1980 년대 초, 에드먼드 클라크 (Edmund Clarke) 와 앨런 에머슨 (E. Allen Emerson), 그리고 독립적으로 조제프 시파키스 (Joseph Sifakis) 에 의해 확립되었다. 세 사람은 이 공적으로 2007 년 ACM 튜링상을 수상했다.

가장 큰 과제는 상태 폭발 문제 (State Explosion Problem) —— 병행 프로세스 수나 데이터가 취할 수 있는 값이 늘어날수록, 상태 공간이 지수적으로 증가한다. 이에 대응하기 위해 켄 매밀런 (Ken McMillan) 등에 의한 이진 결정 다이어그램 (BDD) 을 이용한 기호적 모델 체킹이나, 유계 모델 체킹 같은 기술이 발전했다.

SPIN 과 TLA+ — 병행성을 검증하는 두 대표 도구

SPIN 은 벨 연구소의 제라드 홀츠먼 (Gerard Holzmann) 이 개발한 모델 체킹 도구로, 병행 시스템의 검증에 특화되어 있다. 명세 기술 언어 Promela (Process Meta Language) 를 사용해, 통신 프로토콜이나 멀티스레드 프로그램의 안전성 · 데드락 유무를 검증한다.

TLA+ (Temporal Logic of Actions) 는 분산 시스템 연구의 일인자이자 Paxos 알고리즘 의 고안자로도 알려진 레슬리 램포트 (Leslie Lamport, 2013 년 ACM 튜링상 수상) 가 개발한 형식 명세 기술 언어다. 집합론과 시제 논리에 기반해 시스템의 상태 전이를 수학적으로 기술한다. 함께 딸린 모델 체커 TLC 를 사용하면, 유한한 범위에서 모델을 망라적으로 검증할 수 있다. 프로그래머에게 친숙한 의사코드 형태의 표기법 PlusCal 도 마련되어 있으며, 이는 TLA+ 로 변환된다. 램포트는 저서 『Specifying Systems』 (2002 년) 에서 TLA+ 를 체계적으로 해설했다.

이 외에도, MIT 의 Daniel Jackson 이 개발한 Alloy 는 일계 술어 논리에 기반한 관계 논리로 데이터 모델과 구조적 제약을 기술하는 경량 언어로, 부속 도구인 Alloy Analyzer 가 지정 범위 내의 모든 인스턴스를 탐색해 반례를 찾아낸다. 하드웨어나 유한 상태 프로토콜의 검증에 쓰이는 NuSMV, C/C++ 를 직접 대상으로 SAT/SMT 솔버로 검증하는 CBMC 등, 추상도가 다른 계층을 커버하는 도구들이 용도에 따라 구분되어 쓰인다.

AWS 의 실천 — 구현 전에 버그를 잡다

형식 기법이 학술적 관심에 머무르지 않고 산업 실무에서 성과를 낸 사례로 널리 알려진 것이, 아마존의 AWS 팀에 의한 TLA+ 활용 이다. 크리스 뉴컴 (Chris Newcombe) 등의 논문 「How Amazon Web Services Uses Formal Methods」 (Communications of the ACM, 2015 년) 은, DynamoDB · S3 · EBS 등 여러 핵심 서비스의 설계에 TLA+ 를 적용해, 테스트나 설계 리뷰만으로는 발견이 극히 어려웠던 미묘한 병행성 버그 (드문 타이밍에서만 발생하는 데이터 불일치 등) 를 구현 이전의 설계 단계에서 다수 발견할 수 있었다고 보고한다. 「대규모 분산 시스템의 정확성은 구현 후의 테스트만으로는 담보할 수 없다」 는 것을 보여주는 사례로, 지금도 자주 인용된다.

정리 증명 — 증명 자체를 프로그램으로 쓰다

모델 체킹이 유한한 상태 공간을 자동으로 망라 탐색하는 것과 달리, 정리 증명 (Theorem Proving) 은 더 표현력이 높은 논리 체계 (고차 논리 · 타입 이론 등) 를 이용해, 대개 사람의 도움을 받으며 수학적 증명을 구축하는 접근법이다. 무한한 상태를 가진 시스템의 정확성도, 유한한 증명 절차로 보일 수 있다.

대표적인 증명 보조기 (Proof Assistant):

도구	개발처 · 관계자	이론적 기반
Coq	INRIA (프랑스), Thierry Coquand 등이 기초 이론을 고안	귀납적 구성의 계산
Isabelle/HOL	케임브리지 대학의 Larry Paulson, 뮌헨 공과대학의 Tobias Nipkow 등	고차 논리
Lean	Leonardo de Moura (Microsoft Research 에서 개발 시작, 이후 AWS 등이 지원)	의존 타입 이론

이들 도구는 커리-하워드 대응 (「명제는 타입이고, 증명은 프로그램이다」 라는 대응 관계) 에 기반하며, 증명을 쓰는 것이 프로그램을 쓰는 것과 수학적으로 동치가 된다는 점이 특징이다.

CompCert 와 seL4 — 「버그가 제로」 임을 증명하다

저명한 응용 사례로, CompCert (Xavier Leroy 등이 Coq 로 형식 검증한 C 컴파일러) 와, seL4 (NICTA, 이후의 CSIRO · Data61 이 2009 년에 발표한, 기능적 정확성을 완전히 형식 검증한 마이크로커널. Isabelle/HOL 을 사용) 를 들 수 있다. 이들은 「컴파일러나 OS 커널의 핵심 부분에 버그가 전혀 없다」 는 것을 수학적으로 증명한 몇 안 되는 실례로, 일반적인 테스트로는 도달 불가능한 보증 수준을 보여준다.

계약에 의한 설계 — Eiffel 이라는 또 하나의 길

계약에 의한 설계 (Design by Contract, DbC) 는 버트런드 마이어 (Bertrand Meyer) 가 1986 년에 개발한 언어 Eiffel 에서 도입한 설계 기법으로, 형식 기법과 테스트의 중간에 위치하는 「경량 형식 기법」 의 대표 사례다.

• 사전 조건 (precondition) —— 호출하는 쪽이 보증해야 할 조건
• 사후 조건 (postcondition) —— 구현하는 쪽이 실행 후 보증하는 조건
• 불변 조건 (invariant) —— 객체의 생애 주기 내내 항상 성립해야 할 조건

이들을 표명 (assertion) 으로 코드에 명시하고, 실행 시에 점검함으로써 계약 위반을 즉시 검출할 수 있다. Eiffel 외에도, Java (옛 JML), Python (assert 문이나 icontract 라이브러리), Racket (contract 메커니즘), Ada/SPARK 등 많은 언어에 비슷한 사고방식이 도입되어 있다.

안전 필수 시스템이라는 최전선

형식 기법이 가장 일찍부터 제도적으로 요구되어 온 영역이, 사람의 생명과 직결되는 안전 필수 시스템 (safety-critical system) 이다.

파리 메트로 14 호선 (Météor) 은 장 레몽 아브리알 (Jean-Raymond Abrial) 이 고안한 형식 명세 표기법 B-Method 를 이용해, 무인 운전 자동 열차 제어 시스템이 개발 · 검증된 사례로 알려져 있다. 1998 년에 개통한 이 노선은, 형식 기법이 실제 상업용 대규모 시스템에서 실용화된 대표 사례로 자주 인용된다.

SPARK (Ada 언어의 부분집합에 사전 조건 · 사후 조건 · 데이터 흐름 계약을 더한 언어) 는 정적 분석을 통해 런타임 오류 (배열 범위 초과 · 오버플로 등) 의 부재를 수학적으로 증명할 수 있어, 항공 · 방위 분야에서 널리 쓰인다. 민간 항공기 소프트웨어의 인증 기준 DO-178C 는 개발과 검증의 엄격한 프로세스를 요구하지만, 최근 판에서는 모델 기반 개발이나 SPARK 같은 형식적 분석 기법의 활용도 인증 근거로 인정되고 있다.

경량 형식 기법이라는 제 3 의 길

Daniel Jackson 은 Alloy 같은 「완전한 증명까지는 지향하지 않지만, 유한한 범위를 망라적으로 점검함으로써 많은 버그를 발견할 수 있다」 는 접근법을 경량 형식 기법 (Lightweight Formal Methods) 이라 불렀다. Coq 나 Isabelle 같은 「완전한 증명 (heavyweight)」 과 대비되는, 도입 비용과 효과의 균형을 잡기 위한 중요한 구분이다.

프로퍼티 기반 테스트 도 이 경량 형식 기법의 계보에 위치한다. 명세 (프로퍼티) 를 형식적으로 기술한다는 점은 형식 기법과 공통되지만, 망라적 탐색이 아니라 무작위 표본 추출로 검증한다는 점에서 모델 체킹과는 다르다.

타입 시스템이라는 가까운 형식 기법

정적 타입 시스템도, 넓은 의미에서는 「경량 형식 기법」 의 일종으로 볼 수 있다. 타입 검사는 컴파일 시점에 프로그램 전체를 대상으로, 어떤 종류의 불일치 (타입 불일치) 가 존재하지 않음을 기계적으로 보증한다. 이는 테스트가 지닌 「표본 추출적」 성질과는 대조적이다.

다만 타입 시스템이 검증할 수 있는 것은 「타입이 맞는가」 라는 한정된 성질에 그치며, 비즈니스 로직의 정확성이나 병행성의 안전성까지는 보통 다루지 않는다. 의존 타입 (Dependent Types) 을 가진 언어 (Idris · Agda · Lean 등) 에서는, 타입 자체에 임의의 논리 명제를 담을 수 있어, 타입 검사가 더 강력한 증명의 역할을 하기도 한다.

타입 시스템이 경량 형식 기법으로서 널리 실무에 스며든 최근의 예가, Rust 의 소유권 시스템 (ownership) 과 빌림 검사기 (borrow checker) 다. 컴파일 시점의 정적 검사를 통해, 메모리 안전성 (해제된 메모리에의 접근이나 이중 해제 등) 과 데이터 경합 (data race) 의 부재를 보증하는 구조로, 형식 기법적인 발상이 주류 언어의 컴파일러에 내장된 사례로 자리매김한다.

테스트와 형식 기법, 대립이 아니라 상호 보완

많은 현장에서는, 먼저 모델 체킹으로 설계 수준의 오류를 저렴하게 찾아내고, 특히 보증 수준이 높아야 하는 핵심 컴포넌트에만 정리 증명을 적용하는 단계적 접근이 취해진다. SPIN 과 TLA+ 는 병행 시스템과 프로토콜의 안전성 검증에, Coq · Isabelle · Lean 은 컴파일러나 OS 커널처럼 극히 높은 보증이 요구되는 영역에, 각각 강점을 지닌다.

제 1 화의 다익스트라의 경구는 테스트라는 행위를 부정하는 것이 아니다. 「테스트로 닿는 범위」 와 「수학으로만 닿는 범위」 의 경계선을 그었을 뿐이다. 그 경계선 너머를, 모델 체킹과 정리 증명이 반세기에 걸쳐 메워 왔다 —— 그것이 이 글의 결론이다.

다음 글에서는 시점을 「어떻게 검증하는가」 에서 「품질은 누구의 일인가」 로 옮긴다. 전담 테스터에서 모두의 품질로 —— 정확성의 증명을 넘어, 성능과 보안을 포함한 품질을 조직 전체가 어떻게 짊어지게 되었는지를 따라간다.