분산 프로토콜은 단위 테스트할 수 없지만, 모델 검증은 할 수 있다
분산 버그는 배포 후 수정 비용이 많이 든다. 모델 검증을 사용하면 구현 코드를 한 줄도 작성하지 않은 상태에서 그 버그를 찾을 수 있다. 다음은 TLA+를 이용한 방법이다.
분산 프로토콜은 단위 테스트할 수 없다. 단위 테스트는 한 대의 머신에서 한 개의 프로세스를 정해진 순서로 실행한다. 당신의 프로토콜은 다섯 대의 머신에서 열 개의 프로세스를 통제할 수 없는 순서로 실행한다. 이 두 현실 사이의 간극이 바로 버그가 서식하는 곳이다. 모델 검증은 그…