Timed I/O test sequences for discrete event model verification

Abstract

Model verification examines the correctness of a model implementation with respect to a model specification. While being described from model specification, implementation prepares to execute or evaluate a simulation model by a computer program. Viewing model verification as a program test this paper proposes a method for generation of test sequences that completely covers all possible behavior in specification at an I/O level. Timed State Reachability Graph (TSRG) is proposed as a means of model specification. Graph theoretical analysis of TSRC has generated a test set of timed I/O event sequences, which guarantees 100% test coverage of an implementation under test.