검사의 출발점
자바 소스의 표면적인 모양보다 컴파일된 바이트코드를 분석 대상으로 삼는다. 프로그램에 대해 확인하려는 조건을 별도로 준비하고, 모델 검사 프레임워크에서 해당 동작을 다루는 방식이다. 일반 실행 환경에서 한 번 정상 종료하는 것과 검증 작업은 구분된다.
코어와 확장
JPF는 확장 가능한 기반으로 설계되어 있다. 기호 실행을 제공하는 Symbolic PathFinder처럼 특정 분석 목적을 위한 확장이 존재한다. 다만 코어와 확장은 별도 프로젝트이므로 같은 버전 조합에서 동작하는지 확인해야 한다.
개발 환경 확인
jpf-core는 자바 버전에 따른 브랜치 차이가 있다. 설치 안내에서 요구하는 OpenJDK와 빌드 환경을 맞추는 과정이 필요하다. 특정 확장이 오래된 자바 환경을 요구한다면 최신 코어를 무조건 결합하기보다 해당 확장의 호환 안내를 먼저 따른다.
관련 문서
Symbolic PathFinder / Coyote 동시성 검사 도구 / Lincheck / Jcstress