형식적 검증, 이제 CI 파이프라인에서 실행하세요!
형식적 검증에 대한 오해와 달리, 작은 모델과 차등 퍼징(Differential Fuzzing)을 결합하여 실용적인 테스트를 수행할 수 있음을 강조함.
검증된 모델을 오라클로 활용하여, 구현 코드의 논리적 오류를 효과적으로 찾아내는 방법을 제시하며, 특히 상태 머신, 금융 로직, 파서 등에 유용함을 설명함.
개발자들은 형식적 검증에 대한 전문 지식 없이도, 작은 모델을 시작으로 CI/CD 파이프라인에 통합하여 지속적인 코드 검증을 수행할 수 있다는 점에 주목함.
모델 기반 테스트의 핵심 원리
모델 기반 컨포먼스 테스팅은 검증된 모델과 구현 코드의 동작을 비교하는 차등 퍼징 기법을 활용한다. 구체적으로, 모델은 예상되는 동작을 정의하고, 퍼저는 무작위 입력을 생성하여 모델과 구현 코드에 적용한다. 따라서, 두 시스템 간의 불일치가 발견되면, 이는 코드의 버그로 간주된다. 결과적으로, 복잡한 로직 오류를 효과적으로 찾아낼 수 있다.
모델 선택과 퍼징 전략의 비교
전통적인 테스트 방식은 단위 테스트와 통합 테스트로 나뉘지만, 모델 기반 테스트는 이들의 단점을 보완한다. 반면, 검증된 모델은 명확한 규칙을 제공하여, 테스트 범위를 좁히고, 오류 발생 가능성을 줄인다. 따라서, 모델의 크기를 작게 유지하고, 전체 상태 비교를 통해, 더욱 정확한 버그 검출이 가능하다.
실제 적용을 위한 가이드
모델 기반 테스트를 시작하기 위해, 복잡한 형식적 검증 지식은 필수적이지 않다. 구체적으로, 작고 실행 가능한 모델을 선택하고, 핵심적인 불변성을 중심으로 모델링한다. 따라서, 차등 테스트 하네스를 구축하고, 퍼징을 시작하는 것이 좋다. 결과적으로, 모델에 증명(Proof)을 추가하여 모델의 신뢰도를 높일 수 있다.
