형식 검증의 비즈니스 가치

게시일: 2025년 11월 22일 | 원문 작성일: 2020년 1월 22일 | 저자: Hillel Wayne | 원문 보기

이 글은 상사한테 형식 검증(Formal Methods, FM)의 이점을 설명하는 데 쓸 수 있는 “소개 자료”예요. 간단한 설명, 이점 목록, 사례 연구, 그리고 데모를 담고 있어요. 모든 예시는 TLA+로 되어 있지만, 논거는 Alloy, B, 상태 차트 등에도 똑같이 적용돼요. 여러분의 구체적인 필요에 맞게 조정해서 쓰세요.

간단한 주의: 형식 검증의 코드 검증 측면은 다루지 않을 거예요. 설계 검증이 훨씬 더 설득력이 있으니까요.

형식 검증이란

형식 검증(FM)은 디버그할 수 있는 설계예요. 시스템의 명세(specification)와 시스템이 가져야 할 속성들을 작성해요. 그러면 코드를 전혀 쓰지 않고도 설계를 직접 테스트하고 문제가 있는지 확인할 수 있어요. 문제가 있다면 그건 좋은 거예요, 잘못된 시스템을 구현하는 데 몇 주를 쓰기 전에 고칠 수 있으니까요. 문제가 없다면 올바른 걸 만들고 있다는 확신을 갖고 구현을 시작할 수 있어요.

왜 형식 검증을 쓸까요

비용을 절감해요. FM은 복잡한 시스템에서 복잡한 버그를 찾아내요. 시스템이 복잡할수록 버그가 테스트, QA, 모니터링을 빠져나갈 가능성이 높아요. 더 높은 수준의 설계에서 작동하기 때문에, 한 시간의 모델링이 며칠간의 테스트로도 놓칠 수 있는 이슈들을 잡아내요. 그리고 전체 시스템을 작성할 필요가 없기 때문에, 버그가 구현되기 전에 잡을 수 있어요. 즉, 잘못된 코드를 다시 쓰느라 개발자 시간을 쓸 필요가 없다는 거죠.

형식 검증은 개발 시간과 유지보수 비용도 절약해요. 설계를 직접 테스트할 수 있다면 훨씬 더 간단한 시스템을 만들 수 있고, 훨씬 더 쉬워져요.

레거시 시스템에도 FM을 적용할 수 있어요. 사람들이 문제를 겪기 전에 잠재적 버그를 찾을 수 있죠.

복잡한 시스템을 다루고 있다면, 형식 검증은 “제시간에 예산 내로”와 “2개월 늦고 그 다음 2개월은 버그 수정에만 집중하기” 사이의 차이가 될 수 있어요.

데모

명세를 실제로 보여주는 데 쓸 수 있는 짧은 데모예요. 이 데모는 TLA+로 되어 있어요.

최소한의 탄소 배출권 거래 플랫폼을 생각해보세요:

• 모든 크레딧은 소유자가 있어요.
• 소유자는 다른 사용자에게 크레딧을 제안(offer)할 수 있어요. 받는 사용자는 제안을 수락할 수 있고, 그러면 크레딧 소유권이 그들에게 이전돼요. 또는 거부할 수 있고, 그러면 아무 일도 안 일어나요.
• 수락/거부는 비동기예요: 같은 크레딧을 여러 사람에게 제안할 수 있고 (거래를 구성하기 위해), 사람은 하루를 기다린 후 제안을 수락하거나 거부할 수 있어요.

여기에 심각한 버그가 있어요. 보이나요?

…

포기하셨나요? 여기 있어요:

1. Acme가 크레딧 C1을 가지고 있어요.
2. Acme가 C1을 Nologo에게 제안해요.
3. Nologo가 수락하기 전에, Acme가 C1을 Brandco에게 두 번째로 제안해요.
4. Brandco가 수락해요. 소유권이 Brandco에게 이전돼요.
5. Nologo가 수락해요. 소유권이 Nologo에게 이전돼요.

Brandco는 Nologo에게 크레딧을 제안하지 않았어요. Acme가 했죠. 하지만 소유권이 Brandco에서 Nologo로 이전됐어요. 이건 여러 이유로 매우 심각한 버그예요:

• 복잡해요. 세 사람과 네 단계가 필요해요. 단위 테스트는 이걸 찾지 못할 거예요.
• 미묘해요. 유일한 증상은 크레딧이 사람들 계정에서 신비롭게 사라지는 거예요. QA와 모니터링은 이걸 찾지 못할 거예요.
• 위험해요. 시스템의 핵심 요구사항을 위반해요. 고객들이 돈을 잃고 당신을 신뢰하지 않게 만들 거예요.

미묘하고, 복잡하고, 위험해요. 이런 게 비용이 많이 드는 버그예요. 이 버그가 프로덕션에 오래 있을수록 더 많은 돈을 잃어요.

대조적으로, 명세를 쓰면 어떻게 되는지 봐요:

__CODE_UNDER_0__가 시스템의 요구사항이라고 말함으로써, 모델 체커한테 설계가 그 요구사항을 위반하는지 확인하라고 할 수 있어요:

모델 체커가 2초 만에 오류를 찾았어요. 6분도 안 돼서 시스템을 설계하고 비용이 많이 드는 버그를 찾았어요. 버그를 재현하는 단계 세트도 있어서, 코드 자체에 회귀 테스트를 작성할 수 있어요.

왜 형식 검증을 쓰지 않을까요

사람들이 단점을 물어보거나, 이게 유용할지 확신이 없는 경우를 위한 거예요.

명세는 레거시 시스템과 모든 프로그래밍 언어에서 작동할 만큼 유연해요. 이에 대한 트레이드오프는 자동 코드 변환이 없다는 거예요: 설계를 가져다가 자동으로 일치하는 코드를 생성할 수 없어요. 그건 유연성을 희생하는 대가로 올 거예요. 어떤 언어에서도 쓸 수 없고 레거시 코드에도 쓸 수 없을 거예요. 코드가 설계와 100% 일치하는지 절대적으로 확신해야 한다면 다른 도구가 필요해요. 그리고 일치하는지 확인하는 데 많은 시간과 돈을 써야 할 거예요.

명세 작성은 복잡한 시스템에서 작업할 때 가장 좋아요. 전체 시스템을 “머릿속에” 담을 수 있거나, 복잡한 로직이 많이 포함되지 않았다면, 명세가 큰 이점을 제공하지 않을 수 있어요. 대략적인 경험칙으로, 구현하는 데 일주일도 안 걸릴 것들을 명세화하는 건 노력할 가치가 없다고 생각해요.

마지막으로, 명세는 잡히지 않은 예외나 처리되지 않은 null 같은 단순한 구현 오류를 찾는 데는 그다지 좋지 않아요. 버그가 단순하거나 비용이 낮을 거라는 걸 안다면, 명세보다는 테스트와 QA로 찾을 가능성이 높아요.

상사를 설득할 수 있다면, 제 서비스도 받아보는 게 어때요?

컨설팅

AWS 논문은 사람들이 몇 주 안에 TLA+의 기본을 배울 수 있다고 해요. 하지만 그건 혼자서예요. 숙련된 강사의 도움이 있다면, 학생들은 3일도 안 돼서 배울 수 있어요.

저는 명세 언어를 가르치는 데 가장 경험 많은 강사 중 하나예요. TLA+를 위한 온라인 리소스와 책을 썼고, 현재 Alloy를 위한 새 문서를 작업 중이에요. 제 워크샵은 3일 내내 실습, 그룹 연습, 실전 경험이에요: 체크박스를 채우는 게 아니라 실제로 사람들을 가르치는 거죠. 여기서 더 읽고 여기로 이메일 주세요.

피드백을 준 Colin Curtin, Peter Bhat Harkins, Jay Parlar에게 감사드려요.