Alloy 명세 기반 자동 테스트 데이터 생성 기법

정인상,Chung, In-Sang 한국정보처리학회 2007 정보처리학회논문지D Vol.14 No.2

일반적으로 테스트 데이터 생성 방법들은 테스트 데이터를 자동으로 생성하기 위해서 완전한 프로그램 경로를 기술한 것을 요구한다. 이 논문에서는 프로그램 경로를 완전하게 명시하지 않아도 테스트 데이터를 자동으로 생성하는 새로운 방법을 제안한다. 이를 위해 이 논문에서는 테스트 대상 프로그램을 1차 관계 논리 언어인 Alloy로 변환하고 Alloy 분석기를 통하여 테스트 데이터를 생성하는 방법을 제안한다. 제안된 방법은 사용자로 하여금 프로그램 경로를 선택하도록 하는 부담을 덜어줄 뿐만 아니라 다양한 테스트 적합성 기준에 따라 테스트 데이터를 생성하는 일을 용이하게 한다. 간단하지만 설명에 도움이 될 수 있는 예들을 통하여 제안한 방법에 대해 설명한다. In general, test data generation techniques require the specification of an entire program path for automated test data generation. This paper presents a new way for generating test data automatically een without specifying a program path completely. For the ends, this paper presents a technique for transforming a program under test into Alloy which is the first order relational logic and then producing test data via Alloy analyzer. The proposed method reduces the burden of selecting a program path and also makes it easy to generate test data according to various test adequacy criteria. This paper illustrates the proposed method through simple, but illustrative examples.

다단계 스택 지향 포인터가 있는 프로그램 테스트를 위한 테스트 데이터 자동 생성

정인상,Chung, In-Sang 한국정보처리학회 2010 정보처리학회논문지D Vol.17 No.4

최근에 콘콜릭 테스트이라 불리는 새로운 테스팅 방법이 많은 관심을 받고 있다. 콘콜릭 테스팅은 높은 테스트 커버리지를 달성하기 위해 실제 프로그램 수행과 심볼릭 수행을 결합하여 테스트 데이터를 생성한다. CREST는 콘콜릭 테스팅을 구현한 대표적인 open-source 테스트 도구이다. 그러나 현재 CREST는 입력으로 정수형만 다룬다. 이 논문은 포인터형인 입력이 존재하는 경우에 자동 테스트 데이터 생성을 위한 새로운 규칙을 제안한다. 이 규칙들은 C 프로그램에서 주로 사용되는 다단계 스택 지향 포인터를 효과적으로 처리한다. 또한, 이 논문에서는 제안 된 규칙을 구현한 vCREST라 불리는 도구에 대해 기술하고 C 프로그램에 적용한 결과도 함께 기술한다. Recently, a new testing technique called concolic testing receives lots of attention. Concolic testing generates test data by combining concrete program execution and symbolic execution to achieve high test coverage. CREST is a representative open-source test tool implementing concolic testing. Currently, however, CREST only deals with integer type as input. This paper presents a new rule for automated test data generation in presence of inputs of pointer type. The rules effectively handles multi-level stack-directed pointers that are mainly used in C programs. In addition, we describe a tool named vCREST implementing the proposed rules together with the results of applying the tool to some C programs.

SAT를 이용한 MC/DC 블랙박스 테스트 케이스 자동 생성

정인상,Chung, In-Sang 한국정보처리학회 2009 정보처리학회논문지D Vol.16 No.6

항공 소프트웨어가 FAA(미국연방항공청)에 승인받기 위해서는 DO-178B 표준에 따라야 한다. DO-178B에서는 안전 필수 소프트웨어의 단위 테스트가 MC/DC 기준을 만족하기를 요구하고 있다. MC/DC에 따른 테스트는 안전성과 관련된 오류를 효과적으로 찾을 수 있는 수단으로 알려져 있지만 MC/DC를 만족하는 테스트 케이스를 생성하는 작업이 용이하지 않는 것도 사실이다. 이 논문에서는 MD-SAT이라고 명명한 SAT(SATisfiability) 기술을 사용하여 MC/DC를 만족하는 테스트 케이스를 자동으로 생성하는 도구에 대해 소개한다. 이 도구는 결정표 기반 테스트, 인과 그래핑 및 상태 전이 테스트 방법을 구현한 도구에서 보다 다양한 테스트 케이스 생성을 위해 사용될 수 있다. Airbone software must comply the DO-178B standard in order to be certified by the FAA. The standard requires the unit testing of safety-critical software to meet the coverage criterion called MC/DC(Modified Condition/Decision Coverage). Although MC/DC is known to be effective in finding errors related to safety, it is also true that generating test cases which satisfy the MC/DC criterion is not easy. This paper presents a tool named MD-SAT which generates MC/DC test cases with SAT(SATisfiability) technology. It can be employed for generating diverse test cases in tools implementing various testing techniques including decision table based test, cause-effect graphing, and state-based test.

Do3 CuZnAl 합금에 있어서의 역형상기억효과

정인상,이인철,박정식,이순린 ( In Sang Chung,In Chul Lee,Jung Sig Park,Soon Lin Lee ) 한국열처리공학회 1990 熱處理工學會誌 Vol.3 No.2

Since the reverse shape memory effect(RSME) was reported in a CuZnAl alloy, further study has been done on the mechanism of this phenomenon and reported that it occurs by the bainitic transformation. But the present authors revealed in the previous work that the RSME in a B2 CuZnAl alloy is not caused by the shear process involved in the bainitic transformation and also that the RSME takes place as the remaining α`₂phase, which is two-step transformed strain induced martensite, is newly transformed into α phase. In order to provide further evidence in supporting the facts, thus, more detailed investigations have been carried out in a DO₃CuZnAl alloy.

복합열처리한 연강의 표면경화에 관한 연구

정인상,전해동,신석목 ( In Sang Chung,Hae Dong Chon,Soug Mok Sin ) 한국열처리공학회 1992 熱處理工學會誌 Vol.5 No.1

It is investigated that Fe-C-N compound layer, defusion layer, and induction hardened layer produced by nitrocarburizing blend heat treatment in austenitic temperature with high frequency induction heating of mild steel specimen sprayed sursulf salt-bath. As the temperature of blend-heat treatment got increased, the thickness and hardness of compound layer and diffusion layer were increased. Compound layer(max. 35㎛), diffusion layer (max. 2.5㎛) and induction hardened layer were gained in the shortest time 10 sec and in the case of 1000℃ total hardness depth of those was about 3.5㎜. When the blend-heat treated specimen was repeated, maximum hardness of compound layer was dropped more than that of the repeated compound layer after sursulf treated, whereas hardness of diffusion layer was increased.

SAT를 기반으로 하는 플래그 변수가 있는 프로그램 테스팅을 위한 테스트 데이터 자동 생성

정인상,Chung, In-Sang 한국정보처리학회 2009 정보처리학회논문지D Vol.16 No.3

Recently, lots of research on automated test data generation has been actively done. However, techniques for automated test data generation presented so far have been proved ineffective for programs with flag variables. It can present problems when considering embedded systems such as engine controllers that make extensive use of flag variables to record state information concerning devices. This paper introduces a technique for generating test data effectively for programs with flag variables. The presented technique transforms the test data generation problem into a SAT(SATisfiability) problem and makes advantage of SAT solvers for automated test data generation(ATDG). For the ends, we transform a program under test into Alloy which is the first-order relational logic and then produce test data via Alloy analyzer. 최근에 테스트 데이터를 자동으로 생성하는 방법에 관한 연구가 활발하게 진행되고 있다. 그러나 이러한 방법들은 플래그 변수가 프로그램에 존재하는 경우에는 효과적이지 못함이 밝혀졌다. 이는 엔진 제어기와 같은 내장형 시스템들이 전형적으로 디바이스 관련 상태 정보를 기록하기 위해 플래그 변수를 많이 이용한다는 점을 고려할 때 문제가 된다. 이 논문에서는 플래그 변수가 있는 프로그램에 대하여 효과적으로 테스트 데이터를 생성할 수 있는 방법을 소개한다. 이 방법은 테스트 데이터 생성 문제를 SAT(SATisfiability) 문제로 변환하고 SAT 해결도구를 이용하여 자동으로 테스트 데이터를 생성한다. 이를 위해 프로그램을 1차 관계 논리 언어인 Alloy로 변환하고 Alloy 분석기를 통하여 테스트 데이터를 생성한다.

논문 : Cu - Zn - Al 형상기억합금에 (形狀記憶合金) 있어서 역형상기억효과 (逆形狀記憶效果)

정인상(In Sang Chung),이인철(In Chul Lee),박정식(Jung Sik Park) 대한금속재료학회(구 대한금속학회) 1990 상변태 심포지엄 Vol.2 No.-

프로그램을 재검증하기 위한 최소 경로 선택 방법

정인상(In Sang Chung),권용래(Yong Rae Kwon) 한국정보과학회 1991 한국정보과학회 학술발표논문집 Vol.18 No.2

소프트웨어의 유지/보수에 관련한 작업들은 프로그램의 빈번한 변경을 초래하며 프로그램이 변경된 후에는 수정 의도가 맞게 프로그램이 변경되었는지를 조사하기 위한 재검증(revalidation)이 필요하다. 본 논문에서는 프로그램이 변경될 때마다 재검증하는 노력을 줄이기 위해 Horowitz의 프로그램 비교 알고리즘을 이용한 재검증 조건과, 0-1 integer programming을 이용하여 재검증하여야 하는 프로그램의 경로의 수를 최소로 선택하는 방법을 제시한다.

포함, 파워 관계, 및 테스트 재사용성에 기반을 둔 객체지향 프로그램을 위한 테스트 기준의 비교방법

정인상(In Sang Chung) 한국정보과학회 1995 정보과학회논문지 Vol.22 No.5

클래스들의 신뢰성을 확보할 목적으로 객체지향 프로그램을 위한 테스팅 기법이 소개되고 있다. 테스팅 기법들은 테스트케이스의 선택과 테스팅 종료시점을 안내할 목적으로 보통 테스트 기준을 바탕으로하고 있다. 전통적인 테스팅 기법과는 달리 객체지향 프로그램을 위한 테스트 기준을 비교하는 방법에 관한 연구는 미미한 실정이다. 테스팅 기법의 수준을 평가할 뿐만아니라 더욱 효율적인 테스팅 기법의 개발을 위해서 객체지향 프로그램을 위한 정형적인 테스트 기준의 평가 틀이 요구된다. 본 논문에서는 객체지향 프로그램을 테스팅 하는데 사용할 수 있는 테스트 기준들을 비교하기 위한 방법들을 제시한다. 각 비교 방법은 테스트 기준을 충족하는 어려움정도, 오류검출 능력 및 테스트 재사용성을 바탕으로 하고 있다. 또한 일관되게 테스트 기준을 비교하기 위하여 객체지향 프로그램을 위한 테스트 기준을 형식화 한다. Some testing techniques for object-oriented programs have been presented for the purpose of establishing the confidence of the reliability of classes. Usually, testing techniques are based on some form of test criteria to guide the test case selection and to determine when the testing process is to be terminated. Unlike traditional software testing, few have attempted to address how to compare test criteria for object-oriented programs. It is required to provide a formal framework for comparing test criteria for object-oriented programs in order to develop more effective testing techniques as well as to certify the quality of testing techniques. In this paper, we present some methods of comparing test criteria for object-oriented programs which provide different orderings of criteria. Each method of comparison is based on the relative difficulty of satisfying criteria, the error exposing ability, and the test reusability. We also formalize the notion of test criteria for object-oriented programs in order to compare criteria in the uniform way.

연역 데이타베이스를 이용한 객체지향 프로그램의 분석

정인상(In-Sang Chung),김희진(Hee-Jin Kim),최만용(Maan-Yong Choi),안상원(Sang-Won Ahn),이광모(Kwang-Mo Lee) 한국정보과학회 1996 한국정보과학회 학술발표논문집 Vol.23 No.1A

객체지향 개념에서 제공되는 특성들은 소프트웨어를 개발하는데 많은 이점을 주고 있지만 이러한 장점들이 나중에 소프트웨어를 유지보수하는데 많은 어려움을 주고 있는 요인이 되고 있다. 이 논문에서는 이러한 어려움을 해결해 주고 사용자의 질의에 응답을 주는 연역 데이타베이스를 사용한 객체지향 프로그램 분석도구를 제안한다.