자바 패스파인더를 이용한 소프트웨어 모델 검사 |
 |
이번에는 개발자에게 더 구체적이고 실직적인 도움을 줄 수 있는 유용한 테스트 도구를 하나 소개하고자 한다. 바로 미국 NASA(National Aeronautics and Space Administration)에서 공개한 자바 패스파인더(Java Pathfinder)[1]란 도구다. 이 도구는 화이트박스 테스팅을 위한 도구이며, 모델 검사(model checking) 기법을 이용한다.
테스팅의 분류
기본적인 이야기지만 간단히 테스팅의 분류에 대해 살펴보자. 먼저 테스팅은 크게 두 가지로 나눌 수 있다. 하나는 프로그램 내부 정보를 참조하면서 테스트하는 화이트박스 테스트와 다른 하나는 프로그램 내부 원시 코드를 참조하지 않는 블랙박스 테스트다.
화이트박스 테스트 접근 방법은 일반적으로 프로그램 구조나 논리 흐름을 근간으로 테스트 케이스를 작성한다. 블랙박스 테스트는 프로그램 구조를 고려하지 않고 프로그램에 예상되는 기대값을 산출할 입력값을 넣어 실제 결과와 비교하는 방식으로 테스트를 한다. 프로그램 내의 알고리즘이나 논리 흐름에 신경쓰기보다는 프로그램이 제공하는 기능을 중심으로 테스트하는 방법이다.
테스트는 테스트 단계(level)에 따라 단위 테스트, 통합 테스트, 시스템 테스트로 나누기도 한다.
단위 테스트란 프로그램을 구성하는 작은 단위(가령 클래스, 컴포넌트, 모듈 등)로 구분하여 그 단위 내에서 하는 테스트를 말한다. 보통은 프로그래머가 수행하는 경우가 일반적이며, 코드 커버리지 등으로 테스트 기준을 삼을 수 있다.
통합 테스트는 테스트된 단위(클래스, 컴포넌트, 모듈) 간에 인터페이스 시험을 중심으로 진행한다. UML을 이용한 시퀀스 다이어그램(sequence diagram) 등을 이용하여 단위 간에 인터페이스를 정의해 테스트를 하는 기준으로 삼을 수 있다. 보통 프로그램의 규모가 큰 경우 동적 테스트를 이용한 블랙박스 테스트를 수행하지만, 화이트박스 테스팅 도구(코드 분석 도구)를 이용해 테스트할 수 있다.
이렇게 테스트된 프로그램을 실제 운영 시스템에서 테스트하는 것을 시스템 테스트라 하며, 처음 시스템 요구 분석 리스트를 기준으로 하여 요구된 기능이 모두 구현되었는지, 또 구현된 기능이 정상으로 동작하는지 여부를 확인하는 테스트다. 통상 블랙박스 테스트를 통해 진행된다.
테스트는 프로그램의 실행 여부를 기준으로 동적 테스트와 정적 테스트로 구분하기도 한다. 동적 테스트는 프로그램을 실행하여 결과를 확인하는 방법으로 진행되며, 통상 대부분의 일반적 테스팅의 형태다. 정적 테스트는 프로그램 코드를 수행하지 않고 코드를 검사하는 분석적 방법을 말한다. 이런 특성상 일반적으로 화이트박스 테스팅으로 수행되며, 코드를 분석하는 분석 도구의 도움을 받아 진행한다. 또한 리뷰나 인스펙션을 통해 테스트를 진행하기도 한다.
모델 검사와 테스팅의 차이
모델 검사는 소프트웨어 공학의 한 분야인 정형화 기법(formal method)에 속하는 방법으로, 프로그램 구조가 주어진 논리적 공식 모델에 적합한지 여부를 확인하는 방법이다. 1981년 E.A. Emersion과 E.M. Clarke, 1982년에는 J. P. Queille와 J. Sifakis가 시제 논리(temporal logical)에 의해 처음 모델 검사라는 것을 수행했으며, 일반적으로 하드웨어 디자인 검증 부분에 사용되어 왔다.
소프트웨어에서는 소프트웨어의 결정 불가능성(undecidability)에 의해 쉽게 알고리즘화되지 못하고 있으며, 그러한 이유로 검증 대상의 소프트웨어는 유한상태머신(FSM)[2]이어야 하는 제약이 있다.
일반적으로 상태를 그래프로 표현하며, 최소 명제의 집합은 각 노드의 연결로 표현된다. 노드는 시스템의 상태, 엣지는 가능한 상태 전이를 나타낸다. 이러한 모델을 기반으로 소프트웨어를 검증하는 것을 모델 검사라 하며, 모델 검사를 위한 도구는 SPIN, KRONOS, CHESS, APMC, BLAST 등 다양하게 존재한다.[3] 자바 패스파인더도 그런 도구 중 하나다.
자바 패스파인더란 무엇인가
자바 패스파인더는 실행 가능한 자바 바이트코드 프로그램을 검사(verify)하는 도구로 JVM과 같은 형태로 운영된다. 명시적 상태 모델을 검사하는 모델 검사 도구이며, 미국 NASA에서 개발되어 2005년 4월 오픈 소스 소프트웨어로 공개되었다[4].
자바 패스파인더는 일반적인 디버거와 다르게 소프트웨어를 한번 실행하여 소프트웨어 상태를 확인하는 것이 아니라, 실행 가능한 모든 경로를 조사하여 발생 가능한 속성 위배(property violations) 사항(가령 deadlock이나 unhandled exception)을 확인하여 문제점을 보고한다. 또한 오류가 발생하기까지의 과정을 추적할 수 있다. 자바 패스파인더로 발견되는 문제점은 다음과 같은 것들이 있다.
- 병행성(concurrency) 관련 문제: deadlock, (race), missed signal 등
- 자바 런타임 관련 문제: unhandled exception, heap usage, (cycle budget)
- 기타: complex application specific assertion
자바 패스파인더의 한 가지 특징은 검사 대상 소프트웨어의 크기 제약이 있다는 것이다. 보통 10KLOC(1만 줄의 코드) 내의 소프트웨어를 검사할 수 있으며, 이러한 크기에 제약이 존재하는 이유는 앞서 언급한 소프트웨어의 진행 가능한 모든 경로를 모두 수행하며, 수행 시 상태를 보존하기 때문에 상태 저장 공간 한계로 인해 이러한 제약이 발생한다. 그러면 조금 구체적인 사례를 가지고 자바 패스파인더로 찾을 수 있는 버그를 살펴보겠다.
자바 패스파인더로 찾을 수 있는 버그
다음 코드는 Random 클래스를 이용하여 a와 b 두 개의 변수에 임의의 값을 할당하고 그 두 개의 값을 이용하여 변수 c에 값을 배정하는 간단한 프로그램이다.
<![CDATA[
import java.util.Random;
public class Rand {
public static void main (string[] args){
Random random = new Random(42); // (1)
int a = random.nextInt(2); // (2)
System.out.println(“a=” + a);
// 중간 생략
int b = random.nextInt(3); // (3)
System.out.println(“b=” + b);
int c = a/(b+a -2); // (4)
System.out.println(“c=” + c);
}
}
]]>
|
이제 독자들이 예제 코드가 정상적으로 동작하는지 테스트를 한다고 가정해 보자. 이 예제 프로그램을 수행하면 다음과 같은 결과를 얻을 수도(?) 있다.
예제 코드의 동적 테스팅을 통해 다음과 같은 결과를 얻었다면 이 예제 코드가 정상으로 동작한다고 확신할 수 있을까?
정답은 ‘아니다’. 이상의 결과를 통해 이 예제 코드가 100% 모든 상황에서 정상으로 동작한다고 할 수 없다. Random을 이용해 a에는 0~1까지, b에는 0~2까지가 할당될 수 있으므로 실행할 때마다 다양한 결과가 발생할 수 있으며 그 중 한 가지 경우로 다음과 같은 결과가 나올 수 있다. 예를 들면 다음과 같은 상황도 발생할 수 있는 것이다.
<![CDATA[
a = 1
b = 1
c = 에러 (1/0 -> divided by zero!!!)
]]>
|
발생할 수 있는 모든 상황은 다음과 같다.
자바 패스파인더는 이러한 발생 가능한 모든 상황에 대해 실행 상태를 저장하며 진행 가능한 모든 경로를 반복 수행한다. 자바 패스파인더를 수행한 결과는 다음과 같다.
변수 a가 0인 상황에서 가능한 경로인 b가 0, 1, 2인 모든 상황을 실행하여 발생할 수 있는 문제 상황을 찾아 준다. 이러한 실행 상태를 저장하며 BackTracking을 통한 반복 실행을 하는 이유로 앞서 언급한 대로 ‘검사 대상 소프트웨어에 보통 10KLOC의 크기 제약’이 존재한다.
물론 자바 패스파인더 없이도 모든 경로를 수행할 수 있도록 TestDriver를 이용해 각 변수에 값을 배정하거나, 코드 수정을 통해 가능한 모든 경우를 확인할 수 있지만 자바 패스파인더는 그러한 불편 없이 모든 경우를 확인할 수 있는 점이 장점이다. 이와 비슷한 한 가지 예를 더 살펴 보자.
<![CDATA[
Public class Racer implement Runnable {
int d = 42;
public void run() {
doSomething(1000);
d = 0;
}
public static void main(String[] args){
Racer racer = new Racer();
Thread t = new Thread(racer);
t.start();
doSomething(1000);
int c = 420/racer.d;
}
static void doSomething(int n) {
// 그냥 무엇인가를 하며 시간을 소비한다.
// 코드 생략…
Try { Thread.sleep(n);}catch(InteruptedException e) {}
}
}
]]>
|
위 코드는 Thread에 의해 병렬로 동작하는 프로그램이다. 변수 d에 배정된 값이 42지만, Thread에 의해 어느 순간 0으로 바뀌기 때문에 테스트를 위해 코드를 실행할 때 어느 경우는 정상으로 동작하여 변수 c에 10이 배정되기도 하고, 어느 경우에는 변수 d에 0이 배정되어 ‘divided by zero’ 에러가 발생하기도 한다. 자바 패스파인더로 테스트하면 다음과 같은 결과를 얻을 수 있다.
이렇듯 자바 패스파인더는 자바 프로그램에서 프로그램 실행 시 변수값이 명시적인 한 가지 값으로 고정되지 않고 유동적으로 변하는 경우 발생할 수 있는 오류를 찾는 데 매우 효과적인 도구라 하겠다.
후기
자바 패스파인더는 이클립스 플러그인 형태로 설치하여 사용할 수 있다. 자세한 설치, 설정, 운영 방법은 www.wisestone.kr 사이트의 리서치 게시판에 올려 놓은 ‘Java Pathfinder 사용법.pdf’ 파일을 참조하기 바란다.[5]
화이트박스 테스팅, 특히 유닛 테스팅, 통합 테스팅 단계에서 화이트박스 테스팅은 그 특성상 개발자가 수행하고 코드 품질에 대해 책임져야 하는 경우가 많다. 이번에 소개한 자바 패스파인더는 무료 소프트웨어임에도 프로그램 속에 숨어있는 찾기 어려운 버그를 발견하는 데 효과적인 도구로, 코드의 품질을 높이는 데 개발자가 이클립스, 넷빈즈 등의 개발 환경에서 유용하게 사용할 수 있는 화이트박스 테스팅 도구라 하겠다.
주
[1] http://ti.arc.nasa.gov/projects/jpf/
[2] http://en.wikipedia.org/wiki/Model_checking
[3] http://en.wikipedia.org/wiki/Finite_state_machine
[4] http://javapathfinder.sourceforge.net/
[5] 와이즈스톤 리서치 게시판: http://www.wisestone.kr/gnuboard/bbs/board.php?bo_table=contents
이 문서 북마킹 하기
 [지난 developerWorks Column 보기]
|
이영석 
이정환 
