불완전 테스트 대 철저한 분석 대 사과와 오렌지 비교가 맞습니까?

Question

나는 종종 다음과 같은 주장을 듣는다. 전통적인 테스트의 단점은 합금 분석이 완전하고 (경계 내에서) 완전하지는 않지만 불완전하다는 것이다. 그러나 첫 번째는 소프트웨어에 관한 것이고, 두 번째는 모델에 관한 것입니다. 사과와 오렌지 비교가 아닌가요?

업데이트 : 잘못되었습니다. 비교 대상이 아닙니다 : testing code versus analyzing models. 그것은 사과와 오렌지의 비교입니다. 대신, 비교는 다음과 같습니다.

Testing models versus analysis of models. 

Testing code versus analysis of code. 

이는 사과와 사과의 비교입니다.

따라서 이슈가 모델이든 코드이든 관계없이 두 가지 종류의 분석을 비교할 수 있습니다. 테스트는 크기에 제한없이 상대적으로 적은 수의 사례를 무작위로 그리는 데 해당합니다. 작은 범위 내에서 모든 경우를 포함합니다.

오해를 해결 한 다니엘 잭슨에게 감사드립니다.

Answer 1

먼저 Alloy가 개발되었을 때, 증명을 기반으로하지 않은 Z 및 VDM과 같은 데이터가 많은 언어의 모델을 분석하기위한 기존 도구는 모델 테스트에 사용 된 유일한 시나리오였습니다. 각 시나리오는 사용자가 구성 했으므로 시나리오를 작성하는 비용과 적은 수의 낮은 적용 범위로 인해 접근 방식이 어려웠습니다.

둘째, Alloy는 코드에서 버그를 찾는 데 사용되었습니다. Mandana Vaziri, Mana Taghdiri, Greg Dennis, Juan Pablo Galeotti 및 기타의 PhD 논문을 참조하십시오. 이 모든 것들에서 기존의 테스트를 피하는 버그가 발견되었습니다.

세 번째로 한정된 철저한 테스트가 실행 가능하다는 사실에 주목할 가치가 있습니다. Sarfraz Khurshid는 초기에 Alloy를 기반으로하는 TestEra라는 도구에서 테스트 케이스를 생성하는 데 대한 자신의 논문의 개척자였으며 나중에 (덜 고 Marinov 등과 함께) Korat라는 도구를 사용하여 더 적은 선언적 방법으로보다 명확한 해결 방법을 교환했습니다 제약 조건.