간단한 자바프로그램을 위한 CTL 모델 체킹

( CTL Model Checking for Simple Java Program )

이정림․이태훈․권기현

경기대학교 전자계산학과 소프트웨어공학전공

jrim@kyonggi.ac.kr   taehoon@kyonggi.ac.kr   khkwon@kyonggi.ac.kr

요  약

소프트웨어의 안전성과 신뢰성을 높이기 위해서는 소프트웨어에 대한 철저한 검증이 요구된다. 더군다나 임베디드 소프트웨어에서는 검증이 더욱 요구된다. 왜냐하면 임베디드 소프트웨어는 복잡한 기능을 만족해야 하며, 시간 제약 및 운용 제약과 같은 성능 조건을 만족할 뿐만 아니라 크기와 속도 면에서 최적화되어야 하기 때문이다.

본 논문에서는 간단한 자바 언어로 작성된 임베디드 소프트웨어의 기능을 검증하는 모델 체커를 구현하였다. 모델 체커는 크게 추상화 모듈과 검증 모듈로 구성된다. 추상화 모듈은 상태 폭발을 방지하기 위해서 자바 프로그램을 이진 프로그램으로 변환한다. 검증 모듈은 이진 프로그램의 제어 흐름을 분석해서 CTL(Computation Tree Logic) 모델 체킹을 수행한다.

본 연구는 과학기술부 기초과학 연구

(R01-2005-000-11120-0) 지원으로 수행되었음.

SLAM, BLAST와 같은 기존 소프트웨어 모델 체커가 API(Application Programming Interface) 이용 규칙에 대한 안전성 속성만을 검사하는데 비해서, 본 논문에서 구현된 모델 체커는 안전성 속성과 궁극성 속성 모두를 검사하는데 초점을 맞추고 있다. 또한 추상화 작업 동안에 정리 증명기 호출 횟수를 감소시킴으로서 모델 체커의 성능을 개선하였다.

1. 서  론

프로그래밍언어논문지 제 권 제 호 (    . )

1.1 연구 배경

임베디드 시스템 개발에 있어서 성공여부는 하드웨어 보다 소프트웨어 쪽으로 비중이 옮겨지고 있다. 왜냐하면 임베디드 소프트웨어의 개발은 제한된 자원과 여러 가지 환경변수를 고려해야 하는 어려움이 있고, 에러 발생시에 디버깅이 범용 프로그램보다 훨씬 어렵다. 또한 임베디드 소프트웨어는 대량 생산되기 때문에 소프트웨어 결함은 그 만큼 치명적이다. 즉 결함을 수리하는데 많은 비용이 소요될 뿐만 아니라 일부 펌웨어에서는 결함 수리가 불가능한 경우도 많다. 리콜되는 전자 제품을 분석한 결과 소프트웨어 불량이 결함의 주요 원인중의 하나로 밝혀졌다. 이처럼, 임베디드 소프트웨어의 안전성과 신뢰성을 높이는 일은 매우 중요하다. 따라서 소프트웨어 모델 체킹과 같은 임베디드 소프트웨어에 대한 철저한 검증기술이 필요하다.

모델 체킹이란 정형명세 언어를 사용하여 시스템을 유한상태모델로 표현하고 그 시스템이 만족해야하는 안전성 속성 등을 논리식으로 표현한다. 그리고 시스템이 이 속성을 만족하는 지를 자동으로 철저히 검증해준다[1]. 모델 체킹은 모델이 커짐에 따라 검사해야 할 상태공간의 크기가 지수적으로 증가하는 상태폭발문제[2] 때문에 작은 규모의 상태공간을 갖는 하드웨어나 프로토콜 검증에 주로 사용되어져 왔다. 그러나 최근에는 상태폭발문제를 다루기 위한 다양한 연구와 술어추상화와 같은 추상화 기술의 발전을 가져오고 있다. 따라서 다룰 수 있는 상태공간의 크기가 증가하고 정리증명기의 성능이 향상됨에 따라 모델 대신 무한한 상태공간을 갖는 소프트웨어 자체를 모델 체커의 입력으로 넣어 논리적 에러를 검증하려는 움직임이 활발하다.

소프트웨어는 무한한 상태공간을 갖는다. 예를 들어, 정수형 변수 하나만 하더라도 무수히 많은 상태( ..., -2, -1, 0, 1, 2, ....)를 가질 수 있고 이런 정수형 변수들의 조합은 더욱 무한한 상태공간을 발생시킨다. 따라서 소프트웨어를 모델 체킹하기 위해서는 상태공간을 줄이기 위한 추상화가 필수적이고 매우 중요하다. 본 논문에서 사용할 술어추상화 기법은 소프트웨어 모델 체킹 분야에서 프로그램을 자동으로 추상화시키는데 많이 활용되어지고 있다. 대표적인 연구로는 마이크로 소프트사의 C 모델체커인 SLAM[4], 버클리 대학의 C 모델체커인 BLAST[5], 카네기 멜론 대학의 C 모델체커인 MAGIC[6], 캔사스 대학의 자바 모델 컴파일러인 Bandera[7], NASA의 자바 모델 체커인 JavaPathFinder2[8] 등이 있다. 특히 SLAM은 테스팅에 기반한 전통적 방법으로 찾지 못했던 윈도우의 디바이스 드라이버 에러를 검증한 가장 실용적인 도구로 평가된다. 하지만 SLAM은 C언어를 대상으로 API규칙에 대한 안전성 검사만 한다. 따라서 자바와 같은 객체지향 언어를 대상으로 안전성 속성 뿐만 아니라 궁극성 속성도 검증하는 모델 체커가 필요하다.

그림 1. JAMES(Java Application Model checker for Embedded System)

1.2 연구 목표 및 범위

지금까지 소프트웨어 모델 체커 연구 중에 자바프로그램에 대해 안전성 속성과 궁극성 속성 모두를 검증하는 소프트웨어 모델 체커는 없었다. 따라서 본 연구에서는 자바프로그램 자체의 범용 속성을 검증하기 위해 CTL식(Computation Tree Logic, [9])을 이용한 자바 모델 체커인 JAMES(Java Application Model checker for Embedded System)를 개발하였다. 이 검증 도구는 현재, 추상화 모듈인 JAMES.abs와 검증 모듈인 JAMES.mc로 구성되어 있다.

본 논문에서는 JAMES.abs에 간단한 자바프로그램 [eqn: J] 와 술어의 집합 [eqn: RHO] 를 입력하여 각각의 자바 구문이 술어추상화를 이용하여 어떻게 이진프로그램 [eqn: OMEGA (J, P)]으로 자동 변환되는 지를 보인다. 또한 변환된 [eqn: OMEGA (J, P)]를 JAMES.mc로 받아들여 제어흐름 그래프로 변환해서 어떻게 CTL 속성을 검증하는지 보인다. JAMES.abs는 객체, 참조변수, 참조메소드를 포함하여 JDK1.2버젼의 기본적인 자바 구문을 다룬다. 하지만 아직 멀티 쓰레드나 외부 라이브러리에 관해서는 다루지 않는다. 자바 프로그램의 추상화는 클래스 단위로 이루어지며 Inner클래스를 포함할 수 있다. 검증 과정은 그림1과 같이 일반적으로 사용되는 추상화 - 모델 체킹으로 이루어진다. JAMES.mc는 모델 체킹을 수행한 후 속성을 만족하면 [eqn: true], 만족하지 않으면 반례를 생성하고 반례가 실제 코드에서 도달가능 한 경로이면 [eqn: false], 그렇지 않으면 가짜 반례로 판단한다. 추상화된 [eqn: OMEGA (J, P)]은 [eqn: J]보다 행위가 더 많은 상위 근사화(Over approximation) 된 모델이기 때문에 [eqn: J]에서는 도달 가능하지 못한 경로를 가질 수 있다. 이런 경우 그 경로를 없앨 수 있는 술어를 추가한 후 추상화 단계부터 다시 프로세스를 반복 수행해야한다. 하지만 본 논문에서 추상화 개

선은 다루지 않는다.

적용 사례로써 교육용 임베디드 시스템인 레고 로봇에 탑재되는 자바프로그램을 검증하였다. 또한 JAMES의 성능 향상을 위해 JAMES.abs에

서 사용하는 정리증명기의 호출 횟수를 줄이는

방법을 제시하고 실험 결과 좀 더 빠른 추상화

수행이 이루어진 것을 보인다.

1.3 논문의 구성

본 논문의 구성은 다음과 같다. 2장에서는 자바프로그램을 추상화하기 위한 술어추상화 기법에 대해서 정의하고 3장에서는 추상화된 자바프로그램을 검증하기 위한 CTL 모델체킹 알고리즘을 설명한다. 4장에서는 임베디드 소프트웨어 적용 사례에 대해 살펴보고 5장에서는 JAMES의 성능을 향상시키기 위한 최적화 방법을 살펴본다. 마지막으로 6장에서 결론 및 향후 연구에 대해 기술한다.

2. 자바 프로그램의 술어 추상화

대부분의 소프트웨어 모델 체커 연구에서 추상화는 매우 중요한 문제이다. 현재 프로그램의 추상화를 위해 널리 사용되고 있는 것이 술어추상화이다. 이 술어추상화는 Graf와 Saidi에 의해서 처음 제안되었다[10]. 이 기법은 술어 [eqn: p_{ i} IN P]를 기준으로 매우 큰 데이터 범위를 갖는 변수를 관심 있는 부분만 술어 [eqn: p_{ i}]에 대응하는 이진 변수 [eqn: v _{i} IN `V]로 나타낼 수 있다. 예를 들어, 자바의 integer형 변수 x는 4byte내의 매우 큰 상태 공간을 갖는다. 하지만 x의 값이 음수인지, 양수인지, 0인지만을 알고 싶다면  [eqn: P= LEFT { `x<0,``x>0,``x=0` RIGHT }]와 같이, 3개의 술어만 사용해서 겨우 6개의 상태공간으로 표현이 가능하다. 이 장에서는 우리가 개발한 JAMES.abs의 주요 알고리즘에 대해서 설명한다.

JAMES.abs는 자바프로그램 [eqn: J]와 술어의 집합 [eqn: P= LEFT { p _{1} ,...`...,`p _{n} RIGHT }]를 입력받아서 추상화된 이진프로그램 [eqn: OMEGA (J, P)]를 생성한다. [eqn: P]는 [eqn: J]를 [eqn: OMEGA (J, P)]으로 변환하는데 있어 판단 기준이 된다. [eqn: OMEGA (J, P)]는 변수의 타입이 이진(boolean)형식만 사용이 가능한 프로그램이다. [eqn: OMEGA (J, P)]은 n개의 이진 변수를 갖는다고 하자. 이진 변수는 [eqn: V`=` LEFT { v _{1} ,`...,v _{n} RIGHT }]으로 구성되고 모든 [eqn: v _{i} (0`<`i` LEQ `n)]에 대해서 [eqn: v` _{i``} IN LEFT { true,false,* RIGHT }]이다. 여기서 * 은 참과 거짓인지 알 수 없는 경우이다. 따라서 우리는 [eqn: v _{i}]의 값을 알기위해 select[eqn: ( SQCAP ( KAPPA (W`P`(s,`p _{i} `))),` SQCAP ( KAPPA (W`P(`s,` LNOT p _{i} `)`)))] 함수를 정의한다. 이 장의 제 1 절에서 다룰 이 함수는 기존의 C언어를 대상으로 하는 모델 체커에서 사용되던 함수의 확장함수로써 자바프로그램의 구문 [eqn: s]와 술어 [eqn: p_{ i} IN P]를 입력 받아서 그에 대응하는 이진 변수 [eqn: v _{i}]의 값을 되돌려 주는 JAMES.abs의 출력 함수이다. 여기서 [eqn: W`P(`s,`p _{i} `)]는 Weakest Precondition[4]이다. 이렇게 JAMES.abs에 의해 만들어진 이진 프로그램 [eqn: OMEGA (J, P)]은 속성 검증을 위해 JAMES.mc에서 제어흐름 그래프로 변환된다. 제 4 장에서 설명할 제어흐름 그래프는 원래의 자바 프로그램 [eqn: J] 의 상위 근사화된 모델이기 때문에 [eqn: J] 가 갖는 모든 제어 행위를 포함한다. 따라서 [eqn: J]의 모든 제어 행위는 제어흐름 그래프에서 시뮬레이트 할 수 있다. 또한 JAMES.abs에서 정리증명기는 각각의 자바 구문에서 술어들 간의 만족성관계를 평가하여 추상화 수행 시 결정프로시져로써 사용된다. 다음과 같이, 술어 [eqn: p _{1}], [eqn: p _{2}]의 만족성 관계를 살펴보자.

[eqn: p _{1} ` RARROW `p _{2}]

만약 위의 식이 참이면,

ㅇ “[eqn: p _{1}]은 [eqn: p _{2}]를 만족한다”

ㅇ “[eqn: p _{1}]은 [eqn: p _{2}]보다 강하다”

ㅇ “[eqn: p _{2}]는 [eqn: p _{1}]보다 약하다”

라고 말할 수 있다. 예를 들어, 참인 식 [eqn: x<2` RARROW `x<3]에 대해 [eqn: x<3]은 [eqn: x<2]를 포함하고“[eqn: x<3]이 [eqn: x<2]보다 약하다”라고 말한다.

2.1 할당문의 추상화

추상화 수행 시, 먼저 프로그램 내에 할당문 [eqn: x = e]와 이와 관련된 술어 [eqn: p]가 있을 때 Weakest Precondition을 계산한다. [eqn: W`P`(`x=e,`p _{} `)]는 [eqn: x = e]라는 할당문이 참이 되기 위한 가장 약한 선 조건을 말한다. 술어 [eqn: p]내에 [eqn: x]와 같은 변수가 존재한다면 [eqn: p]내의 변수 [eqn: x]를 [eqn: e]로 대체 한다([eqn: p[ e/x ]]). 예를 들어, 할당문 [eqn: x = x + 2]와 술어의 집합 [eqn: P= LEFT { `x<3,``x<`0,``x==-1` RIGHT }]을 가정하면,

[eqn: W`P`(`x`=`x`+`2,`x`<`3)`=`x`+`2`<`3`=`x`<`1]

이 된다. 이것은 [eqn: x = x + 2]구문 이후에 [eqn: x < 3]이 만족되기 위해서는 선 조건으로 [eqn: x < 1]이 참이 되어야 한다는 의미이다. 하지만 [eqn: x < 1]은 위의 술어의 집합 [eqn: P]에 없기 때문에 [eqn: x < 1]을 만족하는 술어들 중 가장 약한 술어를 [eqn: P]에서 찾는다. 이는 [eqn: x < 1]을 만족하면서 가장 가까운 술어를 찾는 것이다. 먼저 [eqn: P] 내에서 [eqn: W`P(s,`p)]를 만족하는 모든 술어와 술어들의 [eqn: conjunction(` WEDGE `)]에 대한 집합을 나타내는 함수를 [eqn: KAPPA (W`P(s,``p)`)= LEFT { p _{1} ,`p _{2} ,`p _{1} WEDGE p _{2} ,`...`... RIGHT }]라고 정의하자. 여기서 [eqn: v _{i} IN `V]에 대해 [eqn: p _{i} IN ` LEFT { v _{i} ,` LNOT v _{i} RIGHT }]이다. 또한 [eqn: P]에 대응하는 이진변수의 집합을 [eqn: V`= LEFT { b _{1} ,`b _{2} ,`b _{3} RIGHT }]라고 하자.

이때, [eqn: x < 1]를 만족하는 집합은

[eqn: KAPPA (`x`<`1`)`=` LEFT { eqalign{`x == -1,``x<0`,(`x == -1)# WEDGE (`x<0),`# LNOT (x == -1) WEDGE (x<0),`# (x == -1) WEDGE LNOT (x<0),`...`...} RIGHT }# `````````````````````````````````````= LEFT { eqalign{b _{3} ,`b _{2} ,`b _{3} WEDGE `b _{2} ,` LNOT b _{3} WEDGE b _{2} ,`# b _{3} WEDGE LNOT b _{2} ,...`...} RIGHT }]

이다. 그리고 이 집합 내의 술어들 중 가장 약한 즉, 다른 술어를 포함하는 술어를 찾아내는 함수를 [eqn: SQCAP (`)]라고 정의하자.

[eqn: SQCAP ( KAPPA (x<1))`=`x<0]

이다. 가장 약한 술어는 [eqn: KAPPA (x<1)]내의 다른 술어들을 모두 만족하는 [eqn: x<0]이 된다. 따라서 [eqn: x = x + 2]구문 이후에 [eqn: x < 3]이 만족되기 위해서는 선 조건으로 [eqn: x<0]이 참이 되어야 한다. 결국, m개의 할당문을 갖는 [eqn: OMEGA (J, P)]에서 할당문 [eqn: s _{k} IN S``(0<k LEQ m)]이후에 [eqn: p _{i}]가 만족되기 위해서는 선 조건으로 [eqn: SQCAP ( KAPPA (W`P(`s _{k} ,`p _{i} ))`]가 참이 되어야 한다. 또한 역으로,[eqn: SQCAP ( KAPPA (W`P(`s _{k} ,` LNOT p _{i} ))`]이 참이면 [eqn: p _{i}]는 할당문 [eqn: s _{k}]이후에 거짓이 된다. 이 두 가지 경우는 동시에 참일 수 없기 때문에 전자가 거짓일 때 후자는 참이 되는 술어 정보를 가져다 줄 수 있다. 더욱 효율적이고 정확한 추상화를 위해서는 이 두 가지 술어를 같이 평가해야한다. 하지만 둘 다 거짓이 되는 경우, [eqn: p _{i}]에 대응하는 이진변수 [eqn: v _{i}]에 비결정적인 값(*)을 할당할 수 있다. 왜냐하면 [eqn: P] 내의 정보가 술어를 평가하기 충분치 않거나 정리증명기인 Simplify[13]가 불완전해서 올바른 논리식을 증명하는데 실패하는 경우가 있기 때문이다. 따라서 이 두 가지 경우를 함께 평가하기 위해 select[eqn: ( SQCAP ( KAPPA (W`P`(s _{k} ,`p _{i} `))),` SQCAP ( KAPPA (W`P(`s _{k} ,` LNOT p _{i} `)`)))]함수를 다음과 같이 정의한다.

boolean select

[eqn: ( SQCAP ( KAPPA (W`P`(s _{k} ,`p _{i} `))),` SQCAP ( KAPPA (W`P(`s _{k} ,` LNOT p _{i} `)`)))]{

if([eqn: SQCAP ( KAPPA (W`P`(s _{k} ,`p _{i} `)))])

{ return [eqn: true]; }

else if ([eqn: SQCAP ( KAPPA (W`P`(s _{k} ,` LNOT p _{i} `)))])

{ return [eqn: false]; }

else

return *;

}

만약 select()함수의 첫 번째 인자가 참이면 술어 [eqn: p _{i}]에 대응하는 [eqn: v _{i}]는 [eqn: s _{k}]구문 이후에 [eqn: true]이고 두 번째 인자가 참이면 [eqn: s _{k}]구문 이후에 [eqn: v _{i}]는 [eqn: false]이다. 만일 두 인자 모두 [eqn: false]이면 [eqn: v _{i}]의 값은 알 수 없는 비결정적인 값(*)이 된다. 위의 예에서

select[eqn: ( SQCAP ( KAPPA (W`P`(x=x+2,`x<3`))),`]

[eqn: ` SQCAP ( KAPPA (W`P(x=x+2,` LNOT (x<3)`)`)))]

=  select[eqn: (`x<0,` LNOT (x<3))]

이다. 그러므로 [eqn: J] 내의 할당문 [eqn: x = x + 2];는 [eqn: OMEGA (J, P)]에서 [eqn: b _{1}]=select[eqn: (`b _{2} ,`` LNOT b _{1} )];형태로 추상

화되며 select()함수의 선언은 클래스단위로 [eqn: OMEGA (J, P)]내에 포함된다. [eqn: x = x + 2]구문의 변수 [eqn: x]가 들어있는 [eqn: P]내의 모든 다른 술어들도  동일한 방식으로 처리된다.

추상화는 주어진 술어의 집합 [eqn: P]를 기준으로 이루어진다. 따라서 [eqn: P]와 관련이 없는 할당문은 속성 검증에서 관심의 대상이 되지 않기 때문에 skip()한다.

우리는 자바프로그램에서 객체에 의해 참조되는 참조변수를 다룬다. 예를 들어 [eqn: W`P`(`a.x=e,`p _{} `)]의 경우 [eqn: a]는 객체명, [eqn: x]는 [eqn: a]객체가 가지고 있는 변수명이 된다. 이때 술어 [eqn: p]내에 [eqn: b.x]라는 참조변수가 있을 때, 객체 [eqn: a]와 [eqn: b]가 같은 주소 값을 가리킨다면 [eqn: b.x]는 [eqn: e]로 대체된다( [eqn: p[ e/b.x ]] ). 다시 정의하면,

[eqn: p[a.x,e,b.x]] = ( &[eqn: a.x] == &[eqn: b.x WEDGE p[e/b.x])` LOR]( &[eqn: a.x] != &[eqn: b.x WEDGE p`)]

이다. 위의 정의로부터,

[eqn: W`P(a.x`=c.y+1,b.x<`c.y)`]=

(&[eqn: a.x]==&[eqn: b.x WEDGE c.y+1<c.y)`]∨( &[eqn: a.x] != &[eqn: b.x WEDGE b.x`<`c.y`)]

이다. 자바 프로그램의 할당문을 추상화하는 assignmentEstimate(s, [eqn: P], [eqn: V])의 알고리즘은 다음과 같다.

1번 라인에서 할당문 내에 객체를 생성하는 명령어인 new는 미리 객체가 생성된 상황이라 가정하고 클래스 C와 객체 o를 object_table(o, C)에 저장한다.

10~17번 라인에서 객체 a가 참조하는 객체가 있을 경우 그 참조 객체내의 변수 x도 함께 평가한다. 이때 두 객체는 동일한 클래스의 인스턴스들로 가정한다.

Input : s = [ a = b ∨ a.x = e ∨ x = e ∨ C o = new C() ∨ T x = e ]

(a, b, o는 객체, C는 클래스, T는 데이터 타입),

[eqn: P= LEFT { p _{1} ,...`...,`p _{n} RIGHT }], [eqn: V`=` LEFT { v _{1} ,`...,v _{n} RIGHT }]

Output : 할당문 s를 추상화한 구문의 집합 Rs

Initialize : Rs = ∅

1:  if s == "C o = new C()" then

2:	클래스명 C와 객체명 o를 object_table(o, C)에 저장한다.

3:  else if s == "a = b" then

4:	객체명 a, b를 reference_table(a, b)에 저장, 갱신한다.

5:  else if s == "a.x = e" then

6:	for (int i= 1; i <= n ; i++)  do

7:	if [eqn: W`P`(s,`p _{i} `)] != [eqn: p _{i}] then

8:	[eqn: v _{i}] + "=" + select[eqn: ( SQCAP ( KAPPA (W`P`(s,`p _{i} `))),` SQCAP ( KAPPA (W`P(`s,` LNOT p _{i} `)`)))]+";\n";

를 Rs에 추가

9:	end

10:	while reference_table에 a를 참조하는 객체 ref가 있다 do

11:	s = "ref.x = e";

12:	for (int i= 1; i <= n ; i++) do

13:	if [eqn: W`P`(s,`p _{i} `)] != [eqn: p _{i}] then

14:	[eqn: v _{i}] + "=" + select( /*생략*/ )+";\n"; 를 Rs에 추가

15:	end

16:	a = ref;

17:	end

18:  else

19:	for (int i= 1; i <= n ; i++) do

20:	if [eqn: W`P`(s,`p _{i} `)] != [eqn: p _{i}] then

21:	[eqn: v _{i}] + "=" + select( /*생략*/ )+";\n"; 를 Rs에 추가

22:	end

23:  if( Rs == ∅ ) then

24:	return Rs;

25:  else

26:	return "skip()";

아래는 위 알고리즘을 적용한 간단한 예이다.

public static class A {

int value = 3;

}

public static void main( String[] args ) {

Predicate O: a.value = 5;

A a = new A();

A b = new A();

A c = new A();

a = b;

c = a;

c.value = 5;

…

}

public static class A {

skip();

}

public static void main( String[] args ) {

Predicate O: a.value = 5;

A a = new A();

A b = new A();

A c = new A();

skip();

skip();

O = true;

…

}

그림 2. 참조 변수의 추상화

위 예에서 [eqn: O]는 main()메소드 내의 지역술어 [eqn: a.value=5]에 대응하는 이진변수이다. 객체 [eqn: c]는 객체 [eqn: a]를 참조하기 때문에 [eqn: O[]&[eqn: c.value`=]&[eqn: a.value WEDGE 5=5]`=`true]가 된다. 그리고 객체 할당문 [eqn: a=b]와 [eqn: c=a]는 이진변수 [eqn: O]와 관련이 없기 때문에 skip()된다.

2.2 조건문의 추상화

이 절에서는 자바 프로그램의 조건문을 추상화하여 이진 프로그램 [eqn: OMEGA (J, P)]내에 표현되는 것을 보인다. 조건문으로써 if( [eqn: p] )문, while( [eqn: p] )문, for( [eqn: init] ; [eqn: p] ; [eqn: update] )문에 대해서 추상화를 수행한다.( switch()문은 if()문으로 쉽게 변환가능하기 때문에 고려하지 않는다. ) 간단한 if( [eqn: p] ){ ... } else{ ... }문의 경우를 고려해보자. then으로 분기되는 블록의 경우 최소한 조건식 [eqn: p]를 만족해야하고 else로 분기되는 블록은 최소한 [eqn: LNOT p]를 만족해야한다. 따라서 [eqn: OMEGA (J, P)]내에서는 각 블록의 시작점에 assume()문을 두어 각 블록 내에서 만족해야 할 술어들의 조합을 표현한다. then으로 분기되는 블록의 시작점에 assume( [eqn: LNOT K(` LNOT p)] )을 두어 [eqn: p]보다 약한 술어들의 조합을 표현하고 else로 분기되는 블록의 시작점에는 assume( [eqn: LNOT K(`p)] )을 두어 [eqn: LNOT p]보다 약한 술어들의 조합을 표현한다. 다음은 자바 프로그램의 특정 if문이 추상화되는 과정이다.

…

Predicate P1: path == 1;

Predicate P2: path == 2;

If( path == 1) {

…

} else if ( path == 2 ) {

…

} else {

…

}

…

Predicate P1: path == 1;

Predicate P2: path == 2;

If( * ) {

assume( P1∧¬P2 ...∧...);

…

} else if ( * ) {

assume( ¬P1∧P2 ...∧...);

…

} else {

assume( ¬P1∧¬P2 ...∧...);

…

}

그림 3. if()문의 추상화

위의 과정에서 *는 조건식 [eqn: p]가 참일 수도 있고 거짓일 수도 있음을 나타낸다. 따라서 제어의 흐름은 비결정적으로 어느 분기로든지 가능하다. 그리고 각 블록 내 구문들은 assume()문내의 조건을 만족해야 한다. 자바 프로그램의 while()문 역시 블록의 시작점에 assume()문을 놓고 동일하게 처리한다. 자바 프로그램의 for()문은 다음과 같이 while()문으로 변환 처리한다.

for( init ; p ; update) {

...

}

assignmentEstimate(init, P, V);

while ( * ) {

assume( ¬K( ¬p ) );

...

assignmentEstimate(update, P, V);

}

그림 4. for()문의 추상화

위에서 [eqn: init]은 변수에 초기값을 할당하는 구문이고 [eqn: update]는 조건문을 순환할 때마다 변수값을 갱신시키는 구문이라고 하자. 이때 [eqn: init]은 while()문이 시작되기 직전에 정의하고 [eqn: update]는 while()문 블록의 마지막 지점에 정의한다. 그런 다음 [eqn: init], [eqn: update]는 할당문 추상화를 수행하고 while()문에 대해서는 조건문 추상화를 수행하여 [eqn: OMEGA (J, P)]내에 표현된다. 그리고 나서 추상화된 [eqn: OMEGA (J, P)]이 모델체커인 JAMES.mc에 입력될 때 while()문은 다시 if...goto...문으로 변환해서 검증한다. if...goto...문의 변환 예는  3장에서 보인다.

2.3 메소드의 추상화

C프로그램에 함수가 있다면 자바 프로그램에는 메소드가 있다. 물론 인수의 전달이나 리턴 값을 얻는 방식은 함수와 비슷하나 메소드는 C프로그램의 서브루틴이나 함수와 달리 특정 객체를 대상으로 한다. 따라서 우리는 동일 클래스에서 정의되며 파라미터와 리턴 값을 갖는 [eqn: x`]=[eqn: M](a1, a2,...)형태의 메소드 호출 뿐만 아니라 [eqn: x`]=[eqn: obj.M](a1, a2,...)형태의 참조 메소드 호출도 다룬다. (여기서 [eqn: x`]는 임의의 변수, [eqn: obj]는 임의의 객체, [eqn: M]은 임의의 메소드를 말한다.) 이진 프로그램 [eqn: OMEGA (J, P)]는 자바 프로그램 [eqn: J] 와 술어의 집합 [eqn: RHO]를 입력받아서 생성된다. 이때 [eqn: OMEGA (J, P)]내에 메소드 호출을 추상화하기 위해 [eqn: J] 내의 변수들을 전역변수의 집합 [eqn: G _{J}]와 호출되는 메소드 [eqn: M]의 지역변수의 집합 [eqn: L _{M}]으로 구분한다. 또한 [eqn: RHO]는 전역술어의 집합 [eqn: P _{G}]와 [eqn: M]내의 지역술어의 집합 [eqn: P _{M}]으로 구분한다. 그리고 [eqn: P _{G}]와 [eqn: P _{M}]에 대응하는 이진변수의 집합 [eqn: V]는 각각 [eqn: V _{G}]와 [eqn: V _{M}]으로 구분한다. 왜냐하면 메소드가 호출되는 영역과 메소드가 정의되어있는 영역이 다르고 전역술어와는 다르게 지역술어의 활동영역이 자신의 블록 내에 한정되어 있기 때문에 메소드 호출의 추상화 수행 시 고려되어져야 한다.

자바 프로그램 [eqn: J]의 추상화는 메소드 호출의 추상화를 위해 크게 2단계로 구성한다. 1단계는 각 메소드 정보를 Method_Info()에 저장한다. 2단계는 [eqn: J]의 모든 구문과 함께 Method_Info()를 사용하여 메소드 호출을 추상화한다. Method_Info([eqn: Cname], [eqn: Mname], [eqn: M _{f}], [eqn: ret], [eqn: P _{f}], [eqn: P _{r}])에 저장되는 정보는 다음과 같이 6개의 튜플로 이루어진다.

ㅇ [eqn: Cname] - 메소드 [eqn: M]이 속한 클래스의 이름이다.

ㅇ [eqn: Mname] - 메소드 [eqn: M]의 이름이다.

ㅇ [eqn: M _{f}] - 메소드 [eqn: M]의 매개변수 집합이다.

ㅇ [eqn: ret] - 메소드 [eqn: M]의 리턴변수이다.

ㅇ [eqn: P _{f}] - [eqn: M`]의 매개변수에 대응되는 술어의 집합이다. 이 술어들은 다음과 같이 정의한다.

[eqn: LEFT { p IN P _{M} ``|`vars(p)` SMALLINTER L _{M} ``=`0 RIGHT }]

여기서 [eqn: `vars(p)]는 [eqn: `p]가 가지고 있는 변수의 집합을 의미한다.

ㅇ [eqn: P _{r}] - [eqn: M`]의 리턴변수에 대응되는 술어의 집합이다. 이 술어들은 다음과 같이 정의한다.

[eqn: LEFT { eqalign{p IN P _{f} ``|`(`ret` IN `vars(p)` WEDGE # ````````````````````````(vars(p)` RSLANT ` LEFT { ret RIGHT } SMALLINTER L _{M} ``=`0))# ````````````````````````` LOR `(`p IN P _{f} WEDGE (vars(p) SMALLINTER P _{G} `))} RIGHT }]

이제 [eqn: J] 내의 [eqn: S] 메소드 안에 있는 [eqn: x`]=[eqn: obj.M(a _{1} ,`a _{2} ,`...`,`a _{n} )]구문을 추상화해보자. 이 구문은 참조메소드를 호출하기 때문에 먼저 object_table([eqn: obj], [eqn: Cname])를 통해 객체 [eqn: obj]의 [eqn: Cname]을 찾는다. 다음으로 [eqn: Cname]과 [eqn: Mname]에 대응되는 Method_Info()를 추출한다. (이 Method_Info()정보는 이미 위의 추상화 1단계에 의해 저장되어져있다.) 그 다음 실제 [eqn: M]이 선언된 환경에서 각각의 매개변수들 [eqn: f _{i} ` IN M _{f} (0<i LEQ n)]에 대응되는 술어들 [eqn: p _{i} IN P _{f} (`0`<`i` LEQ `n)]로 변환한다. 이때 호출하는 환경 [eqn: S]에서의 매개변수들과 [eqn: M]이 선언된 환경에서의 매개변수들은 서로 대응된다. 따라서

[eqn: p` prime _{i} `=`p _{i} [a _{1} /f _{1} ,`a _{2} /f _{2} ,`...`,`a _{n} /f _{n} ]]

가 된다. 이 [eqn: p` prime _{i}]은 추상화된 [eqn: S`']에서 각 매개변수에 대응하는 술어가 된다. [eqn: p` _{i}]에 대한 [eqn: S]에서의 매개변수[eqn: a _{i}]의 실제 값은 다음과 같이 추상화한다.

[eqn: a _{i} `=`select`(K(p` prime _{i} ),`K( LNOT p` prime _{i} `))]

이때 [eqn: K()]함수에서 [eqn: p` prime _{i}]를 평가하기 위해 사용하는 이진변수의 범위는 [eqn: V`= LEFT { V _{G} ` CUP V _{S} RIGHT }]가 된다.

다음으로 [eqn: M`']에서 [eqn: P _{r} `=` LEFT { p _{1} ,`...`,`p _{d} RIGHT }]을 가정한다. 이때 [eqn: M`']이 선언된 환경에서 리턴변수 [eqn: ret]에  대응되는 술어들 [eqn: p _{i} IN P _{r} (`0`<`i` LEQ `d)]을 [eqn: S`']의 변수들과 대응시켜 새로운 술어의 집합  [eqn: Z`=` LEFT { z _{1} ,`...`,`z _{d} RIGHT }]을 생성한다. 따라서 [eqn: M`']의 리턴 값들은 [eqn: Z]에 할당된다.

[eqn: z _{i} `=`p _{i} [`x/ret,`a _{1} /f _{1} ,``a _{2} /f _{2} ,...,``a _{d} /f _{d} ]],      [eqn: z _{1} ,...,z _{d} `=`M`'(`...`);]

이 된다. 이 [eqn: Z]는 [eqn: S`']에 추가된 새로운 지역술어의 집합이 된다. 이제 마지막으로 [eqn: S`']에서 [eqn: x`]에 대응하는 술어의 집합 [eqn: r _{j} ` IN `R]을 추상화한다. 따라서 [eqn: r _{j} ` IN `R]에 대응하는 이진변수 [eqn: v _{j} IN V _{R}]의 값은 다음과 같이 추상화한다.

[eqn: v _{j} `=`select`(K(r _{j} ),`K( LNOT r _{j} `))]

이때 [eqn: K()]함수에서 [eqn: r _{j} ` IN `R]을 평가하기 위해 사용하는 이진변수의 범위는 [eqn: V`= LEFT { ((V _{G} ` CUP V _{S} ) RSLANT V _{R} ) CUP V _{Z} RIGHT }]이 된다. [eqn: S`']에서 [eqn: r _{j} ` IN `R]을 새롭게 얻어진 [eqn: V _{Z}]으로 평가하기 위해 [eqn: V _{R}]은 제외한다. 이로써, 자바 프로그램 [eqn: J]의 [eqn: x`]=[eqn: obj.M(a _{1} ,`a _{2} ,`...`,`a _{n} )]구문에 대한 메소드 호출의 추상화는 이진 프로그램 [eqn: OMEGA (J, P)]내에 생성된다. 다음은 sam()메소드 내에서 Exam2 클래스의 leo()메소드를 호출하는 예이다.

public class Exam2 {

public int leo(int n, int y) {

Predicate A1: y >= 0;

Predicate A2: n <= y;

Predicate A3: y == t1;

Predicate A4: y > t2;

int t1, t2;

… …

return t1;

}

}

public void sam(int m, int x) {

Predicate B1: m<=0;

Predicate B2: x==0;

Predicate B3: r==0;

int r;

if(m <= x) {

m=x;

}

else {

m=m+x

}

… …

Exam2 moov = new Exam2();

r=moov.leo(m, x);

… …

}

그림 5. 참조 메소드의 호출 예

위의 예를 보면서 참조 메소드인 moov.leo(m, x)를 호출하는 구문이 어떻게 추상화되는지를 보인다. 먼저, 추상화 1단계에 의해 다음의 Method_Info()가 저장된다.

Method_Info() =

(“Exam2", "leo", { n, y }, "t1", { n <= y, y <= 0 }, { y == t1} )

이제 추상화 2단계에 의해 sam()메소드 내의 할당문, 조건문과 함께 메소드 호출의 추상화를 수행한다. 먼저 object_table(“moov”, “Exam2”)을 이용해 sam()의 메소드 정보를 추출한다.

int leo(n. y)의 매개변수 n, y는 moov.leo(m, x)의 매개변수 m, x와 대응하기 때문에 [eqn: P _{f}] = { n <= y, y <= 0 }는 다음과 같이 치환된다.

(m <= x) = (n <= y)[ m/n, x/y ],   (x <= 0) = (y <= 0)[ m/n, x/y ]

따라서,

frm1 = select([eqn: K](m<=x), [eqn: K](￢(m<=x));

frm2 = select([eqn: K](x<=0), [eqn: K](￢(x<=0));

이다. 이때 frm1, frm2는 leo()의 중간매개변수이다. leo(frm1, frm2)로부터 [eqn: P _{r}] = { y == t1 }는 다음과 같이 치환된다.

(x == r) = (y == t1)[ r/t1, m/n, x/y]

따라서, R1 = moov.leo(frm1, frm2); 이다. 이진변수 R1은 (x == r)에 대응되고 sam() 메소드 내에 (x == r)가 지역술어로 추가된다. 마지막으로 변수 r에 대응하는 [eqn: R] = { r==0 }을 다음과 같이 추상화한다.

{ r==0 }=select((x==0) & R1, (x==0) & R1 );

결국, sam()메소드의 추상화는 [eqn: OMEGA (J, P)]내에 다음과 같이 생성된다.

public void sam(int m, int x) {

Predicate B1: m <= 0;

Predicate B2: x == 0;

Predicate B3: r == 0;

if( * ) {

assume( !(B2 & !B1));

B1 = select(B2, false);

}

else {

assume( !(B1 & B2));

B1 = select(B1 & B2, B2 & !B1);

}

Exam2 moov = new Exam2();

// n <= y 를 m <= x로 치환, 추상화

frm1 = select(B1 & B2, B2 & !B1);

//  y <= 0을 x <= 0으로 치환, 추상화

frm2 = select(B2, false);

//  leo()로부터 Predicate R1: x == r 생성

R1 = leo(frm1, frm2);

//  r에 대응하는 술어 r == 0의 추상화

B3 = select(B2 & R1, B2 & !R1);

}

그림 6. 참조 메소드의 추상화

3. 추상화된 자바 프로그램의 CTL 모델 체킹

이 장에서는 JAMES.abs에 의해 생성된 이진 프로그램 [eqn: OMEGA (J, P)]을 JAMES.mc에서 제어흐름 그래프로 변환하고 검증을 위한 CTL 모델 체킹 알고리즘을 보인다.

3.1 이진 프로그램의 변환

[eqn: OMEGA (J, P)]은 변수의 타입이 이진(boolean)형식만 사용이 가능한 프로그램이다.  [eqn: OMEGA (J, P)] 은 n 개의 이진 변수와 m 개의 프로그램 구문이 있다. 이진 변수는 [eqn: V`=` LEFT { v _{1} ,`...,v _{n} RIGHT }]으로 구성되고 모든 [eqn: v _{i} (0`<`i` LEQ `n)]에 대해서 [eqn: v` _{i``} IN LEFT { true,false,* RIGHT }]이다. 여기서 * 은 참과 거짓인지 알 수 없는 경우이다.

[eqn: PC SUBSETEQ ℕ]

[eqn: VALUE= LEFT { v _{1} ,...,v _{n} RIGHT }]

public void main( ) { Predicate C1: m<=10; Predicate C2: x==0; Predicate C3: r==true; int m = 0; int x = 0; boolean r = false; while( !r ) { if(m <= 10) { m++; }else { x = 1; r = true; } } }	1. public void main( ) { Predicate C1: m <= 10; Predicate C2: x == 0; Predicate C3: r == true; 2. C1 = true; 3. C2 = true; 4. C3 = false; 5. L1: 6. if( * ) { 7. assume( !(C3)); 8. if( * ) { 9. assume( C1); 10. C1 = select(false, !C1); }else { 11. assume( !(C1)); 12. C2 = false; 13. C3 = true; } 14. goto L1; } 15. }

여기서 [eqn: PC]는 프로그램의 위치를 의미한다. [eqn: OMEGA (J, P)]의 CTL 모델 체킹을 위해, [eqn: OMEGA (J, P)]을 다음과 같이 모델링 한다. [eqn: OMEGA (J, P)]에서 각각의 상태는 다음과 같이 구성된다.

그림 7. 자바 프로그램과 변환된 이진 프로그램

[eqn: S=PC TIMES WP (VALUE)]

[eqn: WP (VALUE)]는 이진 변수들의 가능한 값들의 멱집합이다. 상태의 전이를 구축하기 위해서는 주어진 프로그램에서 도달 가능한 상태들의 집합을 우선 구해야한다. 프로그램의 초기 구문에서 시작하여 상태의 변화가 더 이상 없을 때까지 계속 탐색을 수행한다. 각각의 구문에 따라서 전이를 추가한다. 다음과 같이 왼편의 자바 프로그램이 주어졌을 때 변환된 오른편의 [eqn: OMEGA (J, P)]을 예로 들어보자.

변환 된 이진 프로그램 [eqn: OMEGA (J, P)]은 모델 체킹을 위해 JAMES.mc에서 다시 제어흐름 그래프 [eqn: CFG(S,`init,`T,`final)]로 변환된다.

[eqn: CFG(S,`init,`T,`final)]

◦ [eqn: S`=`PC` TIMES WP (VALUE)]에서 각각의 상태 [eqn: s` IN `S] 는 프로그램의 위치와 이진 변수들의 가능한 값들의 멱집합을 갖는다.

◦ [eqn: init` IN `S] 는 프로그램의 시작지점인 초기 상태를 나타낸다.

◦ [eqn: T` SUBSETEQ `S` TIMES S] 는 상태들 간의 전이를 나타낸다.

◦ [eqn: final` IN `S] 는 프로그램의 종료지점인 최종 상태를 나타낸다.

따라서 그림 11 의 이진 프로그램의 제어흐름 그래프는 다음과 같다.

그림 8. 위 이진 프로그램의 제어흐름 그래프

위의 제어 흐름 그래프를 기반으로 도달 가능한 변수의 값을 검사할 수 있다. 그림 12 의 각 상태 [eqn: s` IN S] 내의 숫자는 [eqn: pc` IN `PC] 를 나타낸다. 이때 술어 구문은 원래 프로그램의 구문이 아니기 때문에 [eqn: PC] 에서 제외한다. 또한 술어 구문에서 선언된 이진 변수 값들은 모두 [eqn: true]라고 가정한다. 프로그램의 위치가 [eqn: pc=2], [eqn: pc=3] 일 때는 변수 값의 변화 없이 [eqn: OMEGA = LEFT { (C1,true),(`C2,`true),`(C3,`true) RIGHT }]를 갖는다.

[eqn: pc=4] 에서는 변수 [eqn: C`3]가 선언되면서 [eqn: false] 값이 대입된다. 따라서 프로그램 변수 값의 변경이 발생하게 된다. 프로그램의 변수 값은 [eqn: OMEGA = LEFT { (C`1,true),(C`2,true),(C`3,false) RIGHT }]이 된다. 그리고 [eqn: pc=3]에서 [eqn: pc=4]로 이동할 때 상태의 전이가 다음과 같이 추가된다.

[eqn: C`3=true WEDGE C`3 prime =false]

[eqn: pc=5]일 때는 라벨을 설정한 것이기 때문에 변수 값의 변경은 없고 프로그램의 위치만 이동된다.

[eqn: pc=6]에서는 if()문이 있고 참일 경우 프로그램의 실행 위치가 변경되게 된다. 변수 [eqn: C`3]의 값에 따라서 if()문의 분기가 일어나게 되는데 현재 [eqn: C`3]의 값이 조건문을 만족하기 때문에 현재에는 참인 부분으로만 프로그램 구문이 이동하게 된다. 따라서 현재 [eqn: pc=6]에서 [eqn: pc=7]로 가는 전이가 추가되게 된다.

[eqn: pc=7]에서는 [eqn: assume(!C`3)]에 의해 이 블록 내에서 [eqn: C`3]는 [eqn: false]로 가정한다. 하지만 [eqn: select(`)]문을 만날 때를 제외하고 블록 내의 다른 위치에서 [eqn: C`3]가 [eqn: true] 또는 [eqn: false]로 결정되어 있는 경우는 그 위치에 따른다.([eqn: pc=14]의 [eqn: C3`=`false])

[eqn: pc=8]에서는 다시 if()문을 만나게 되고 [eqn: C`1]의 값에 따라 분기가 일어나게 된다. 프로그램 실행 당시 [eqn: C`1]의 값은 [eqn: true]값을 가지고 있기 때문에 [eqn: pc=8]에서 [eqn: pc=9]로 전이된다. [eqn: pc=9]의 [eqn: assume(C`1)]구문은 이 블록 내에 [eqn: C`1]을 [eqn: true]라고 가정한다. 따라서 [eqn: pc=10]에서 [eqn: C`1]는 [eqn: select(false,`!C`1)]에 의해 [eqn: true]값을 가질 수 없고 [eqn: C`1]이 이 블록 내에서 [eqn: true]라고 가정했기 때문에 [eqn: C`1]은 [eqn: false]값도 가질 수 없다. [eqn: pc=10]에서 [eqn: C`1]은 최종적으로 알 수 없는 [eqn: *]값을 갖게 된다. 따라서 [eqn: pc=9]에서 [eqn: pc=10]으로 비결정적인 전이는 다음과 같다.

[eqn: (C`1=true WEDGE C`1 prime =`*`)`]

[eqn: pc=10]에서는 블록이 끝나고 제어 흐름에 따라 [eqn: pc=14]로 간다. 이 동안은 변수 값의 변경은 없고 [eqn: pc`=`14]에서 [eqn: goto]문이 나왔기 때문에 역시 변수 값의 변경 없이 프로그램의 위치만 [eqn: pc=5]로 변경하게 된다. 이 외에 만일 메소드가 호출되는 구문을 만나면 호출된 메소드로 이동한다. 이런 제어 흐름을 통해 상태공간을 탐색하게 된다. 프로그램의 위치를 변경한 이후에도 위의 방법을 이용해서 프로그램의 도달 가능한 상태와 전이 관계를 구축할 수 있다. CTL 모델 체킹을 수행하기 위해 프로그램이 종료 되는 시점인 [eqn: pc=15]는 자기 자신으로 가는 전이가 있다고 가정한다. 각각의 프로그램 위치에서 가질 수 있는 도달 가능한 변수 값들의 집합 [eqn: R SUBSETEQ S]는 다음과 같다.

[eqn: (2, LEFT { (T,`T,`T) RIGHT } )]

[eqn: (3, LEFT { (T,`T,`T) RIGHT } )]

[eqn: (4, LEFT { (T,`T,`F) RIGHT } )]

[eqn: (5, LEFT { (T,`T,`F),(*,`T,`F),(F,`F,`T) RIGHT } )]

[eqn: (6, LEFT { (T,`T,`F),(*,`T,`F),(F,`F,`T) RIGHT } )]

[eqn: (7, LEFT { (T,`T,`F),(*,`T,`F) RIGHT } )]

[eqn: (8, LEFT { (T,`T,`F),(*,`T,`F) RIGHT } )]

[eqn: (9, LEFT { (T,`T,`F) RIGHT } )]

[eqn: (10, LEFT { (*,`T,`F) RIGHT } )]

[eqn: (11, LEFT { (F,`T,`F) RIGHT } )]

[eqn: (12, LEFT { (F,`F,`F) RIGHT } )]

[eqn: (13, LEFT { (F,`F,`T) RIGHT } )]

[eqn: (14, LEFT { (*,`T,`F),`(F,`F,`T) RIGHT } )]

[eqn: (15, LEFT { (F,`F,`T) RIGHT } )]

3.2 이진 프로그램을 위한 CTL 모델 체킹 알고리즘

변환된 제어흐름 그래프에서 프로그램 구문과 변수 값의 변화를 살펴보기 위해 하나의 상태에 대한 프로젝션 함수를 다음과 같이 정의한다.

[eqn: proj _{pc} (pc,V)=pc]

[eqn: proj _{val} (pc,V)=V]

[eqn: LEFT . PROJ _{pc} (S _{1} ,S _{2} )= LEFT { eqalign{(proj _{pc} (s _{1} ),proj _{pc} (s _{2} ))# |s1 IN S1,s2 IN S _{2}} RIGHT } RIGHT .]  [eqn: LEFT . PROJ _{val} (S _{1} ,S _{2} )= LEFT { eqalign{(proj _{v} (s _{1} ),proj _{v} (s _{2} ))# |s1 IN S1,s2 IN S _{2}} RIGHT } RIGHT .]

여기에서 [eqn: OMEGA SUBSETEQ WP (VALUE)]는 현재 프로그램 위치에서 가능한 값들의 집합을 나타낸다. CTL 모델 체킹을 수행하기위해  [eqn: pre _{EXIST }] 연산자를 이 장에서는 이진 프로그램에 알맞게 재정의 한다.

[eqn: pre _{EXIST } (i,j)= LEFT { eqalign{(x,y) IN R|# (x`,i) IN PC` TIMES PC WEDGE # (y,j) IN WP (V) TIMES WP (V)} RIGHT }]

재 정의된  [eqn: pre _{EXIST }]을 이용해서 이진 프로그램을 위한 CTL 모델 체킹 알고리즘을 아래와 같이 정의한다.

[eqn: 〚(pc, OMEGA )〛= LEFT { eqalign{(pc, OMEGA )`` IN ``R vert OMEGA `` SUBSETEQ ``proj _{val} (R)# `` WEDGE pc IN proj _{pc} (R)} RIGHT }]

[eqn: 〚v〛= LEFT { eqalign{(pc,v) IN R``|v SUBSETEQ proj _{val} (R)# WEDGE pc IN proj _{pc} (R)} RIGHT }]

[eqn: 〚pc〛= LEFT { eqalign{(pc,v) IN R``|pc IN proj _{pc} (R)# WEDGE v=proj _{val} (R)} RIGHT }]

[eqn: 〚 BOT 〛= EMPTYSET]

[eqn: 〚 LNOT (pc,v)〛=S```"-"`〚(pc,v)〛]

[eqn: 〚(pc _{1} ,v _{1} )`` WEDGE ``(pc _{2} ,v _{2} )`〛# =〚(pc _{1} ,v _{1} )〛` SMALLINTER `〚(pc _{2} ,v _{2} )〛]

[eqn: 〚(pc _{1} ,v _{1} )`` LOR ``(pc _{2} ,v _{2} )`〛# =〚(pc _{1} ,v _{1} )〛` CUP `〚(pc _{2} ,v _{2} )〛]

[eqn: rm 〚EX(pc,v)〛= it pre _{EXIST } (〚(pc,v)〛)]

[eqn: rm 〚EG(pc,v)〛# =`` nu ``Z.(〚(pc,v)〛 SMALLINTER it ``pre _{EXIST } rm (Z`))]

[eqn: rm 〚E((pc _{1} ,v _{1} )`U``(pc _{2} ,v _{2} )``)〛# =`` mu ``Z.(〚(pc _{2} ,v _{2} )〛`` CUP `# `(〚(pc _{1} ,v _{1} )〛)`` SMALLINTER it ``pre _{EXIST } rm (Z`))]

[eqn: (PC,P)-(pc,j)=# LEFT { (pc prime ,p)|pc prime IN PC```"\"pc RIGHT } CUP LEFT { (pc,j prime )|j prime IN LNOT j RIGHT }] [eqn: LEFT { (i _{1} ,j _{1} ) RIGHT } SMALLINTER LEFT { (i _{2} ,j _{2} ) RIGHT }# = LEFT { eqalign{(i prime ,j prime )|(i prime IN PROJ _{val} (i _{1} ,j _{1} )# WEDGE i prime IN PROJ _{val} (i _{2} ,j _{2} ))WEDGE ``(`j prime =j _{1} SMALLINTER j _{2} )} RIGHT }][eqn: LEFT { (i _{1} ,j _{1} ) RIGHT } CUP LEFT { (i _{2} ,j _{2} ) RIGHT }# = LEFT { eqalign{(i prime ,j prime )|(i prime IN PROJ _{val} (i _{1} ,j _{1} ) WEDGE # i prime IN PROJ _{val} (i _{2} ,j _{2} ))``` WEDGE ``(`j prime =j _{1} CUP j _{2} )} RIGHT }]

모든 상태는 [eqn: (pc, OMEGA )]의 형태로 표현된다. [eqn: pc]는 현재 프로그램의 실행 위치를 나타내고 [eqn: OMEGA]는 [eqn: pc]에서 가질 수 있는 변수 값들의 집합을 나타낸다. CTL 로 속성을 명세할 때는 하나의 상태만을 표현해야 하는 것이 아니기 때문에 항상 [eqn: pc] 와 [eqn: OMEGA]를 입력할 필요는 없다. 따라서 다음과 같은 CTL 구문이 가능하다.

[eqn: EF```L1`:`b`=false]

여기서 [eqn: b]는 이진 변수를 나타내고 [eqn: L1]은 [eqn: b]의 값을 갖는 구문의 레이블이 된다. 따라서 위의 식은 제어흐름 그래프에서 [eqn: L1]이 레이블 된 위치에서 [eqn: b`=false]가 되는 경로가 존재하는 지를 검증한다. 또한 CTL 연산자는 EX, EG, EU만으로도 다른 모든 연산자 표현이 가능하다[11].

[eqn: LNOT (pc, OMEGA )]를 만족하는 집합을 구하는 방법은 다음과 같다. 전체 상태들의 집합에서 현재 상태들의 집합의 [eqn: pc]가 아닌 [eqn: pc]들의 집합이거나 현재 [eqn: pc] 중에 [eqn: OMEGA] 를 만족하지 않는 상태들은  [eqn: LNOT (pc, OMEGA )]인 상태들이다. [eqn: LEFT { (i _{1} ,j _{1} ) RIGHT } SMALLINTER LEFT { (i _{2,} j _{2} ) RIGHT }]는 두 개의 상태들이 동일한 [eqn: pc]를 가지고 있고 여러 변수의 값을 가지고 있을 경우의 합집합을 되돌려 준다.

4. 적용 사례

JAMES.abs를 통해 얻은 [eqn: OMEGA (J, P)]와 속성으로 기술한 CTL식을 JAMES.mc에 입력해서 간단한 자바 프로그램의 속성을 검증한다. [eqn: OMEGA (J, P)]는 JAMES.mc 내에서 제어흐름 그래프로 변환된다. 그리고 이 변환된 그래프의 제어흐름을 분석하여 주어진 속성이 만족하는 지를 검사한다. 검증해야 할 범용 속성에는 크게 안전성(Safety)과 궁극성(Liveness)으로 나뉜다. 안전성은 시스템 실행 도중, 나쁜 상태에 도달할 수 없음을 의미한다. 안전성의 대표적인 예는 교착상태의 부재이다. 궁극성은 시스템 도중 언젠가는 좋은 상태에 도달할 수 있음을 의미한다. 궁극성의 대표적인 예는 자원 사용 허가이다. 시스템이 정확하다는 것을 보장하기 위해서는 두 가지 속성이 만족됨을 보여야 한다. 대부분의 소프트웨어 모델체커에서는 검증할 수 있는 속성이 안전성에 국한되어 있지만 우리는 CTL식을 통해 자바 프로그램의 궁극성도 검증한다.

4.1. 문제 선정

먼저, 검증 대상으로 아래 그림 3의 핸드폰에 탑재되는 푸시푸시게임 50판을 선정하였다.

그림 9. 푸시푸시 50판과 이를 구현한 크레인 시스템

푸시푸시 게임은 플레이어가 보드위에 흩어져있는 공들을 목적지에 모두 옮겨놓으면 클리어된다. 이 게임을 교육용 로봇제작 툴킷인 LegoMindstorm[12]을 사용해 실제 구현하였다. 모터 2개와 터치 센서 2개, 레고 블럭을 이용해 크레인을 만들고 RCX라는 임베디드 시스템을 연결하였다. RCX는 8bit CPU와 32K 메모리, LCD창, 그리고 각종 센서를 부착할 수 있는 포트들로 구성된다. RCX에 적재할 Firmware로는 자바 프로그램을 지원하는 LeJos(Lego JavaOS)를 선택하였다. 메모리에 LeJos환경을 올리고 남는 16K의 메모리는 자바 프로그램을 적재할 수 있는 공간이 된다. 또한 LeJos는 레고로봇을 위해 JDK1.1버젼의 일부분만을 지원하기 때문에 검증이 수월하였다.(JAMES.abs는 JDK 1.2를 지원한다) 이 크레인은 Arm을 이용해 공을 상, 하, 좌, 우로 움직이며, 터치센서를 통해 Arm이 움직이는 거리를 측정하고 다음 움직임을 결정한다.

푸시푸시 게임 50판은 48개의 셀로 구성되며 237의 큰 상태공간을 사용하기 때문에 사람이 손으로 풀기에는 쉽지 않은 게임이다. 따라서 우리는 크레인이 초기위치부터 목적지까지 공들을 모두 옮길 수 있는 경로(338 step)를 모델체커 SMV에서 반례생성을 통해 얻어내었다[11]. 그리고 크레인이 이 경로를 따라 Arm을 움직여서 모든 공을 목적지로 옮기는 자바 프로그램을 작성하였다.

4.2 속성 검증

작성한 자바 프로그램에서 검증하려는 안전성 속성과 궁극성 속성을 아래와 같이 CTL식으로 기술한다.

1) [eqn: LNOT EF```L1`:` LNOT](game == "Clear")

이 안전성 속성의 의미는 “game이 Clear되지 않는 경우는 존재하지 않는다” 이다. 다시 말해서, 크레인이 모든 공을 목적위치에 옮겨놓지 못하는 경우는 존재하지 않는다는 것이다. 검증을 위해 프로그램 내, 게임이 클리어 되어야 하는 지점에 game = “Clear”; 를 삽입하고 프로그램을 추상화하여 이 구문이 참이 되는지 분석한다. 위 식이 거짓이면, 게임이 클리어 되지 않는 경로를 보여준다.

2)  [eqn: AG`]( [eqn: L2`:] (sensing == [eqn: true])  ⇒ [eqn: AF``L3`:] ( lr_cycle_cnt ++ ) )

이 궁극성 속성의 의미는 “언제나 sensing이 일어나면 언젠가는 lr_cycle_cnt가 1증가 한다” 이다. 다시 말해서, 언제든지 크레인의 터치센서가 센싱되면 움직인 거리가 측정되고 다음 움직임을 결정한다. 만약 터치센서가 센싱되도 lr_cycle_cnt가 증가하지 않으면 다음 움직임 없이 Arm은 한 방향으로만 무한히 진행된다.

위 두 가지 속성을 검증한 결과, 크레인 시스템 프로그램이 주어진 경로에 따라 오작동 없이 공을 모두 목적지까지 옮길 수 있다는 것을 알 수 있었다. 따라서 실제 시스템을 실행한 결과도, 시스템이 올바르게 동작하여 모든 공을 목적지까지 옮기고 게임이 종료되었다.

만일 크레인에 오동작이 발견되었다면 발견된 에러에 대해 CTL 속성을 기술하고 모델 체킹해서 왜 에러가 발생했는지에 대한 반례를 생성해 줄 수 있다. 이 반례는 크레인이 오동작하는 일련의 행위가 된다. 따라서 반례를 보고 에러를 디버깅할 수 있다.

5. 성능 최적화 및 개선

술어추상화는 추상화 수행 시 정리증명기를 빈번하게 호출한다. 최악의 경우, 술어의 집합  [eqn: P]를 입력할 때 약 [eqn: O(2 ^{|P``|} )]만큼 정리증명기를 호출하게 된다. 따라서 JAMES의 전체 성능을 향상시키기 위해서는 front-end인 JAMES.abs에서 얼마나 정리증명기의 호출 횟수를 줄이느냐가 관건이다. 결국, 술어가 추가될 때마다 정리증명기의 호출횟수는 기하급수적으로 늘어나기 때문에 추상화 수행 시 불필요한 술어들을 제거해야한다. 다음은 JAMES의 성능 최적화를 위해 JAMES.abs에 적용한 몇 가지 방법이다.

1) 할당문의 술어 추상화에서 각 할당문이 [eqn: P] 내의 모든 술어들에 대해서 추상화되지는 않는다. [eqn: W`P`(`x=e,`p _{} `)`=`p]의 경우 할당문의 [eqn: x]와 [eqn: p]는 관련되지 않는다. 따라서 이런 경우 [eqn: p]는 추상화 전에 제거한다.

2) [eqn: assume(`)]문의 [eqn: LNOT K( LNOT `p`)]를 구할 때, [eqn: p]를 만족하는 술어는 단항 술어나 술어들 간의 [eqn: conjunction( WEDGE )]으로 이루어진다. 이때 [eqn: p]를 만족하는 술어 조합들 간에 포함관계가 생기게 되는데 이들 중 포함되어지는 술어 조합은 제거해도 무방하다. 예를 들어, 어떤 술어의 조합 [eqn: a _{1} WEDGE a _{2}]이 [eqn: p]를 만족하고 [eqn: a _{1} WEDGE a _{2} WEDGE a _{3}]도 [eqn: p]를 만족하면 [eqn: a _{1} WEDGE a _{2} SUBSETEQ a _{1} WEDGE `a _{2} WEDGE a _{3}]이다. 이때 [eqn: LNOT K( LNOT `p`)]의 집합에서 술어[eqn: a _{1} WEDGE a _{2} WEDGE a _{3}]는 제거해도 무방하다.

실험	자바 프로그램	라인 수	[eqn: |P`|]	호출 횟수	실행시간(sec)	적용
1	LejosPush50+1	328/219	21/4	907	32	1) ~ 5)
2	LejosPush50	340	25	907	32	1) ~ 5)
3	LejosPush50	340	25	1122	39	1), 5)

3) 또한 [eqn: K(`p`)]를 구할 때, [eqn: p]를 만족하는 술어는 단항 술어나 술어들 간의 [eqn: conjunction( WEDGE )]으로 이루어진다. 이때 술어의 집합 [eqn: P]가 커질 경우 [eqn: conjunction( WEDGE )]의 길이가 길어지고 [eqn: p]를 만족하는 술어의 개수 [eqn: |K(`p`)|]도 많아지게 된다. 이런 경우 상수 [eqn: b]를 설정해 [eqn: conjunction( WEDGE )]의 길이를 제한할 수 있다. 또한 [eqn: |K(`p`)|]의 개수도 제한 가능하다. [eqn: conjunction( WEDGE )]와 [eqn: |K(`p`)|]의 제한은 술어 정보의 부족으로 추상화의 정확성을 떨어뜨릴 수 있기 때문에 적절한 값을 선택해야 한다. 본 논문에서는 [eqn: b`=`2]로 제한하였고 조건문의 [eqn: assume(`)] 구문에 대해서만 술어의 개수를 [eqn: | LNOT K( LNOT `p`)|`=`4`]로 제한하였다. [eqn: b`=`2]이기 때문에 할당문에서의 [eqn: |K(`p`)|]를 따로 제한하지 않았다.

<표 1> LejosPush50 자바 프로그램의 추상화 결과

4) [eqn: C _{1} `` RARROW `C _{2}]의 경우 [eqn: C _{1}] 자체가 [eqn: false]라면 [eqn: C _{1} `` RARROW `C _{2}]는 [eqn: C _{2}]가 어떠한 진리 값을 갖더라도 항상 참인 식이 되고 [eqn: C _{1}]은 [eqn: C _{2}]를 만족하는 술어가 된다. 따라서 본 논문에서는 술어 평가 전에 [eqn: C _{1}]과 같은 술어를 제거한다. 예를 들어, [eqn: K(`x`<`3`)]를 구할 때 [eqn: P`= LEFT { x == `0,`x`<`-1 RIGHT }]이라고 가정하자. 이때 [eqn: (x` == `0` WEDGE `x``<`-1)`` RARROW `(``x`<3`)]는 참이 된다. 하지만 [eqn: x==0]과 [eqn: x`<`-1]은 동시에 참이 될 수 없기 때문에 [eqn: K(`x`<`3`)]에서 [eqn: LEFT { x` == `0` WEDGE `x``<`-1 RIGHT }]은 제거한다.

5) 할당문의 술어 추상화에서 [eqn: SQCAP (`K(p)`)]는 [eqn: p]를 만족하는 가장 약한 술어이다. 먼저 [eqn: K(p)`]를 구하기 위해 단항 술어부터 약한 술어의 조합을 만들어나가고 [eqn: p]를 만족하는 술어의 조합을 차례로 배열에 정렬한다. 따라서 정렬된 배열의 첫 번째 인덱스부터 계산하여 가장 약한 술어[eqn: SQCAP (K(p)`)]를 구할 수 있다.

위의 방법들 중 1), 2), 4)는 기존의 소프트웨어 모델체커에서 거론되고 있는 최적화 방법들이다. 이 외에 우리는 3), 5)방법들을 JAMES.abs에 추가하여 다음과 같은 실험결과를 얻었다.

실험 대상으로 사용한 프로그램은 5장의 적용사례에서 사용된 레고 로봇에 탑재되는 자바 프로그램이다.

- 실험 1에서는 LejosPush50 클래스가 다른 클래스의 메소드를 참조한다.

- 실험 2에서는 LejosPush50 클래스가 다른 클래스의 메소드를 참조하지 않고 자체 메소드를 사용하였다. 실험 1처럼 술어의 개수와 최적화 적용 방법은 동일하게 하였다. 이때 정리증명기

의 호출횟수와 실행시간에는 변동이 없었다. JAMES.abs는 추상화 전에 모든 클래스의 메소드 정보를 추출한다. 실험 1에서는 두 개 클래스의 모든 메소드 정보를 추출하고 실험 2에서는 하나의 클래스의 메소드 정보를 추출한다. 결국 메소드 정보의 추출은 거의 실행시간에 영향을 미치지 않는다.

- 실험 3에서는 최적화 방법 1)과 5)만 적용하였다. 위 표에서 정리증명기의 호출 횟수와 실행 시간이 눈에 띄게 증가한 것을 알 수 있다. 이는 술어 추상화 수행 시 정리증명기의 호출 횟수가 실행시간에 얼마나 많은 영향을 끼치는 지를 보여준다.

6. 결론 및 향후 연구 과제

오늘날, 소프트웨어 자체의 논리적 에러를 찾아내기 위해 소프트웨어 모델체커에 관한 연구가 매우 활발하다. 하지만 아직까지 자바프로그램에 대해 안전성 속성과 궁극성 속성 모두를 검증하는 소프트웨어 모델 체커는 없었다. 따라서 우리는 간단한 자바 프로그램을 대상으로 CTL식의 범용 속성을 검증하는 모델체커인 JAMES를 개발하였다. 본 논문에서 자바 프로그램과 술어의 집합을 받아들여 이진프로그램으로 추상화시키는 JAMES.abs와 추상화된 이진 프로그램을 제어흐름 그래프로 변환해서 어떻게 JAMES.mc로 검증하는 지를 보였다. JAMES.abs에서는 JDK 1.2버젼의 모든 자바 구문을 받아들이고 참조 변수와 참조 메소드에 대한 객체 참조와 기본 구문들을 다룬다. 그리고 실제 크레인 시스템을 구현하여 그 시스템에 탑재된 자바 프로그램의 다양한 속성들을 검증하였다. 속성은 CTL식을 이용하기 때문에 안전성 속성과 궁극성 속성 모두 표현이 가능하다. 따라서 두 가지 속성 모두 검증한 결과, 크레인 프로그램이 주어진 경로에 따라 오작동 없이 공을 모두 목적지까지 옮길 수 있다는 것을 알 수 있었다. 또한 실제 시스템을 실행한 결과도, 시스템이 올바르게 동작하여 모든 공을 목적지까지 옮기고 게임이 종료된다는 것을 확인할 수 있었다. 또한 JAMES의 성능 향상을 위해 정리증명기의 호출을 최적화하는 방법을 보였다. 하지만 현재는 자바 프로그램의 정적인 부분에 대해서만 술어추상화가 적용되고 있다. 따라서 자바의 다중 쓰레드나 외부 라이브러리에 대한 술어추상화 연구가 필요하다. 또한 CTL식으로 표현된 속성이 주어지면 자동으로 효율적인 술어의 집합을 추출해내는 기법도 향후 연구해야 할 중요한 과제이다. 마지막으로 JAMES는 현재 추상화 - 모델 체킹 과정으로 이루어진다. JAMES.mc는 모델 체킹을 수행한 후 속성을 만족하면 [eqn: true], 만족하지 않으면 반례를 생성하고 반례가 실제 코드에서 도달가능 한 경로이면 [eqn: false], 그렇지 않으면 가짜 반례로 판단한다. 추상화된 [eqn: OMEGA (J, P)]은 [eqn: J] 보다 행위가 더 많은 상위 근사화(Over approximation) 된 모델이기 때문에 [eqn: J] 에서는 도달 가능하지 못한 경로를 가질 수 있다. 현재 가짜 경로를 제거하는 추상화개선 단계를 연구 중에 있다.

참고 문헌

프로그래밍언어논문지 제 권 제 호 (    . )

[1] E. M. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, 1999.

[2] E. M. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith, “Progress on the     State Explosion Problem in Model Checking,”in Proceedings of 10 Years Dagstuhl, LNCS 2000, pp.154-169, 2000

[3] 김태효, 차성덕, “코드기반 모델 체킹 방법의 연구동향,” 정보과학회 소프트웨어공학회지, 제15권 제2호, pp.3-16, 2002.

[4] T. Ball, R. Majumdar, T. Millstein and S.K. Rajamani, "Automatic Predicate Abstraction of C programs," SIGPLAN Notices, Vol. 36, No.5, pp.203-213, 2001.

[5] T.A. Henzinger, R. Jhala, R. Majumdar and G. Sutre, "Lazy Abstraction," in Proceedings of Principles of Programming Languages, pp.58-70, 2002.

[6] S. Charki, E.M. Clarke, A. Groce, S. Jha and H. Veith, "Modular Verification of Software Components in C," IEEE Transactions on Software Engineering, Vol.30, No.6, pp.388-402, 2004.

[7] J. Corbett, et.al., "Bandera: Extracting Finite-state Models from Java Source Code," in Proceedings of International Conference on Software Engineering, 2000.

[8] W.Visser, S.Park, J.Penix. “Using Predicate Abstraction to Reduce Object-Oriented Programs for Model Checking” - FMPS'00. 9

[9] E. A. Emerson, Temporal and modal logic, in the Handbook of Theoretical Computer Science：Formal Models and Semantics, J. van Leeuwen, editor, Elsevier, pp.995-1072, 1990.

[10] S. Graf and H. Saidi, "Construction of Abstraction State Graphs with PVS," in Proceedings of Computer Aided Verification, pp.72-83, 1997.

[11] A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani and A. Tacchella, “NuSMV 2：An OpenSource Tool for Symbolic Model Checking,” In Proceedings of CAV ’02, 2002.

[12] G. Farrari, A. Gombos, S. Hilmer, J. Stuber, "Programming Lego Mindstorms with Java: The Ultimate Tool for Mindstorms Maniacs," Syngress, April 2002.

[13] http://research.compaq.com/SRC/esc/

Simplify.html

이 정 림

2004년 경기대학교 전자계산학과 졸업(학사)

2004년~현재 경기대학교 전자계산학과 석사과정

관심분야 : 정형 기법, 임베디드 소프트웨어, 소프트웨     어 모델링

이 태 훈

2003년 경기대학교 전자계산학과 졸업(학사)

2005년 경기대학교 전자계산학과 졸업(석사)

2005년 ~ 현재 경기대학교 전자계산학과 박사과정

<관심분야> 모델 체킹 , 정형기법, 소프트웨어 공학

권 기 현

1985년 경기대학교 전자계산학과 졸업(학사)

1987년 중앙대학교 전자계산학과 졸업(이학석사)

1991년 중앙대학교 전자계산학과 졸업(공학박사)

1998년~1999년 독일드레스덴 대학 전자계산학과 방문교수

1999년~2000년: 미국 카네기 멜론 대학 전자계산                  학과 방문교수

1991년~현재: 경기대학교 정보과학부 교수

<관심분야> 소프트웨어 모델링, 소프트웨어 분석, 정형 기법등