소프트웨어 테스팅 vs. 정형 검증

높은 수준의 소프트웨어 신뢰성이 요구되는 OS(Operating System) 개발, 항공, 자동차, 국방 등의 분야에서 최근 정형 검증(formal verification)이라는 기법이 도입되고 있다.

 소프트웨어 테스팅은 모든 시험 조건(test case)를 확인하기가 현실적으로 어렵기 때문에 수학적인 정형 검증 모델에 기반하여 소프트웨어의 취약성을 확인하는 정형 검증 기법이 이론적으로는 좀 더 신뢰성을 갖고 있는 방법론이다.

 단순한 예를 들어 자동차의 auto cruise 기능이 동작 시에 운전자가 핸들을 조작하면 자동차는 auto cruise 모드에서 수동 운전 모드로 반드시 진입해야 한다는 조건을 어떻게 만족할지 확인하고 싶을 때 auto cruise 모드를 빠져나오게 하는 입력 조건들이 아주 많을 경우(즉, 시험 조건이 많을 경우), 정형 검증 기법을 사용하면 수학적인 검증 모델을 적용하여 항상 auto cruise 모드가 운전자 조작에 의해 수동 운전 모드로 항상 전환된다는 것을 보장할 수 있다(아직 내가 실제로 사용해본 적이 없어서 구체적으로 설명하기는 어렵지만 개념적으로 좀 더 신뢰성을 확보할 수 있는 방법인 것 같다).

 MathWorks사는 2012년 출시된 MATLAB SW에서 Polyspace라는 정형 검증 툴을 지원하고 있으니 참고하기 바란다.