Pink Spider/Java Pathfinder 사용법

아래에 Java Pathfinder (JPF) 사용하는 방법을 자세히 안내드립니다. Java Pathfinder는 자바 프로그램의 모델 체킹(model checking) 도구로, 프로그램의 상태 공간을 탐색하여 버그나 데드락 등을 찾는 데 활용됩니다.

아래 내용을 단계별로 설명드릴게요.

🧭 1. Java Pathfinder(JPF)란?

**Java Pathfinder (JPF)**는 자바 프로그램을 실행하며 상태공간을 체계적으로 탐색하는 툴입니다.

주요 기능

• 멀티스레딩 버그 탐지
• Assertion 위반 검출
• Deadlock 탐지
• Non-deterministic 동작 검증
• Symbolic execution (jpf-symbc) 지원

⚙️ 2. 설치

JPF는 GitHub 저장소에서 직접 빌드하는 것이 일반적입니다.

2.1 Git 설치

git clone https://github.com/javapathfinder/jpf-core.git

2.2 환경 변수 설정

예: ~/.bashrc 또는 ~/.zshrc에 추가

export JPF_HOME=$HOME/jpf-core
export PATH=$PATH:$JPF_HOME/bin

적용:

source ~/.bashrc

2.3 빌드

cd $JPF_HOME
ant

빌드가 성공하면 bin 디렉토리에 실행 스크립트들이 생성됩니다.

🛠️ 3. JPF 구성 및 실행

JPF는 **설정 파일 (.jpf)**로 분석 대상을 정의합니다.

아래에 샘플 예제를 보여드리겠습니다.

3.1 예제 Java 클래스

public class TestAssertion {
    public static void main(String[] args) {
        int x = 42;
        assert x == 43 : "x must be 43!";
    }
}

이 코드는 AssertionError가 발생할 수 있습니다.

3.2 JPF 설정 파일(test.jpf)

test.jpf를 프로젝트 루트에 작성:

target=TestAssertion
classpath=.

설명

• target: main 메서드를 가진 클래스 이름
• classpath: 클래스 경로(컴파일된 .class 파일이 위치한 곳)

▶️ 3.3 실행

다음 명령어로 실행:

jpf test.jpf

출력 예시:

====================================================== error  #1
gov.nasa.jpf.vm.NoUncaughtExceptionProperty
java.lang.AssertionError: x must be 43!

즉, AssertionError를 탐지합니다.

🧩 4. 동시성 버그 탐지 예제

멀티스레딩 문제 예제를 보겠습니다.

public class TestRace {
    static int shared = 0;

    public static void main(String[] args) {
        Thread t1 = new Thread(() -> {
            shared++;
        });

        Thread t2 = new Thread(() -> {
            shared--;
        });

        t1.start();
        t2.start();
    }
}

이 경우에도 race condition 가능성이 있습니다.

설정 파일 race.jpf:

target=TestRace
classpath=.

실행:

jpf race.jpf

이렇게 하면 다양한 스케줄링 시나리오를 시도하여 동시성 문제를 탐색합니다.

🧠 5. Symbolic Execution(jpf-symbc)

심볼릭 실행을 통해 프로그램 입력 공간을 검증할 수도 있습니다.

설치:

git clone https://github.com/javapathfinder/jpf-symbc.git
cd jpf-symbc
ant

jpf.properties에 extensions 설정 추가:

extensions=gov.nasa.jpf.symbc.SymbolicListener

이후, 심볼릭 분석을 위한 옵션을 .jpf 파일에 추가할 수 있습니다.

📂 6. 주요 옵션 정리

*.jpf 설정 파일에서 자주 쓰는 옵션:

💡 7. 참고 리소스

• JPF GitHub
• JPF 사용 가이드
• NASA JPF 홈페이지