Modeling Pairwise Test Generation from Cause-Effect Graphs as a Boolean Satisfiability Problem

Chung, Insang The Korea Contents Association 2014 International Journal of Contents Vol.10 No.3

A cause-effect graph considers only the desired external behavior of a system by identifying input-output parameter relationships in the specification. When testing a software system with cause-effect graphs, it is important to derive a moderate number of tests while avoiding loss in fault detection ability. Pairwise testing is known to be effective in determining errors while considering only a small portion of the input space. In this paper, we present a new testing technique that generates pairwise tests from a cause-effect graph. We use a Boolean Satisbiability (SAT) solver to generate pairwise tests from a cause-effect graph. The Alloy language is used for encoding the cause-effect graphs and its SAT solver is applied to generate the pairwise tests. Using a SAT solver allows us to effectively manage constraints over the input parameters and facilitates the generation of pairwise tests, even in the situations where other techniques fail to satisfy full pairwise coverage.

Investigating Effectiveness of Software Testing with Cause-Effect Graphs

Insang Chung 보안공학연구지원센터 2014 International Journal of Software Engineering and Vol.8 No.7

Automated Goal-Oriented Testing for Pointer Programs with SAT

Insang Chung 한국멀티미디어학회 2008 한국멀티미디어학회 국제학술대회 Vol.2008 No.-

Few works have been done on Automated Test Data Generation (ATDG) in the presence of pointers. This paper presents the rules for translating programs with pointers to the first-order relational logic, Alloy. The approach allows us to consider the test data generation problem into a SAT (SATisfiability) problem and makes advantage of SAT solvers for ATDG. In addition, it supports the goal-oriented test data generation that does not require the specification of an entire path.

Using Boolean Satisfiability Solving for Pairwise Test Generation from Cause-Effect Graphs : Comparison of Three Approaches

Insang Chung 보안공학연구지원센터 2015 International Journal of Software Engineering and Vol.9 No.9

Cause-effect graphs can be used for specifying safety critical systems including avionics control software that are often intended to satisfy Boolean expression. Using cause-effect graphs for requirements-based testing demands the ability of dealing with various constraints in cause-effect graphs. Due to its rapid advance, Boolean Satisfiability (SAT) solving seems to be a promising approach for constraint handling. In this paper, we present three approaches using SAT solving for pairwise test generation from cause-effect graphs. One is an ideal approach that tries to obtain a minimal set of tests. Another approach focuses on breaking the problem to smaller solvable problems to scale the applicability of SAT solving. The other makes full use of a partial instance that forms a part of a solution known priori. We compare the three approaches in terms of the number of generated pairwise tests and fault detection capability. Comparison results show that an approach using partial instances can generate less number of pairwise tests than the other two approaches without degrading fault detection capability.

Modeling Pairwise Test Generation from Cause-Effect Graphs as a Boolean Satisfiability Problem

Insang Chung 한국콘텐츠학회(IJOC) 2014 International Journal of Contents Vol.10 No.3

A cause-effect graph considers only the desired external behavior of a system by identifying input-output parameter relationships in the specification. When testing a software system with cause-effect graphs, it is important to derive a moderate number of tests while avoiding loss in fault detection ability. Pairwise testing is known to be effective in determining errors while considering only a small portion of the input space. In this paper, we present a new testing technique that generates pairwise tests from a cause-effect graph. We use a Boolean Satisbiability (SAT) solver to generate pairwise tests from a cause-effect graph. The Alloy language is used for encoding the cause-effect graphs and its SAT solver is applied to generate the pairwise tests. Using a SAT solver allows us to effectively manage constraints over the input parameters and facilitates the generation of pairwise tests, even in the situations where other techniques fail to satisfy full pairwise coverage.

CEGPairGen : An Automated Tool for Generating Pairwise Tests from Cause-Effect Graphs

Insang Chung 보안공학연구지원센터 2015 International Journal of Software Engineering and Vol.9 No.1

Pairwise testing is known to be effective in finding errors while considering only a small fraction of input space. Recently, a new testing technique that generates pairwise tests from the cause-effect graph has been presented. This technique assumes the use of the Alloy analyzer to generate pairwise tests from the cause-effect graph. Since, however, the Alloy analyzer does not support APIs that build and manipulate the Alloy formulas, the task of test generation may be tedious and error-prone. In this paper, we introduce a tool named CEGPairGen that automates the process of generating pairwise tests from the cause-effect graph without any human intervention. CEGPairGen produces a test generator written in Java KodKod APIs that generates pairwise tests from a given cause-effect graph. KodKod has been designed to efficiently construct, manipulate, and solve constraints. CEGPairGen takes an incremental test generation strategy for situations where the number of pairs to be covered grows quickly. We show a case study where experimental assessment of tests produced by CEGPairGen has been carried out.

자동화된 프로그램 시험을 위한 입력 자료구조의 모양 식별

정인상(Insang Chung) 한국정보과학회 2004 정보과학회논문지 : 소프트웨어 및 응용 Vol.31 No.10

프로그램 시험 비용은 테스트 데이타를 생성하는 과정을 자동화함으로써 상당히 즐일 수 있다. 테스트 데이타 생성은 보통 선택된 프로그램 경로를 실행하는 입력 값들을 식별하는 데 주안점을 둔다. 지금까지 많은 연구가 있어왔지만 여전히 해결해야할 문제가 있다. 그러한 문제들 중에 모양 문제가 있다. 모양 문제는 주어진 프로그램 경로를 수행하기위해 요구되는 입력 자료구조를 밝혀내는 문제이다. 이 논문에서 이 모양 문제에 대한 새로운 방법을 제시한다. 이 방법은 주어진 경로를 포인터 역참조가 없는 정적단일 할당문 (Static Single Assignment, SSA) 형태로 변환한다. 이는 주어진 경로 상에 존재하는 각 프로그램 문장을 등식이나 부등식과 같은 제약식으로 간주할 수 있게 해준다. 이러한 제약식에 대한 해는 각 입력 변수에 대한 “points-to relation” 형태로 나타난다. 간단한 예들을 통하여 제안한 방법에 대해 설명한다. We can significantly reduce the cost of program testing by automating the process of test data generation. Test data generation usually concerns identifying input values on which a selected path is executed. Although lots of research has been done so far, there still remains a lot of issues to be addressed. One of the issues is the shape problem. The shape problem refers to the problem of figuring out a shape of the input data structure required to cause the traversal of a given path. In this paper, we introduce a new method for the shape problem. The method converts the selected path into static single assignment (SSA) form without pointer dereferences. This allows us to consider each statement in the selected path as a constraint involving equality or inequality. We solve the constraints to get a solution which will be represented in terms of the points-to relations for each input variable. Simple, but illustrative examples are given to explain the proposed method.

분기 커버리지를 위한 동적 테스트 데이터 생성

정인상(Chung Insang),성영락(Seong Yeong Rak) 한국정보과학회 2012 한국정보과학회 학술발표논문집 Vol.39 No.1B

일반적으로 테스트 데이터 자동 생성을 지원하기 위해 심볼릭 실행기나 제약 해결기와 같은 도구를 요구한다. 그러나 이와 같은 도구들을 개발하는 것은 상당한 노력이 요구되는 것도 사실이다. 이 논문에서는 이러한 도구들의 지원 없이 분기 커버리지를 효과적으로 달성할 수 있는 테스트 데이터 생성 방법을 제안한다. 이를 위해 경로 지향 테스트 데이터 생성을 위해 개발된 Korel의 방법을 확장하여 프로그램의 분기들을 가능한 많이 실행할 수 있는 테스트 데이터를 효과적으로 생성하는 방법을 제안한다.

목적 지향 콘콜릭 테스팅

정인상(Insang Chung),박정규(Jungkyu Park) 한국정보과학회 2010 정보과학회논문지 : 소프트웨어 및 응용 Vol.37 No.10

콘콜릭 테스트는 높은 테스트 커버리지를 달성하기 위해 실제 프로그램 수행과 심볼릭 수행을 결합하여 테스트 데이터를 생성한다. CREST는 콘콜릭 테스팅을 구현한 대표적인 open-source인 테스트 도구이다. 그러나 현재 CREST는 기본적으로 프로그램의 모든 가능한 실행 경로들을 탐색하는 것을 목적으로 한다. 이 때문에 특정 분기 또는 블록만을 테스트하는 경우에는 비효율적일 수 있다. 이 논문에서는 프로그램 상의 한 분기 또는 블록을 주고 이를 실행할 수 있는 테스트 데이터를 생성하는 목적 지향 콘콜릭 테스트 방법을 제안한다. 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 aims at exploring all possible execution paths. In case of testing a specific branch or block, thus, it can be ineffective. This paper suggests a goal-oriented concolic testing that generates test data to execute a given branch or block.

특허 문서 분류를 위한 영역-자질 선택 방법

강민규(Minkyu Kang),정인상(Insang Chung),강승식(Seungshik Kang) 한국정보과학회 2009 한국정보과학회 학술발표논문집 Vol.36 No.1

특허 출원을 위한 기존의 특허 문서와의 비교 요구가 항상 존재하는 특허 문서 검색에 있어서 사용자 요청에 맞는 문서를 추출해주기 위해 정확하고 세분화된 문서 분류의 기준이 필요하다. IPC 등의 국제 표준이 존재하지만 모든 범위에 걸쳐서 완벽한 분류 기준을 제시해 주지 못하기 때문에 검색 서비스에서는 제2, 제3의 분류 기준을 갖추고 있어야 하고, 그에 맞춰진 자동 분류 시스템을 구현해야 한다. 특허 문서와 같은 특수 문서의 검색에 있어서 분류 성능을 높이기 위한 영역 선택과 자질 선택은 필수라고 할 수 있다. 이에 따라 본 논문에서는 특허 문서의 텍스트 필드에 대한 분석을 통해 특정 영역에서 자질로 선택해도 좋을 만한 품사를 살펴보고, 각 영역과 품사에 대한 분류 실험을 통해 특허 문서의 분류에 있어서 더 나은 성능을 보여줄 수 있는 방법을 제안하고자 한다.