Testing is a dynamic activity to check the system behavior against the specification without analyzing the entire state space of the implementation. Effective testing process must address test cases, oracles, and adequacy criteria. Especially in the testing of event-driven real-time systems, the test cases include event sequences and the time of each event occurring. Most previous researches for the testing of real-time systems could generate the latter case only.
In this thesis we propose some adequacy criteria and a method of generating the event sequences from Modechart specification using symbolic execution. For applying the symbolic execution to the specification of event-driven real-time systems, we define symbolic system configuration which describes the computation of such systems. We execute the specification symbolically, build real-time symbolic execution tree with the execution traces, and generate the test sequences from this tree. By applying the proposed method to event-driven real-time systems, the test cases are generated effectively.
테스팅이 효과적으로 이루어지기 위해서는 테스트 케이스, 오라클, 만족 조건 등이 제공되어야 한다. 특히 사건기반 실시간 시스템의 테스트 케이스는 일련의 사건 순서 집합과 각 사건이 발생하는 시간에 관한 정보를 포함하고 있어야 한다. 하지만 지금까지의 실시간 시스템 테스팅을 위한 테스트 케이스 생성에 대한 연구에서는 각 사건이 발생하는 시간만을 고려하였다.
이 논문에서는 Modechart로 기술된 명세로부터 일련의 사건 순서 집합을 생성하는 방법과 이때 사용될 수 있는 만족 조건들을 제안하였다. 사건 순서 집합을 구하는 방법으로 시간에 관한 기호적 실행을 이용하였다. Modechart 명세의 기호적 실행을 위하여 기호 시스템 형상을 정의하고 이것을 이용하여 명세를 기호적으로 실행하였다. 기호적 실행을 수행할 때 제안된 만족 조건이 실행의 종료 규칙으로 사용된다. 이렇게 수행된 실행 경로들을 트리의 형태로 표현하고, 만들어진 트리로부터 사건 순서 집합을 구하였다.
실시간 시스템 명세의 각 실행 경로는 두 사건사이의 시간 구간에 의존하여 결정되는 데, 이러한 시간 영역을 기호적 실행을 이용하여 정확히 찾아낼 수 있었다. 또한 제안된 방법이 각 사건의 발생 시간에 관한 테스트 케이스 생성 방법의 하나인 영역 테스팅 방법과 결합된다면, 실시간 시스템 테스팅을 위한 완전한 테스트 케이스 생성 방법이 될 수 있다.
