자바 패스파인더

Java Pathfinder
자바 패스파인더
개발자NASA
안정된 릴리스
6.0 / 2010년 11월 30일 (2010-11-30)
기입처자바
운영 체제크로스 플랫폼
크기1.6 MB (아카이브)
유형소프트웨어 검증 툴, 가상 머신
면허증.Apache 라이센스 버전 2
웹 사이트https://github.com/javapathfinder/

Java Pathfinder(JPF)는 실행 가능한 Java 바이트 코드 프로그램을 확인하는 시스템입니다.JPF는 NASA Ames Research Center에서 개발되어 2005년에 오픈 소스되었습니다.약어 JPF는 관련 없는 Java Plugin Framework 프로젝트와 혼동하지 마십시오.

JPF의 핵심은 Java Virtual Machine입니다.JPF는 일반 Java 바이트 코드 프로그램을 실행하고 프로그램 상태를 저장, 일치 및 복원할 수 있습니다.데이터 레이스나 데드록 등의 결함을 찾기 위해 동시 프로그램 모델체크를 주로 해 왔다.JPF는 각각의 확장에 의해 다음과 같은 다양한 목적으로도 사용할 수 있습니다.

  • 분산 응용 프로그램 모델 검사
  • 모델 체크, 사용자 인터페이스의
  • 기호 실행을 통한 테스트 사례 생성
  • 저수준 프로그램 검사
  • 프로그램 계측 및 런타임 모니터링

JPF에는 상태 공간 브랜치의 고정 개념이 없으며 데이터와 스케줄링 선택을 모두 처리할 수 있습니다.

예

다음 테스트 대상 시스템은 동일한 변수에 액세스하는 두 스레드 간의 단순한 레이스 조건을 포함합니다.d(1) 및 (2)에서 (1)이 (2)보다 먼저 실행될 경우 예외 없이 분할될 수 있다.

일반의 학급 레이서 용구 실행 가능 {      인트 d = 42;       일반의 무효 달려. () {           어떻게 좀 해봐.(1001);           d = 0;                              // (1)      }       일반의 정적인 무효 주된 (스트링[] args){           레이서 레이서 = 신규 레이서();           실 t = 신규 실(레이서);           t.개시하다();            어떻게 좀 해봐.(1000);           인트 c = 420 / 레이서.d;              // (2)           시스템..나가..인쇄(c);      }            정적인 무효 어떻게 좀 해봐. (인트 n) {           해라 { 실.수면.(n); } 또 만나 (중단됨예외. ix) {}      } }

추가 설정이 없으면 JPF는 분할을 0으로 검출하여 보고합니다.JPF가 레이스 조건의 부재를 검증하도록 설정되어 있는 경우(잠재적인 다운스트림 효과에 관계없이), 다음과 같은 출력이 생성되어 오류를 설명하고 오류를 초래하는 카운터 예를 제시합니다.

JavaPathfinder v6.0 - (C) RIACS/NASA Ames 리서치 센터 ====================================================== 테스트 대상 시스템 응용 프로그램: Racer.java ... ====================================================== 오류 #1 를 참조해 주세요.Precision Rrace 검출기 필드 레이서 @13d.d 레이스 Main at Racer.main (Racer.java:16) "int c = 420 / racer.d; " : getfield Racer.run의 스레드 0(Racer.java:7) "d = 0; " : 풋필드  ====================================================== 추적 #1 ----전환 #0 스레드: 0 ... ----전환 #3 스레드: 1 governor.jpf.jvm.choice 를 참조해 주세요.ThreadChoiceFromSet[id="sleep",isCascaded:false,{main,> 스레드-0} [3개의 insn(소스 없음)] Racer.java:22 : { 스레드}를 시도합니다.sleep(n); } catch(중지됨)예외 ix) {} Racer.java:23 : } Racer.java:7 : d = 0; ... ----전환 #5 스레드: 0 governor.jpf.jvm.choice 를 참조해 주세요.ThreadChoiceFromSet[id="sharedField",isCascaded:false,{>main,스레드 0}] Racer.java:16 : int c = 420 / racer.d;

확장성

JPF는 다양한 방법으로 확장할 수 있는 개방형 시스템입니다.주요 확장 구조는 다음과 같습니다.

  • 청취자 - 복잡한 속성(예: 시간 속성)을 구현합니다.
  • 피어 클래스 - 네이티브 메서드를 구현하는 데 주로 사용되는 호스트 JVM 수준에서 코드를 실행합니다.
  • 바이트 코드 팩토리 - 바이트 코드 명령의 대체 실행 의미론을 제공합니다(예: 심볼릭 실행을 구현합니다).
  • 선택 생성기 - 예약 선택 또는 데이터 값 집합과 같은 상태 공간 분기를 구현합니다.
  • 직렬화기 - 프로그램 상태 추상화를 구현합니다.
  • 게시자 - 다른 출력 형식을 생성합니다.
  • 검색 정책 - 다른 프로그램 상태 공간 통과 알고리즘을 사용합니다.

JPF에는 이러한 구조를 별도의 JPF 확장 프로젝트로 패키지화하는 런타임 모듈 시스템이 포함되어 있습니다.메인 JPF 서버에서는 심볼릭 실행 모드, 수치 분석, 완화된 메모리 모델의 레이스 조건 검출, 사용자 인터페이스 모델 체크 등 다수의 프로젝트를 이용할 수 있습니다.

제한 사항

  • JPF는 Java 네이티브 메서드를 분석할 수 없습니다.테스트 대상 시스템이 이러한 메서드를 호출하는 경우, 이러한 메서드는 피어 클래스 내에서 제공되거나 리스너에 의해 대행 수신되어야 합니다.
  • 모델 체커로서 JPF는 부분 순서 감소를 즉시 수행하지만 조합 폭발에 취약합니다.
  • JPF 모듈 및 런타임 옵션을 위한 구성 시스템은 복잡할 수 있습니다.

「 」를 참조해 주세요.

  • MoonWalker - Java PathFinder와 유사하지만 용.Java 프로그램 대신 NET 프로그램

외부 링크

레퍼런스

  • 빌럼 비서, 코리나 S퍼서리아누, 사르프라즈 쿠르시드Java PathFinder를 사용한 입력 세대 테스트.입력: George S.Avrunin, Gregg Rothermel (Ed.) : ACM/SIGSOFT 소프트웨어 테스트 및 분석에 관한 국제 심포지엄 2004 진행.ACM Press, 2004. ISBN1-58113-820-2.
  • Willem Visser, Klaus Havelund, Guillaume Brat, Park, Flavio Lerda, Model Checking Programs, Automated Software Engineering 10(2), 2003.
  • Klaus Havelund, Willem Visser, 새로운 트렌드로서의 프로그램 모델 체크, STT 4(1), 2002.
  • Klaus Havelund, Thomas Pressburger, Java PathFinder를 사용한 Java 프로그램 모델 체크, STTT 2(4), 2000.