A Method of Virtual Test Based on Model Checking and a Case Study

In this paper a virtual test method, which is a fusion approach on the combination of automata-based model checking theory and systems engineering theory, is proposed. An automaton of Window Tree Model (WTM) based on multi-tree to describe the system behavior as a system model is used on one hand, and a State Transition Graph (STG) based on Buchi automaton to describe design correctness as a specification is used on the other hand. An automaton-based model checking mechanism is designed to build the foundation of the virtual test method. Moreover, the two main aspects of the method, which are the design correctness verification and the interface test, are defined. A case study is followed to illustrate the modeling and verification process. Finally, a Virtual Test Platform (VTP), which implements the method, is introduced to unfold the virtual test configuration, virtual test execution as well as the virtual test evaluation features.