정형적 명세를 이용하면 원시코드의 복잡함에 방해받지 않고 필요한 구현 정보를 테스트 프로그래머가 얻을 수 있다. 특히 웹 기반 소프트웨어는 정형적 명세로 시스템에 대한 외부 입력과 반응을 잘 나타낼 수가 있다. 이 논문에서는 정형적 명세를 이용하여 테스트 데이터를 추출하는 방법을 제안한다. 복잡하고 구성요소가 다양한 웹 어플리케이션의 기능을 Object-Z 정형 명세언어를 이용하여 핵심적으로 나타낸다. 정형 명세에서부터 상태모델을 구성하고 최상위 레벨의 STD에서 세부적으로 STD를 추가하여 테스트 시나리오를 추출하였다. 실험 대상은 보안과 정확성을 요하는 웹 뱅킹 시스템으로 정하고 계좌이체 과정의 테스트 데이터를 추출하였다. 제안한 방법은 사용기반 테스트 기법과 결합하여 웹 소프트웨어의 테스트 자동화에 중요한 요소가 될 것이다.
Programmers can be got the test-related information for implementation without interference of source code complexity by use of the formal specification. Especially the external inputs and system responses can be represented precisely by formal specification in testing phase of web-based software systems. This paper suggests a method of extracting test cases by use of formal specification. Object-Z formal specification represents various test-related information for complex functions of web-based applications. State Transition Models could be built from the formal specification so that test scenarios were extracted from STDs from the highest level to detail levels. The target system for verification of this method is a web-based banking system which is necessary to be secured and critical on errors. This method would be an important factor in automatizing test procedure for web-based application software systems combining the user-base test technique.
