코드 실행 대신 상태 모델
동기식부터 비동기식까지 시스템의 전이 관계를 기술할 수 있다. 모듈과 계층 구조로 구성 요소를 나누고 재사용하는 모델을 작성한다. 실제 구현을 모델로 옮길 때 어떤 상태를 포함하고 어떤 동작을 생략했는지가 결과의 의미를 결정한다. 모델 자체의 일관성도 검토해야 한다.
시간에 따른 성질
항상 유지해야 할 불변식이나 시간에 따라 성립해야 할 관계를 명세한다. 단순한 최종 출력 비교와 달리 가능한 상태 변화의 성질을 확인한다. 같은 문장처럼 보여도 경로와 시간에 대한 논리 표현이 다르면 요구가 달라질 수 있다. 작성한 명세가 실제 의도와 맞는지 작은 사례로 점검한다.
분석 방식과 경계
BDD를 사용하는 기호 분석과 SAT 기반의 경계 있는 모델 검사를 제공한다. 정한 깊이에서 문제가 없다는 결과를 모든 길이의 실행에 대한 보증으로 확장하지 않는다. 입력 모델은 유한한 자료형을 중심으로 구성되므로 추상화가 필요한 실제 시스템에서는 그 대응 관계를 확인한다. 모델과 명세 및 검사 옵션을 함께 보존해 결과를 재현한다.