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

정인상,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.

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.

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 분석기를 통하여 테스트 데이터를 생성한다.

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

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

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

퍼지 이론을 이용한 실시간 시스템의 모델링 및 검증

정인상(In Sang Chung),배현섭(Hyun Seop Bae),권용래(Yong Rae Kwon) 한국정보과학회 1998 정보과학회논문지(B) Vol.25 No.6

실시간 시스템 개발에 있어서 가장 중요한 요소 중에 하나는 시스템의 시간 특성을 정확히 모델링하고, 그 모델이 주이진 시간 제약을 만족하는지를 검증하는 것이다. 그러나, 요구 명세 및 설계 단계에서 시스템의 정확한 시간 특성을 예측하고 측정하는 것은 거의 불가능하다. 이는 시스템 개발 중에 다양한 형태의 시간 불확정성이 유발되기 때문인데 이런 불확정성을 개발 초기 단계에서 적절하게 모델링하고 검증하지 않은 경우에 구현된 시스템에 예측하지 못한 오류가 발생할 수 있다. 본 논문에서는 이와 같은 실시간 시스템의 시간 불확정성을 모델링하기 위해서 기존의 duration calculus를 확장한fuzzy duration calculus를 제시한다. Fuzzy duration calculus에서는 시간을 표현하는데 퍼지 개념을 도입함으로써 시스템이 가지고 있는 모호한 시간 특성을 모델링할 수 있다. 또한 이 논문에서는 확장된 fuzzy duration calculus에 대한 의미와 증명 체계를 정의하고 이 정의를 바탕으로 실제 원자력 발전소 제어 시스템의 일부분에 대한 모델링과 검증 사례를 설명한다. Modeling the timing behaviors of systems and verifying the timing constraints against the model are key steps in developing the real-time systems. However, it appears to be extremely difficult to predict and measure precise timing behavior of the target real-time systems at the earlier development phases of life cycle. Timing uncertainty, if not considered properly in the modeling and verifying steps, may induce subtle but critical errors in final real-time systems. We suggest a way of dealing with such timing uncertainty using an extended duration calculus formalism. The extended duration calculus, named fuzzy duration calculus, allows us to specify uncertain timing behavior of the system using fuzzy theory Semantics and proof system of the duration calculus are re-defined in order to accommodate fuzzy concepts. Based on the semantics and proof system, we can verify timing constraints against the system model. A partial development of Nuclear Power Plant(NPP) control system demonstrates the feasibility and the effectiveness of our approach.

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

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

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

회장이란 중책을 맡고

정인상(In Sang Chung) 한국열처리공학회 2000 熱處理工學會誌 Vol.13 No.4