Although testing has been widely recognized as a practical means of establishing that the software meets its intended purpose, it is an extremely costly and time consuming process.
Model checking is proposed as an automatic verification technique to analyze whether a system model satisfies the system properties. However, we are interested in its capability to generate counterexamples as well as its verification function. Our concern is how model checking be employed in automatic generation of test cases.
In this thesis we apply model checking technique to data-flow oriented test case generation from statecharts specification. We first identify the data flow information from the statecharts. The statecharts is then translated into the form of model checker`s input. Then the properties are generated using the data flow information of the statecharts to force the SMV, the model checker we use, to generate test cases. We have conducted a case study with a real world example to demonstrate that data-flow oriented test cases can indeed be obtained by utilizing our ideas.
테스팅은 소프트웨어의 품질을 보증하는 실제적인 방법으로서 가장 많이 이용되고 있지만 높은 비용과 노력을 필요로 하고 있다.
이러한 테스팅 과정을 자동화 하기 위하여 모델 체킹 방법을 사용할 수 있다. 모델 체킹은 시스템 모델이 특정 성질을 만족하는지를 검증하기 위해 제안된 자동화된 방법으로서 그 성질이 만족되지 않는 경우에 대해서는 반례를 생성해 준다. 이러한 반례는 테스트 케이스를 생성하는데 사용되어 질 수 있다.
본 논문에서는 모델 체킹 도구인 SMV를 이용하여 statecharts로 기술된 정형 명세로부터 자료 흐름 지향 테스트 케이스 생성을 자동화 할 수 있는 방법을 제안하고 있다. 우선 statecharts를 SMV 입력 언어로 바꾸는 과정을 소개하고, statecharts에서 나타나는 자료 흐름 정보를 이용하여 SMV로부터 반례를 생성하는 방법을 제안하였다.
본 논문에서 제안한 방법에 따라 월성 원자로 제어 정지 시스템에 대한 자료 흐름 지향 테스트 케이스를 생성해 볼 수 있었다.
