eSpark는 TLA+를 사용해 세 가지 규칙을 모두 충족하는 설계가 없음을 증명한 뒤, 하나를 포기했다

초등학교를 위한 에듀테크 제공업체인 eSpark Learning은 모든 고객에 대해 수동의 반정기적 구성 프로세스를 운영했는데, 이는 여러 타사 시스템을 조율하고 고객의 IT 네트워크를 직접 수정했다. 사용자 기반이 성장하면서 업무량은 지속 불가능해졌고, 지원 팀은 유지하기 위해서만 매년 새로운 정규 직원을 한 명씩 채용해야 한다는 것을 깨달았다. 경영진은 항상 이 프로세스의 자동화를 너무 위험하다고 판단해 왔다. 실수 하나가 고객의 네트워크에 영향을 미쳐 계약을 잃을 수 있었기 때문이다.

엔지니어 Hillel Wayne은 최근 배치 업로더 프로젝트에 형식 명세(TLA+ 스타일)를 사용했고, 코드를 작성하기 전에 아키텍처 버그를 잡아내어 납기를 일주일 단축했다. 프로젝트 관리자는 자동화된 대체 시스템이 안전하려면 보장해야 하는 세 가지 속성을 정의했다. Wayne은 명세 언어로 시스템을 모델링하고 모델 검사기를 통해 실행했는데, 이 검사기는 명세가 허용하는 모든 시나리오를 철저히 시뮬레이션하고 규칙을 위반하는 시나리오를 발견하면 구체적인 추적을 반환한다.

이틀간의 모델링 후, 모든 설계는 즉시 깨지거나 몇 달 동안 프로덕션에서 눈에 띄지 않다가 붕괴될 수 있는 미묘한 결함을 포함하고 있었다. 일부 설계는 세 가지 필수 속성 중 두 가지를 충족했지만, 세 가지 모두를 충족하는 설계는 없었다. Wayne은 그냥 하나를 선택하고 희망하기보다는 프로젝트 관리자를 모델링 산출물로 끌어들여 각 설계가 어떻게 실패할지 구체적으로 보여주고, 비즈니스가 어떤 속성 없이 살 수 있는지 물었다.

사내 설계 전문가들은 한 속성이 항상이 아니라 보통만 유지되면 된다고 판단했다. 그 단일 트레이드오프가 좁혀지자 모델 검사기는 이제 여러 설계가 작동할 것임을 확인했고, 팀은 그중 하나를 구축했다. 자동화된 구성 서비스는 이후 수년간 문제없이 운영되었으며, 이를 구축한 엔지니어들의 재임 기간보다 오래 지속되었다.

모델 검사기는 세 가지 규칙을 모두 충족하는 설계가 없음을 증명했다; 협상

명세 언어로 모델링하는 것은 버리기 쉽다. 거의 다 구축된 코드베이스는 그렇지 않으므로, 구현 전에 모든 설계 아이디어를 테스트하면 엔지니어링 시간 낭비를 피할 수 있었다.

모델 검사기는 구체적인 실패 추적을 반환하는데, 이는 추상적인 위험 경고보다 비엔지니어 이해관계자를 설득하는 데 더 효과적이다.

코드를 작성하기 전에 '이 설계 중 어느 것도 세 가지 요구사항을 모두 충족하지 않는다'는 사실을 드러내는 것은 암묵적이고 검토되지 않은 가정을 프로젝트 관리자가 실제로 내릴 수 있는 명시적 결정으로 바꾸었다.

시도하는 모든 설계가 실패하는 것처럼 보일 때, 먼저 그 공간을 형식적으로 모델링하라. 모델 검사기는 막연한 위험 감각을 코드를 작성하기 전에 제기할 수 있는 구체적이고 협상 가능한 트레이드오프로 바꿔준다.

자동화된 구성 관리 서비스는 수년간 효율적으로 운영되었으며, 이를 구축한 엔지니어들의 재임 기간을 훨씬 넘어섰다. Wayne은 이후 형식 명세 컨설턴트로 전임 일을 하며 이 실무에 대해 글을 썼고, 주제에 관한 책과 Alloy 명세 언어의 문서 작업을 포함했다.