Java Pathfinder 설치 및 실행법

Java Pathfinder 는 NASA Ames 연구소에서 개발한 Java 언어용 모델 검증 도구입니다. Java bytecode를 대상으로 검증합니다. 테스팅이 아닌 모델 검증 도구이므로, 한 번의 실행에 하나의 경로만을 검사하지 않고 모든 가능한 실행 경로를 탐색하여 모델이 검증 속성을 위배하는지 아닌지 검사해줍니다. 그래서 Race Condition처럼 테스팅만으로 알아내기 힘든 부분을 손쉽게 검증할 수 있습니다. 

일반적으로 모델 검증은 모델링 언어로 정형 모델을 작성할 것을 요구하는 경우가 많은데 Java 코드를 그대로 사용하는 도구라는 점에서 진입 장벽이 상대적으로 낮다고도 볼 수 있겠습니다. 

다만 Java Pathfinder의 경우, 다른 검증 도구인 CBMC나 Spin, BLAST 등에 비해 설치가 상당히 까다롭습니다. 설치를 위해 준비할 것이 많은데, 여기서는 Eclipse 를 기준으로 설치하는 방법을 설명합니다. NASA 측에서는 NetBeans 설치를 권장하는 것 같지만요.

먼저 준비해야 하는 것은

1. Java/Javac의 버전 확인

Java와 javac 둘 다 cmd로 확인해서 잘 실행되는지 알아봅니다. 최신 버전일 수록 좋습니다. 특히 람다식을 지원할 수 있도록 JRE 8 이상이 설치되어 있는지 확인합니다. 둘 다 1.8 이상이라면 설치하기 알맞은 환경입니다.

2. Mercurial 설치

설치하는 방법은 무궁무진한데 시도와 삽질을 반복한 결과 Mercurial로 받는 게 가장 쉽습니다. SVN 같은 곳에서 받는 것보다 좀 더 빨리 리뉴얼되는 것 같기도... 머큐리얼 설치 후 커맨드창에 hg 를 쳐서 실행이 잘 되는지 확인해봅니다.

3. Mercurial Eclipse plugin 설치

marketplace 등에서 이클립스 플러그인을 받습니다. 다 받고 나면 Window>Preferences>Team>Mercurial에서 hg.exe 파일의 경로를 설정해줍니다. 

4. Ant Builder 설치

받아온 소스를 빌드하려면 이클립스 Ant Builder가 추가로 필요하므로 이것 역시 받아줍니다. http://download.eclipse.org/releases/<version_name>으로 받으실 수 있습니다. Install new software 에서 다운로드합니다.

설치하기

커맨드라인 환경에서 실행시키는 방법도 있지만 대부분의 사람들이 Java 프로그램을 개발할 때 Eclipse를 사용하므로 여기서는 이클립스 환경에서 JPF를 실행시키는 것만 다루겠습니다.

1. 먼저 jpf-core를 import 해줍니다.

Mercurial을 사용해 jpf-core를 import합니다. Import>Mercurial>Clone Existing Mercurial Repository를 선택해서 git clone 하듯이 소스를 복사해옵니다. 주소는 http://babelfish.arc.nasa.gov/hg/jpf/jpf-core  입니다.

2.site.properties 파일 생성

아마 기본 설정을 유지하셨을 경우에 jpf-core는 projects나 workspace에 다운로드 되었을 것입니다. 여기에 추가로 site.properties 파일이 필요합니다.  

유저 홈 디렉토리(저는 Windows 사용자이므로 C:\Users\username이겠지요.) 에 .jpf 폴더를 만들어줍니다. Win7 유저의 경우 GUI 환경에서는 숨김폴더를 만들 수 없으므로 cmd에서 mkdir를 사용해서 만들어줍니다. 이후 메모장에서 site.properties 파일을 만들고 다음과 같이 입력해줍니다.

# JPF site configuration

user.home=C:/Users/sec

jpf.home = ${user.home}/workspace/

# can only expand system properties

jpf-core = ${user.home}/workspace/jpf-core

# annotation properties extension

jpf-aprop = ${jpf.home}/jpf-aprop

extensions+=,${jpf-aprop}

# numeric extension

jpf-numeric = ${jpf.home}/jpf-numeric

extensions+=,${jpf-numeric}

# concurrent extension

#jpf-concurrent = ${jpf.home}/jpf-concurrent

#extensions+=,${jpf-concurrent}

jpf-shell = ${jpf.home}/jpf-shell

extensions+=,${jpf-shell}

jpf-awt = ${jpf.home}/jpf-awt

extensions+=,${jpf-awt}

jpf-awt-shell = ${jpf.home}/jpf-awt-shell

extensions+=,${jpf-awt-shell}

jpf-core 최상위 폴더의 위치, workspace 경로에 따라 변수들의 값은 변경될 가능성이 있으니 개인 설정에 맞추어 작성해주시면 됩니다.

3. Eclipse Plugin 설치

JPF도 놀랍게도 Eclipse 플러그인을 제공해줍니다. Install new software로 다음 주소에서 플러그인을 받습니다.

http://babelfish.arc.nasa.gov/trac/jpf/raw-attachment/wiki/projects/eclipse-jpf/update

다운로드 하고 나서는 Window>Preferences의 JPF Preferences 항목으로 들어가 *jpf/site.properties가 올바른 경로에 설정되어 있는지 확인합니다. 2까지 하셨으면 대체로 맞겠지만 다른 경우에는 site.properties 위치를 수동으로 지정해줍니다.

4. jpf-core 빌드하기

JPF 사용에 앞서 빌드를 해줍니다. 빌드는 jpf-core 프로젝트의 build.xml 파일을 우클릭>Run As>Ant Build로 실행하는 방법으로 할 수 있습니다. javac가 1.8.0_20 이상이 아닐 경우 문제가 생길 수 있습니다.

5.검증할 프로젝트의 application properties 생성

검증할 프로젝트의 application.properties 파일이 필요합니다. 파일 이름은 아무것이나 상관 없습니다. 프로젝트 우클릭>New>File 로 .properties 파일을 생성해줍니다. 이 application properties 파일은 jpf-core의 jpf.properties 및 default.properties보다 우선적으로 실행되므로, 설정을 바꾸기 위해 두 파일을 건드리는 일은 없으시기 바랍니다.

+classpath=${config_path}/bin

target=<packagename>.ClassName

application properties 파일에는 다음과 같이 적어줍니다. 보시다시피 classpath가 bin으로 설정이 되어 있습니다. 즉 .class 파일이 생성되어야(바이트코드가 있으므로) 분석 가능한 것입니다. 컴파일 불가능한 코드는 JPF로 검증할 수 없습니다.

6.검증하기

application *.properties 파일을 우클릭하여 Verify 를 선택합니다. JPF가 실행되면서 해당 클래스의 모델 검증을 실시합니다. 결과는 다음과 같습니다.

위의 출력 결과는 application properties 파일에 listener=gov.nasa.jpf.listener.PreciseRaceDetector 를 추가하고 Race condition 이 발생하는 클래스를 작성하여 Verify한 결과입니다.