|
프로그램을 테스트하는 방법은 프로그램의 실행 여부에 따라 정적 분석-(Static analysis) 방법과 동적 분석(Dynamic analysis) 방법으로 분류할 수 있다. 동적 분석 방법은 프로그램을 실제로 수행하여 오류를 검출하는 반면, 정적 분석 방법은 프로그램을 실행하지 않고 프로그램 및 명세를 검토하여 오류를 검출한다. 이 장에서는 정적 분석 방법을 사람의 관여 정도에 따라 사람 중심 분석 방법과 도구 기반 분석 방법으로 분류하여 설명한다.
대표적인 사람 중심 분석 방법으로는 공식 검토(Formal review, FR), 인스펙션(Inspection), 워크쓰루(Walkthrough) 등을 들 수 있다. 이 방법들은 여러 전문가들이 모여 코드를 검토하여 오류를 검출한다. 이러한 사람 중심 분석 방법은 기본적으로 프로그램을 실행하지 않고 여러 전문가들이 모여 문서와 코드 검토를 통해 오류를 검출하므로 소프트웨어 개발 중에 생성되는 모든 산출물들에 대해서도 적용할 수 있다는 이점이 있다. 즉, 요구사항 명세서, 설계 명세서, 심지어 테스트 계획서와 같은 문서들이 올바르게 작성되었는지를 판단하기 위해 정적 분석 방법을 이용할 수 있다.
위에서 열거한 방법들 외에도 자동화된 도구를 사용하여 정적 분석을 수행할 수있다. 예를 들면, 컴파일러는 문법 오류 등과 같은 기본적인 오류들도 검출할 수 있을 뿐만 아니라 경우에 따라 프로그램 내에 무한 루프나 절대 실행할 수 없는 프로그램 문장 등을 검출하는 기능도 있다. 이 장에서는 도구 중심 분석 방법으로 심볼릭 실행(Symbolic execution), 자료 흐름 분석(Data flow analysis) 및 형식적 검증(Formal verification)에 대해서 기술한다.
정적 분석 방법을 분류하여 도식화하면 그림과 같다.
4.1 공식 검토
공식 검토(Formal review)는 각 SW 개발 단계에서 산출된 작업 결과물이 제대로 되었는지를 판별하기 위해 각 개발 단계의 종료 시점에서 수행되는 정적 분석 방법이다. 공식 검토가 인스펙션이나 워크쓰루와 같은 동료 검토와 가장 크게 다른 점은 다음 단계로 진행될지 여부를 승인하는 단계가 있다는 점이다.
이러한 공식 검토에는 SW 요구사항 검토(Software requirementsreview, SRR), SW 아키텍처 설계 검토(Preliminary design review,PDR), 상세 설계 검토(Critical design review, CDR) 및 테스트 준비 검토(Test
readiness review, TRR) 등이 있다.
명칭(약어) | 검토 내용 |
SW 요구사항 검토 (Software requirementsreview SRR) | 요구사항의 적절성 기술적 타당성 요구사항의 완전성 검증 가능성 등 |
SW 아키텍처 설계 검토 (Preliminary design review PDR) | SW 아키텍처의 기술적 타당성 - 사용된 설계기법에 대한 기술적 적절성 - 설계 시 기능과 성능에 대한 요구사항 반영의 적절성 - SW와 HW 및 사용자와의 인터페이스 적절성 |
상세 설계 검토 (Critical design review CDR) | 코딩 작업 전 상세설계의 기술적 타당성, 완벽성 및 정확성 |
테스트 준비 검토 (Test readiness review TRR) | 단위 및 통합 테스트 결과 테스트 절차의 완전성 인수 테스트 준비 완료 여부 |
표. 공식 검토
공식 검토도 인스펙션이나 워크쓰루와 같이 검토를 위해 팀을 구성해야 한다. 그러나 공식 검토는 인스펙션이나 워크쓰루와는 달리 시스템 개발 진행에 대한 승인권을 가지므로 회의 참가자들을 선정할 때 특히 주의해야 한다. 동료 검토에서는 검토자들이 비슷한 직급의 사람들로 구성되지만 공식 검토에서는 직급이 보다 높은사람들로 구성된다. 특히 중재자는 프로젝트에 관한 지식을 잘 갖추고 있어야 하며 개발팀과 좋은 관계를 유지하고 있어야 한다. 공식 검토의 절차는 아래와 같다.
① 계획(Planning) 단계 : 각 개인에게 역할을 할당하고, 시작 조건과 종료 조건을 정의한다.
② 킥오프(Kick-off) 단계 : 문서를 분배하고 참가자들에게 검토 목적, 프로세스들에 대해 설명한다.
③ 개별 준비(Individual preparation) 단계 : 참가자별로 잠재 결함을 체크하고 회의에서 제기할 문제 및 코멘트를 준비한다.
④ 리뷰 미팅(Review meeting) 단계 : 문서화된 기록 또는 상세한 기록과 더불어 논의와 로깅을 한다. 미팅 참석자들은 결함을
처리하기 위하여 의견을 제시하거나결함에 대한 수정 여부를 결정 하기 위하여
간단하게 결함을 기록할 수 있다.
⑤ 재작업(Rework) 단계 : 작성자(Author)가 발견된 결함을 고친다.
⑥ 추가 작업(Follow up) 단계 : 사후 점검 단계에서는 처리된 결함을 확인하고 측정기준을 수집하여 종료 조건을 확인한다.
공식 검토에 참여하는 참가자의 역할은 다음과 같다.
• 관리자(Manager) : 검토 실행에 대한 결정을 하고 프로젝트 일정 내에서 검토 시간을 할당한다.
또한, 리뷰의 목표가 달성되었는가를 결정한다.
• 중재자(Moderator) : 검토 계획, 미팅 운영, 미팅 후 사후관리 등을 이끈다.
• 작성자(Author) : 문서에 대한 책임이 있는 사람으로 검토 시 자신의 결과물에 대해 설명한다.
• 검토자(Reviewer) : 검토자는 특정기술 혹은 비즈니스 배경을 가지고 있는 사람이 담당하며, 검토 기간 동안 제품에서
발견된 사항을 정의하는 역할을 한다.
• 기록인(Recorder) : 검토 기간의 모든 이슈사항, 결함, 그리고 미팅 동안 제기된 문제점 등 회의 내용을 기록하여 문서화하는
역할을 한다.
공식 검토 과정은 인스펙션 과정과 별다른 차이점은 없으나 작업 결과물이 승인된 경우에는 다음 개발 단계로 진행을 한다는 점이 다르다.
그림에서 볼 수 있듯이 검토 회의의 결과는 완전 승인, 부분 승인, 승인 거부의 3가지 형태가 될 수 있으며, 결과에 따라 각기 다른 작업 흐름을 수행한다.
• 완전 승인 : 다음 개발 단계로 즉시 이전할 수 있다. 간혹 약간의 수정 작업이 요구되는 경우도 있다.
• 부분 승인 : 작업물의 일부분은 승인되어 다음 단계로 갈 수 있지만 나머지 부분은 수정 작업이 요구된다.
이 경우는 다시 공식 검토 과정을 처음부터 거치지 않고 수정 부분을 담당한 검토인이 승인하거나 필요에 따라
해당 부분만을 검토하는 특별 검토 회의에 의해 승인된다.
• 승인 거부 : 공식 검토가 다시 필요한 경우이다. 작업물에서 매우 심각한 오류들이 많이 발견된 경우에는 개발자가
수정 작업을 거친 후 다시 공식 검토 과정을 거쳐야 한다.
4.2 인스펙션
인스펙션(Inspection)은 품질을 높이기 위한 목적으로 사용되는 정형적인 검토를 지칭한다. 1970년대 초 IBM에서 처음 사용되었으며 페이건(Fagon)에 의해 정립되었다. 페이건은 가능하면 오류가 발생한 시점에서 가까운 시기에 오류를 제거하기 위하여 좀 더 구조적이고 절차적인 방법이 필요하다는 생각에서 인스펙션 프로세스를 정립하였다.
4.2.1 목적
인스펙션이나 다음절에서 설명할 워크쓰루는 개발과정에서 수행하는 동료 검토(Peer review)라고 할 수 있다. 동료 검토란 비슷한 직급이나 역할을 담당하는 사람들이 개발 단계의 산출물을 프로그램의 소스 코드를 분석하여 세부사항들을 검토하는 작업을 말한다. 동료 검토의 목적은 개발 초기 단계에서 검사하는 제품의 결함을 찾아내는 것이다. 시스템 생명 주기의 각 단계에서 표 와 같은 인스펙션 활동이 이루어진다.
프로그램 개발이 완료된 후에 발견되는 오류를 수정하기 위해서는 많은 시간과 비용이 소요되므로 인스펙션 활동을 통해 가능한한 개발 초기에 오류를 찾아내고 수정함으로써 프로그램의 품질을 향상시키고 개발 비용을 줄이고자 하는 것이다.
프로그램 개발이 완료된 후에 오류를 수정하는데 소요되는 비용은 요구 단계나 설계 단계에서 오류를 수정하는 비용보다 100배 이상 많은 비용이 소요된다. 따라서 오류가 발생하면 가능한 빨리 검출하여 제거하여야 한다.
개발 단계 | 인스펙션 활동 |
요구사항 분석 | • 개발자와 테스트 엔지니어, QA 분석가는 기술적인 가능성, 투명성 그리고 타당성을 점검 • 테스트 엔지니어는 테스트 가능성을 점검 |
설계 | • 기술전문가는 기술적 적합성과 설계의 신뢰성을 점검 • 비즈니스 분석가는 요구사항에 적합한지를 분석 • 사용자는 사용 용이성을 점검 |
코드 | • 코드의 구조 및 표준과의 적합성 등을 점검 |
테스트 | • 테스트 계획 및 검토, 테스트 절차와 환경 점검, 테스트를 수행 |
설치 | • 설치과정 등을 점검 |
표. 개발 단계에 따른 인스펙션 활동
4.2.2 인스펙션 참가자의 역할
올바른 인스펙션 과정의 수행은 인스펙션을 더 효율적이게 하고 자원과 시간의 낭비를 줄일 수 있다. 인스펙션에 참여하는 참가자의 역할은 다음과 같다.
• 중재자(Moderator) : 인스펙션 중재자의 주된 임무는 검토 대상을 기초로 인스페션 참가자들을 선택하고 인스펙션을 계획하는 일이다. 중재자는 인스펙션 참가자들에게 미리 검토할 자료를 전달하여야 하며 참가자들이 인스펙션 회의를 충분히 준비할 수 있게 해야 한다. 인스펙션 회의에서 중재자는 회의를 주재하는역할을 담당한다. 또한 인스펙션 회의 또는 준비 기간 동안 발생할 수 있는 참가자간의 불화 또는 예기치 않는 상황에 잘 대처하여야 하며 인스펙션 회의를 마친뒤 어떤 후속 조치가 필요한지 신속히 결정할 수 있어야 한다.
• 검토인(Inspector) : 인스펙션 회의를 위해서 전달 받은 자료를 충분히 검토해야하고 인스펙션 회의를 준비해야 한다. 또한 검토인은 검토할 작업물을 충분히 이해하도록 노력하여야 하고 주어진 자료에서 오류를 찾아내고 기록한다. 검토인은 해결자의 입장이 아니기 때문에 찾아낸 오류를 해결하기 위해 노력하지 말아야 하고 간단한 의견만 제시하여야 한다. 다른 사람의 의견을 비판하거나 개발자를 비판하기 위해 인스펙션 회의에 참가하는 것이 아니라 개발자와 인스펙션 팀을 돕기 위해 인스펙션 회의에 참가하는 것이므로 개인적인 친분은 배제하고 최대한 객관적인 관점에서 회의에 참가해야 한다.
• 작성자(Author) : 인스펙션에 필요한 자료를 제출하여야 하며 자료 내용에 관한 설명을 하거나 질문에 대답을 할 수 있어야 한다. 개발자는 회의 내용을 경청하고 토의에 적극적으로 참가하여야 하며, 방어적인 자세로 회의에 참가해서는 안된다. 회의가 끝난 후에는 검출된 오류 내용에 대하여 후속조치를 해야 한다.
• 기록자(Recorder) : 기록자는 인스펙션 회의에서 논쟁, 모든 질문 및 답변 등을 기록한다. 또한, 인스펙션 회의가 종료되면 기록된 사항들을 정리하여 문서화하여야 한다. 따라서, 기록자는 인스펙션 회의의 토론을 이해하고 의미있는 문서를위해 충분한 지식을 갖추어야 한다. 또한, 기록자는 회의에서 회의 중재자나 작성자 입장이 아닌 검토자 입장에서 참가해야 한다.
• 판독자(Reader) : 작성자 외의 다른 사람이 판독자 역할을 맡아야 하며 인스펙션의 진행속도를 조정하는 역할을 한다. 작업물에 대해 이해하고 있어야 하며 작업물의 세부 로직이나 문서의 주요 요소에 대해 부연 설명이 가능해야 한다.
• 테스터(Tester) : 인스펙션 참가자 중 테스터가 포함되며 인스펙션 이후 테스트를 진행하게 될 사람이 참석한다.
4.2.3 인스펙션 과정
일반적인 인스펙션 과정의 각 단계는 다음과 같다.
① 계획(Planning) 단계 : 인스펙션을 계획하고 팀을 편성하고 팀원에게 역할을 할당한 후 스케줄을 계획하는 일로 중재자에게 책임이 있다. 인스펙션을 위한 팀은 각각 중재자, 판독자, 작성자, 기록인, 테스터, 검토인의 역할을 담당하는 4~7명 정도의 인원으로 구성된다. 구성원 모두 검토인의 역할을 수행한다. 즉, 이미 중재자와 같은 다른 역할이 있다 할지라도 검토인으로서의 역할을 수행한다. 검토인은 주어진 산출물을 분석하여 오류를 찾아내는 작업을 수행한다.
② 개요(Overview) 단계 : 작성자에게 책임이 있으며 인스펙션 팀원을 교육한다. 이는 검토인들에게 보다 친숙하게 검토할 작업물에 대한 이해도를 높이기 위함이다. 검토인은 작업물에 대한 이해를 높이기 위한 질문을 할 수 있지만 이 단계에서 더 나은 해결책(설계 또는 구현 방법)을 제안하거나 오류를 수정하는 것과 같은 작업은 하지 않는다. 만약 참가자 모두가 검토할 작업물에 대해 충분한 지식을 가지고 있다면 이 단계는 생략할 수 있다.
③ 준비(Preparation) 단계 : 참여자에게 인스펙션 자료를 제공하고 각자 자신이 맡은 역할을 준비한다. 이 때 검토할 작업물의 크기는 한 두 시간 안에 검토될 수 있는 크기이어야 한다. 프로그램의 경우 주석문을 포함하여 200 라인 이상을 검토하게 해서는 안되며 기능적 명세는 3~5쪽 이내이어야 한다
④ 인스펙션(Inspection) 단계 : 실제 결함을 찾는 과정으로 오류의 유형을 나열한 체크리스트를 이용한다. 인스펙션 회의 시간은 대략 45분에서 2시간 정도로 한정한다. 2시간 이내에 끝낼 수 없다면 다음 회의로 연기하여 다루지 못한 부분을 처리한다. 이 결과 발견된 결함은 표와 같은 방법으로 분류한다.
인스펙션 중에는 작업물에 대한 검토를 하며 작성자에 대한 평가는 하지 않도록 한다. 작성자는 본인의 작업물에 대해 설명하고 회의의 이해를 돕는 역할을 해야 하지만 너무 방어적인 태도를 가져서는 안 된다. 이 때 명심할 것은 인스펙션에서는 오류를 제거하고 해결하는 방안에 대한 토론은 하지 않는다는 사실이다. 만약 작성자가 해결방안에 대한 피드백을 원한다면 인스펙션 후에 작성자가 주체가 되어 검토인에게 문의할 수 있다.
구분 | 분류 | 설명 |
중요도 | Major | 사항이 중대할 경우 |
Minor | 사소한 문제의 경우 | |
Missing | 필요한 요소가 누락되었을 경우 | |
종류 | Wrong | 요소가 잘못되었거나, 불합리하거나, 표준에 적합하지 않을 경우 |
Extra | 부가요소가 나타나거나, 표준에 부합하지 않는 경우 |
표. 인스펙션 결과 결함 분류
⑤ 프로세스 개선(Process improvement) 단계 : 중재자에게 책임이 있으며, 인스펙션 결과에 대해 분석한다.
인스펙션 결과를 분석할 때 고려해야 할 사항은 다음과 같다.
• 인스펙션율(Inspection rate) : 시간당 검사된 설계 페이지 수
• 결함밀도(Fault density) : 검사된 KLOC당 결함 개수
• 결함발견율(Fault detection rate) : 시간당 발견된 결함 개수
• 결함발견효과(Fault detection efficiency) : 사람당 발견한 결함 개수
⑥ 재작업(Rework) 단계 : 작성자는 발견된 결함을 실제 작업물에 수정하는 작업을 수행한다. 예를 들면 코드 인스펙션에서 이러한 작업은 코드를 변경하는 작업, 주석문을 추가하거나 제거하는 작업 및 프로그램 구조를 재구성하는 작업이 포함될 수 있다.
⑦ 후속작업(Follow up) 단계 : 중재자가 발견된 모든 오류들에 대해 재작업이 충분하게 이루어지는지 확인한다. 만약 충분하게 이루어지지 않았다면 재작업을 반복적으로 수행한다.
4.2.4 인스펙션 예제
여기서는 어느 항공사의 좌석 예약프로그램에 대한 요구사항 명세와 문서 작성 표준을 인스펙션 하는 예를 살펴본다. 4.2.3절에서 명시한 바 대로 각 과정에 따라 인스펙션이 이루어지며 인스펙션 후 결함에 대한 리스트를 작성한다.
• 요구사항 명세
① 항공티켓을 예약할 경우 잔여석이 있는지 여부를 확인한 후 좌석을 예약한다.
② 좌석은 일등석, 비즈니스석 이코노미석으로 구분되며, 각각의 좌석 요금이 서로 상이하다.
③ 출발 한달 전에 예약하는 경우 10%의 할인가가 적용된다.
④ 비행기 편의 항공사명과 출발 시간을 정보로 입력해야 한다.
⑤ 비행기 티켓은 편도, 왕복으로 구분된다.
• 문서 작성 표준(코딩 규칙)
① 모든 클래스의 주석에는 작성자 작성일, 최종 수정일이 포함되어야 한다.
② 코드 작성 시 들여쓰기의 기준은 탭으로 한다.
③ 클래스, 함수의 시작과 함수의 종료를 나타내는 중괄호(')는 같은 위치에 있어야 한다.
④ 변수는 항상 선언한 후에 사용한다.
• 산출물
import java.sql.*;
public class reservation {
private int rate first = 1000;
private int rate business 600;
private int rate economy = 200;
public void print_flightlist(int class_code) {
String url="jdbc:mysql://localhost:3306/test”;
String id="test”;
String pass="test123";
ResultSet rs;
try {
Class.forName ("com.mysql.jdbc.Driver”);
String t_query="select name, remainseat first,
remainseat business,
remainseat economy from flight”;
Connection conn=DriverManager.getConnection (url, id, pass);
Statement stmt conn.createStatement ();
rs-stmt.executeQuery (t_query);
while(rs.next( )){
System.out.println (rs.getString ("name")
+ rs.getInt ("reaminseat first") + payrate ('1')
+ rs.getInt ("reaminseat business") + payrate ('2')
+ rs.getInt ("reaminseat_economy") + payrate ('3')
};
}
stmt.close();
conn.close();
}
catch (Exception e) {
e.printStackTrace();
}
}
public int payrate (int class_code) {
switch (class_code) {
case 1 :
return rate_first;
case 2 :
return rate business;
case 3 :
return rate_economy;
}
return 0;
}
}
위 예제의 인스펙션 결과인 표에는 결함의 상세 내용과 중요도, 그리고 분류를 기술한다.
No | 결함 상세 내용 | 중요도 | 분류 |
1 | 코드의 상단 주석에 작성자의 이름이 누락되어 있음 | Major | Missing |
2 | 한달 전에 예약할 경우 10% 할인가를 적용하는 소스코드가 누락되어 있음 | Major | Missing |
3 | ... | ||
4 | ... | ||
5 | ... |
표. 인스펙션 결과
4.3 워크쓰루
워크쓰루(Walkthrough)는 인스펙션에 비해 비형식적인 방법으로 주로 개발자의 요청에 의해 이루어지며 완성된 결과물이 아닌 중간 산출물을 대상으로 한다. 주요 목적은 다음 단계로 넘어갈 지에 대한 결정이 아니라, 토론하고 결함을 찾고 그것에 대한 해결책을 서로 조언하는데 있다. 참가자들의 역할이 명확하게 구분되지 않으며 산출물의 작성자 본인이 회의를 주재한다. 또한, 인스펙션은 보통 완전한 산출물이 나온 후에 수행되지만 워크쓰루는 중간 산출물을 대상으로 하기 때문에 SW 개발 어느 단계에서도 행할 수 있다.
워크쓰루 방법은 인스펙션과 달리 참가자들이 작업물을 숙지한 후 회의에 참석하는 것이 아니라 개요 정도를 파악한 후 참여하게 된다. 회의는 프로그램 흐름에 따라 프로그램을 훑어가며 오류를 찾아내는 방식으로 진행된다. 또한, 워크쓰루 회의 후 발견된 결함이 모두 수정이 되었는지 확인하는 후속 작업에 대한 검사가 이루어지지 않을 수 있다.
4.4 심볼릭 실행
프로그램 테스트(Test)와 형식적 검증(Formal verification)은 일반적으로 많이 알려진 프로그램 검증 방법이다. 테스트는 특정 입력값으로 프로그램에 대해 테스트를 수행하고 결과를 확인함으로써 프로그램을 검증하는 방식으로 테스트하지 않은 입력값에 대해서는 프로그램의 정확성을 보장하기 어렵다는 단점이 있다. 형식적 검증 기법은 프로그램을 수행하지 않고 프로그램이 명세서에 명시된 대로 동작하는지 확인하는 방법으로 명세서와 프로그램의 완성도가 높아야 한다. 형식적 검증에 대한 내용은 4.6절에서 자세히 설명한다.
심볼릭 실행(Symbolic execution)은 위에 기술한 프로그램 테스트와 형식적 검증 방법의 중간에 위치한 방법으로, 프로그램의 입력 변수를 기호화 해서 표현하는 SW 분석 기법이다. 심볼릭 실행 수행 시, 프로그램의 출력값은 기호화된 입력 변수들로 이루어진 논리적, 수학적 수식으로 표현된다.
심볼릭 실행은 임의의 프로그램 입력값을 나타내는 심볼을 사용하여 프로그램을 검증하기 때문에 프로그램이 주어진 명세를 만족하는지 확인하기 위해 가능한 모든 입력값으로 프로그램을 실행할 필요가 없으며, 심볼릭 트리를 통해 특정 경로를 실행하는 테스트 데이터 생성에 필요한 정보를 제공한다.
아래 예제를 통해 심볼릭 실행에 대해 자세히 살펴보자.
public class SymExecl
{
public static void main(String args[ ] ){
1 : int valuel;
2 : int value2;
3 : int one = Integer.parseInt (args[0]); // A
4 : int two = Integer.parseInt (args[1]);
5 : valuel = one * one; // A* A
6 : valuel = valuel + 1; // A² + 1
7 : if(valuel <= 0)
8 : value2 -1;
9 : System.out.println("Result:" + valuel);
}
}
3번 라인의 변수 one을 심볼 A라는 기호로 할당하면, 5번 라인의 변수 valuel은 A*A, 즉 A2로, 6번 라인의 valuel은 A2+1이라는 심볼릭 값으로 표현된다. 변수 one을 심볼로 대체함으로써 one에 모든 입력값을 넣어 프로그램을 실행하지 않고도 최종 실행 결과(valuel의 값)는 항상 0보다 크다는 것을 알 수 있다.또한 심볼릭 실행은 심볼 입력값을 통해 경로 조건(Path condition)을 단순화하여 프로그램 상의 실행 불가능한 경로를 찾을 수 있게 한다.
public class SymExec2
{
public static void main(String args[ ] )
{
1 : int valuel;
2 : int value2;
3 : int one = Integer.parseInt (args[0]); //A
4 : int two = Integer.parseInt (args[1]); //B
5 : value1 = one * one; // A* A
6 : value1 = valuel + 1; // A² + 1
7 : value2 = two; // B
8 : if(value1 <= 0) // if (A2 + 1 <=0)
9 : value2 = -1;
10 : if (value1 == 101)
11 : value2 = 100;
12 : value1 = value1 + value2;
13 : if (value1 < 1100)
14 : value2 = 1000;
8번 라인의 if 문을 실행하기 직전의 변수 valuel의 값 (심볼릭 값: A² + 1)은 항상 0보다 크다. 따라서 "value1<=0"의 조건은 항상 False 이며, 경로 3-4-5-6-7-8-9는 실행이 불가능하다는 사실을 알 수 있다.
심볼릭 실행 시 심볼러 실행 트리(Symbolic execution tree)를 통해 프로그램의 경로 조건을 만족하는 값들의 집합을 테스트 데이터 집합으로 사용할 수 있다.
심볼릭 실행 트리는 프로그램의 흐름에 따라 변수를 심볼릭 값으로 치환해 가면서 프로그램을 실행하는 과정을 도식화한 것이다. 심볼릭 실행 트리의 경로 분기점의 기준이 경로 조건이다. 특정 경로를 실행하는 테스트 데이터를 생성하기 위해서는 경로 조건을 만족하는 심볼릭 값을 선택하면 된다. 심볼릭 실행 트리에서 노드는 프로그램의 실행문을, 간선(Directed edge)은 노드에서 노드로의 전이를나타낸다. 노드의 레이블은 실행문 번호(Statement number)를 나타낸다.
위 예제에 대한 심볼릭 실행 트리는 그림과 같다.
① 심볼릭 실행 트리 그리기
심볼릭 실행 트리를 그리기 전에 먼저 세 개의 조건문을 각각 살펴보자.
<첫 번째 조건문(line 8): if(value1<=0)〉
- 심볼릭 값
8번 라인의 조건문을 심볼릭 값으로 치환하면 "if(A²+1<=0)"가 된다. 단순화 하면 “if(A<=-1)"이 경로 조건이 된다.
- True일 경우
4.4절에서 살펴본 바와 같이 실행 불가능한 경로이므로 고려하지 않는다.
- False일 경우
두 번째 조건문으로 이동한다.
<두 번째 조건문(line 10): if(value1==101)〉
- 심볼릭 값
10번 라인의 조건문을 심볼릭 값으로 치환하면 "if(A²+1==101)”이 된다. 단순화 하면 "if(A==100)"가 경로 조건이 된다.
- True일 경우
11번 라인의 value2에 심볼릭 값 B) 100이 할당되며, 12번 라인의 value1의 값은 201이 된다. (value1의 값: 101, value2의 값: 100)
- False일 경우
12라인의 value1는 심볼릭 값 A2+1+B로 치환된다. (value1: A+1,value2: B)
<세 번째 조건문(line 13): if(value1>1100)>
- 심볼릭 값
13번 라인의 조건문을 심볼릭 값으로 치환하면 "if(A²+101<1100)”이 된다. 단순화 하면 “if(A<999)”가 경로 조건이 된다. 세 번째 조건문은 두 번째 조건문에 영향을 받기 때문에 두 번째 조건문이 세 번째 조건문에 추가된다.
- True일 경우
추가된 조건을 고려하여 13번 라인의 조건이 True가 되기 위해서는“(A²==100 && A²+1+100<1100)”이어야 한다. 즉, “(A==100 &&A<999)" 일 경우이다.
- False일 경우
추가된 조건을 고려하여 13번 라인의 조건문이 False가 되는 조건은 아래와같다.
− “(A2 !=100 && A²+1+B<1100)”
− “(A2 !=100 && A²+1+B>=1100)”
− “(A2==100 && A²+1+100>=1100)”
② 테스트 데이터 생성하기
심볼릭 실행 트리를 통해 테스트 데이터를 생성한다. 그림에서 1-2-3-4-5-6-7-8-10-11-12-13-14의 경로를 실행하는 테스트 데이터를 생성하려면 해당경로 조건을 만족하는 A의 값을 구하면 된다. 이 경우 해당 경로를 실행하는 테스트 데이터는 A==100인 값이다. 따라서 변수 one의 테스트 데이터를 양수 또는음수 10으로 선택하면 해당 경로를 실행 할 수 있다.
4.5 자료 흐름 분석
코딩 시 프로그래머는 변수를 정의하지 않고도 사용할 수 있으며, 변수를 초기화하지 않고도 사용할 수 있다. 잘못된 변수 및 값의 사용은 프로그램에 심각한 영향을 미칠 수 있으며, 이로 인한 프로그램 오동작 시 원인을 찾기도 힘들다.
자료 흐름 분석(Data flow analysis) 기법은 프로그램의 제어 흐름에 기반을 둔기법들과는 달리 프로그램 내의 데이터의 정의와 흐름에 대한 패턴을 분석하여 프로그램을 검증하는 기법이다. 자료 흐름 분석 기법을 통해 치명적인 잠재적 오류를 쉽게 발견해 낼 수 있다.
다음은 자료 흐름 분석을 위한 기본적 용어 정의이다.
① 정의됨(Defined)
함수의 입력 인자, 치환문의 왼쪽에 있는 변수 등의 값이 새로 설정되거나 변경되는 경우 변수는 해당 문장에서 “정의되었다"라고 한다.
예) "a=b+c"에서 변수 a는 이 문장에서 정의됨
② 참조됨 (Used)
변수의 값이 변경되지 않고 수식계산이나 조건을 평가할 때 사용될 경우 변수가"참조되었다”라고 말한다. 변수의 참조는 두 가지 종류가 있다. 변수가 일반 수식을 계산할 때 사용되면 계산 참조라 하며 c-use로 나타낸다. 변수가 조건의 참, 거짓을 결정할 때 사용되면 조건 참조라 하며 p-use로 나타낸다.
예) “a=b+c”에서 변수 b, c는 이 문장에서 계산 참조됨
예) “if(d==true)"에서 변수 d는 이 문장에서 조건 참조됨
③ 무효화됨 (Killed)
변수가 선언된 영역 밖으로 벗어날 때 그 변수는 “무효화되었다”라고 한다.자료 흐름 패턴은 표를 참조한다. 몇 가지 자료 패턴은 오류가 발생할 수 있는 가능성을 보여주기 때문에 주의 깊게 살펴보아야 한다. 예를 들어, ku' 쓰임새패턴은 변수가 영역을 벗어나) 무효화된 후에 다시 사용된다는 사실을 나타내기때문에 'null pointer exception' 과 같은 오류가 발생할 수 있다.
기호 | 설명 |
d | 정의됨(Defined) |
u | 참조됨(Used) |
k | 무효화됨(Killed) |
~x | 모든 선행 행위들이 x(d, k 또는 u)와 관련 없음 |
x~ | x 이후에 행위들이 x (d, k 또는 u)와 관련 없음 |
표. 자료 흐름 용어
패턴 | 설명 | |
~d | 처음 정의됨 | 문제 없음 |
du | define-use | 문제 없음 |
dk | define-kill | 잠재적 오류, 자료가 사용되지 않음 |
~u | 처음 사용됨 | 잠재적 오류, 자료가 정의되지 않고 사용됨 |
ud | use-define | 문제 없음, 자료가 사용된 후 다시 정의됨 |
uk | use-kill | 문제 없음 |
~k | 처음으로 무효화 | 잠재적 오류, 자료가 정의되지 않고 무효화됨 |
ku | kill-use | 심각한 오류, 무효화 후 사용됨 |
kd | kill-define | 문제 없음, 무효화 후 다시 정의됨 |
dd | define-define | 잠재적 오류, 연속으로 정의됨 |
uu | use-use | 문제 없음 |
kk | kill-kill | 잠재적 오류 |
d~ | 제일 나중에 발생한 정의 | 잠재적 오류 |
u~ | 제일 나중에 발생한 참조 | 문제없음 |
k~ | 제일 나중에 발생한 무효화 | 문제 없음 |
표. 자료 흐름 패턴
아래 예제 프로그램에서 변수 a는 2번 라인과 3번 라인에서 연속적으로 변수 a가 정의되었으며, 변수 x는 정의되지 않고 7번 라인에서 바로 사용 되었다.
1 : int dfEx (int d1, int d2) {
2 : int a=0, x;
3 : a = d1 + d2;
4 : if (a>0)
5 : x = 1;
else
6 : d1 = 10;
7 : a = a+x;
8 : return a;
9 : }
자료 흐름 | 설명 | |
패턴 | 경로 | |
~d | 1-2 | 문제 없음 |
dd | 2-3 | 잠재적 오류, 두 번 연속으로 정의됨 |
du | 3-4, 7-8 | 문제 없음 |
ud | 7 | 문제 없음 |
uk | 8-9 | 문제 없음 |
uu | 4-5-7, 4-6-7 | 문제 없음 |
k~ | 9 | 문제 없음 |
표. 자료 흐름(변수 a)
자료 흐름 이상 | 설명 | |
패턴 | 경로 | |
du | 5-7 | 문제 없음 |
~u | 2-3-4-6-7 | 잠재적 오류, 자료가 정의되지 않고 바로 사용됨 |
k~ | 9 | 문제 없음 |
표. 자료 흐름(변수 x)
변수 a와 변수 x에 대한 자료 흐름은 표.자료 흐름(변수 a)과 표. 자료 흐름(변수 x)을 참고한다.
자료 흐름 상태 그래프는 자료 흐름 패턴을 입력으로 받아 이상 여부를 알려주는상태 그래프이다. 각 노드는 현재 변수의 상태를 나타내고 노드 간의 간선은 노드의 상태 전이를 나타낸다.
위 예제의 변수 a에 대하여 'uu' 패턴을 보여주는 부분 경로 4-5-7을 생각해보자, 4번 문장은 변수 a를 참조하는 조건식이므로 상태 그래프에서 'U' 상태에 머물게 된다. 5번 문장은 변수 a를 정의하거나 참조하지 않으므로 계속해서 'U' 상태에 머무른다. 7번 문장에서 a를 참조하므로 전이가 이루어지는데 이 경우에는 다시 'U' 상태로 전이가 된다.
그림과 같은 자료 흐름 상태 그래프를 통해 자료 흐름의 잠재적 오류를 쉽게 파악 할 수 있다.
4.6 형식적 검증
형식적 검증(Formal verification)은 프로그램이 주어진 명세나 속성에 부합하는지 수학적 기법을 통해 증명하는 방식을 말한다. 형식적 검증에는 크게 모델 검사(Model checking)와 논리적 추론(Logical inference) 방식이 있다. 본 장에서는 모델 검사에 대해서만 소개한다.
모델 검사 기법이란 대상 프로그램이 수행할 수 있는 모든 가능한 동작을 표현하는 형식 모델을 구축하고, 프로그램의 기대 행위(Desired behavior)를 정형적으로 기술한 후 형식 모델이 기대 행위를 만족하는지 검증하는 방법이다. 모델 각각의 상태가 증명하고자 하는 행위에 도달할 수 있는지의 여부를 증명하는 방법을 도달성 분석(Reachability analysis)이라 한다. 예를 들면, 시스템이 데드락(Deadlock) 상태에 도달할 수 있는지를 검사하기 위하여 시스템의 모든 도달 가능한 상태들을 식별하고 더 이상 진행이 불가능한 상태가 있는지를 검사한다. 오류가 있다면 즉, 모델이 행위를 만족하지 못한다면 반례(Counter example)를 생성한다. 반례는 어떤 상황에서 오류가 발생했는지에 대한 정보를 포함하며, 반례를 통해 형식 모델이 갱신된다. 오류가 없다면, 모델을 정제하여 더욱 구체화 한 후 증명 과정을 반복한다.
개념적으로 모델 검사는 유한 상태 오토마타(Finite State Automata)의 포함관계를 검사하는 것으로 간주할 수 있다. 요구사항과 시스템 모델이 유한 상태 오토마타로 표현되었다고 가정하면, 시스템 모델을 표현하는 오토마타(S)에서 처리될 수 있는 단어들은 요구사항을 표현하는 오토마타(R)에서도 처리 될 수 있어야 한다. 즉, 요구사항 오토마타가 시스템 모델을 표현하는 오토마타를 포함해야 한다. 수식으로 나타내면 다음과 같다.
모델 검사 기법 | |
입력 | 모델, 속성 명세 |
검사방법 | 상태 공간의 탐색 |
출력 | 참 또는 반례 |
표. 모델 검사 기법
S U R
이와 같이 오토마타의 포함 관계를 검사하기 위해서 모델 검사 기법들은 다음과같은 연산을 수행하여 결과가 공집합인지를 검사한다.
R∩S
결과가 공집합이면 시스템 모델은 요구사항을 만족한다는 의미이며, 공집합이아니면 요구사항을 만족하지 않는다는 의미이다.
일반적으로 자료의 처리는 무한한 상태 공간을 야기하기 때문에 모델 검사 방법은 자료 중심적 시스템 보다는 제어 중심적 시스템에 적합하다.
모델 검사는 실제의 시스템이 아닌 시스템의 모델로 검증을 수행하기 때문에 모델 김중의 결과가 실제 시스템의 결과라고 확신할 수 없다. 시스템과 모델의 일치성을 높이기 위해 시스템에서 모델을 자동적으로 추출하는 방법에 대한 연구가 진행되고 있다. 또한 모델 검사는 프로그램 테스트와는 달리 시스템이 주어진 행위를 만족하는지 여부에 대해서 검사할 수 있다.
연습문제
1 정적분석의 특징을 설명하고 정적분석 방법을 설명하시오.
2 인스펙션을 수행하는 과정을 설명하시오.
3 공식 검토, 인스펙션, 워크쓰루의 차이점을 비교 설명하시오.
4 요구사항 분석 및 설계 단계에서 인스펙션을 위해 사용하는 체크리스트의 항목들을 나열하시오.
5 Java 언어로 작성된 프로그램에 대해 코드 인스펙션을 하려고 할 때, 사용할 수 있는 체크리스트 항목들을 조사하고 나열하시오.
6 다음 프로그램에 대해 심볼릭 트리를 구성하시오.
1: d=b+c; 2: if (20) 3: 4: if (b<a) { 5: a=1; 6: if (d<2*b) 7: 8:} a=3* a+d; b=2;
7(5)번 문제에 주어진 프로그램 코드에서 1-2-3-4-5-6-7-8 경로 조건을 구하고, 이 경로를 실행하는 a, b, c를 계산하시오.
8 (5)번 문제에 주어진 프로그램 코드에 대해 자료 흐름 이상을 검출하시오.
|