중요한 동작을 모델로
Promela는 프로세스의 동작을 표현하는 C와 비슷한 모델링 언어다. 실제 애플리케이션의 모든 코드를 그대로 넣기보다 확인할 상호작용과 상태를 추려 모델을 만든다. 어떤 동작을 생략했는지와 실제 구현이 모델을 따르는지 확인해야 한다. 동명의 웹 프레임워크나 인체 복원 모델과는 별개의 도구다.
탐색 방식의 선택
깊이 우선과 너비 우선 및 여러 코어를 사용하는 방식 등 다양한 탐색 구성을 제공한다. 실행 순서의 불필요한 중복을 줄이는 방식과 탐색 깊이를 제한하는 방식은 목적과 보증 범위가 다르다. 모델의 크기에 맞춰 기법을 고르되 선택한 검사에서 무엇을 빠뜨릴 수 있는지 이해한다.
범위와 결과의 기록
비트 상태 탐색처럼 저장 공간을 줄이는 방식과 상태를 완전하게 저장하는 방식의 결과를 같은 의미로 해석하지 않는다. 제한된 탐색에서 오류를 찾지 못한 사실은 모든 실행의 증명과 구분한다. 모델과 속성 및 탐색 옵션을 함께 보존하고 보고된 실행 경로가 실제 구현에서도 가능한지 조사한다. 모델 변화 후에는 같은 요구를 다시 검사한다.
관련 문서
NuSMV / TLAplus / Civl 검증기 / Loom 동시성 테스트